Proof Step: c_0_100

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

Proof State Overview

proof_step c_0_4 ⊖ zero_zero_real = numeral_numeral_real X11 c_0_81 ⊖ numeral_numeral_real X8 = zero_zero_real c_0_4->c_0_81 c_0_100 ⊖ numeral_numeral_real X8 = zero_zero_real c_0_81->c_0_100 c_0_124 ⊖ powr_real numeral_numeral_real X8 numeral_numeral_real X11 = zero_zero_real c_0_100->c_0_124 c_0_207 ⊖ x = zero_zero_real c_0_100->c_0_207

Input Dependencies

c_0_4

Assumptions

c_0_81

Conclusion

c_0_100

Dependents

c_0_124 c_0_207

Formula

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

Source

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