Proof Step: c_0_77

name: c_0_77 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_0 ⊕ divide_divide_real pi numeral_numeral_real bit0 one = the_real ? c_0_66 ⊕ the_real ? = divide_divide_real pi numeral_numeral_real bit0 one c_0_0->c_0_66 c_0_77 ⊕ the_real ? = divide_divide_real pi numeral_numeral_real bit0 one c_0_66->c_0_77 c_0_88 ⊕ times_times_real numeral_numeral_real bit0 one divide_divide_real pi numeral_numeral_real bit0 one = pi c_0_77->c_0_88

Input Dependencies

c_0_0

Assumptions

c_0_66

Conclusion

c_0_77

Dependents

c_0_88

Formula

( ( the_real
  @ ^ [Z0: real] :
      ( ( ord_less_eq_real @ zero_zero_real @ Z0 )
      & ( ord_less_eq_real @ Z0 @ ( numeral_numeral_real @ ( bit0 @ one ) ) )
      & ( ( cos_real @ Z0 )
        = zero_zero_real ) ) )
= ( divide_divide_real @ pi @ ( numeral_numeral_real @ ( bit0 @ one ) ) ) )

Source

inference(evalgc,[status(thm)],[c_0_66])