Proof Step: c_0_56

name: c_0_56 syntax: thf role: plain inference: fof_simplification

Proof State Overview

proof_step c_0_0 ⊕ divide_divide_real pi numeral_numeral_real bit0 one = the_real ? c_0_56 ⊕ divide_divide_real pi numeral_numeral_real bit0 one = the_real ? c_0_0->c_0_56 c_0_59 ⊕ divide_divide_real pi numeral_numeral_real bit0 one = the_real ? c_0_56->c_0_59

Input Dependencies

c_0_0

Assumptions

c_0_0

Conclusion

c_0_56

Dependents

c_0_59

Formula

( ( divide_divide_real @ pi @ ( 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 ) ) ) )

Source

inference(fof_simplification,[status(thm)],[c_0_0])