Theorem zlteqd ≪ | index | src | ≫ 

theorem zlteqd (_G: wff) (_m1 _m2 _n1 _n2: nat):
  $ _G -> _m1 = _m2 $ >
  $ _G -> _n1 = _n2 $ >
  $ _G -> (_m1  _m2 
    

      
        
StepHypRefExpression

        

          1
          
          hyp _mh
          
_G -> _m1 = _m2

        

        

          2
          
          hyp _nh
          
_G -> _n1 = _n2

        

        

          3
          1, 2
          zsubeqd
          
_G -> _m1 -Z _n1 = _m2 -Z _n2

        

        

          4
          3
          oddeqd
          
_G -> (odd (_m1 -Z _n1) <-> odd (_m2 -Z _n2))

        

        

          5
          4
          conv zlt
          
_G -> (_m1 <Z _n1 <-> _m2 <Z _n2)

        

      
    

    
Axiom use

    axs_prop_calc
     (ax_1,
      ax_2,
      ax_3,
      ax_mp,
      itru),
    axs_pred_calc
     (ax_gen,
      ax_4,
      ax_5,
      ax_6,
      ax_7,
      ax_10,
      ax_11,
      ax_12),
    axs_set
     (elab,
      ax_8),
    axs_the
     (theid,
      the0),
    axs_peano
     (peano2,
      addeq,
      muleq)