Proof Step: c_0_68

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

Proof State Overview

proof_step c_0_3 ⊕ ord_less_eq_real divide_divide_real pi numeral_numeral_real bit0 one numeral_numeral_real bit0 one c_0_61 ⊕ ord_less_eq_real divide_divide_real pi numeral_numeral_real bit0 one numeral_numeral_real bit0 one c_0_3->c_0_61 c_0_68 ⊕ ord_less_eq_real divide_divide_real pi numeral_numeral_real bit0 one numeral_numeral_real bit0 one c_0_61->c_0_68 c_0_79 ⊕ ord_less_eq_real divide_divide_real pi numeral_numeral_real bit0 one numeral_numeral_real bit0 one c_0_68->c_0_79

Input Dependencies

c_0_3

Assumptions

c_0_61

Conclusion

c_0_68

Dependents

c_0_79

Formula

ord_less_eq_real @ ( divide_divide_real @ pi @ ( numeral_numeral_real @ ( bit0 @ one ) ) ) @ ( numeral_numeral_real @ ( bit0 @ one ) )

Source

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