Proof Step: c_0_179

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

Proof State Overview

proof_step c_0_21 ⊖ zero_zero_real = numeral_numeral_real X54 c_0_159 ⊖ numeral_numeral_real X3 = zero_zero_real c_0_21->c_0_159 c_0_179 ⊖ numeral_numeral_real X3 = zero_zero_real c_0_159->c_0_179 c_0_208 ⊖ divide_divide_real pi esk1_0 = zero_zero_real c_0_179->c_0_208

Input Dependencies

c_0_21

Assumptions

c_0_159

Conclusion

c_0_179

Dependents

c_0_208

Formula

! [X3: num] :
  ( ( numeral_numeral_real @ X3 )
 != zero_zero_real )

Source

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