Proof Step: c_0_97

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_77 ⊕ X2 = zero_zero_real ⊖ powr_real X2 X4 = zero_zero_real c_0_0->c_0_77 c_0_1 c_0_1 c_0_78 ⊕ powr_real X2 semiri2110766477t_real X9 = power_power_real X2 X9 ⊖ ord_less_real zero_zero_real X2 c_0_1->c_0_78 c_0_97 ⊕ X2 = zero_zero_real ⊖ power_power_real X2 X9 = zero_zero_real ⊖ ord_less_real zero_zero_real X2 c_0_77->c_0_97 c_0_78->c_0_97 c_0_124 ⊖ powr_real numeral_numeral_real X8 numeral_numeral_real X11 = zero_zero_real c_0_97->c_0_124

Input Dependencies

c_0_0 c_0_1

Assumptions

c_0_77 c_0_78

Conclusion

c_0_97

Dependents

c_0_124

Formula

! [X9: nat,X2: real] :
  ( ( X2 = zero_zero_real )
  | ( ( power_power_real @ X2 @ X9 )
   != zero_zero_real )
  | ~ ( ord_less_real @ zero_zero_real @ X2 ) )

Source

inference(evalgc,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78])])