Proof Step: c_0_76

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

Proof State Overview

proof_step c_0_2 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_65 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_2->c_0_65 c_0_76 ⊕ times_times_real numeral_numeral_real bit0 one the_real ? = pi c_0_65->c_0_76 c_0_88 ⊕ times_times_real numeral_numeral_real bit0 one divide_divide_real pi numeral_numeral_real bit0 one = pi c_0_76->c_0_88

Input Dependencies

c_0_2

Assumptions

c_0_65

Conclusion

c_0_76

Dependents

c_0_88

Formula

( ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) )
  @ ( 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 ) ) ) )
= pi )

Source

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