Theorem zltadd2 ≪ | index | src | ≫ 

theorem zltadd2 (a b c: nat): $ b  a +Z b 
    

      
        
StepHypRefExpression

        

          1
          
          oddeq
          
b -Z c = a +Z b -Z (a +Z c) -> (odd (b -Z c) <-> odd (a +Z b -Z (a +Z c)))

        

        

          2
          1
          conv zlt
          
b -Z c = a +Z b -Z (a +Z c) -> (b <Z c <-> a +Z b <Z a +Z c)

        

        

          3
          
          eqcom
          
a +Z b -Z (a +Z c) = b -Z c -> b -Z c = a +Z b -Z (a +Z c)

        

        

          4
          
          zpnpcan2
          
a +Z b -Z (a +Z c) = b -Z c

        

        

          5
          3, 4
          ax_mp
          
b -Z c = a +Z b -Z (a +Z c)

        

        

          6
          2, 5
          ax_mp
          
b <Z c <-> a +Z b <Z a +Z c

        

      
    

    
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
     (peano1,
      peano2,
      peano5,
      addeq,
      muleq,
      add0,
      addS,
      mul0,
      mulS)