Theorem zltadd1 ≪ | index | src | ≫

theorem zltadd1 (a b c: nat): $ a  a +Z c 
    
      
        Step Hyp Ref Expression
        
          1
          
          oddeq
          a -Z b = a +Z c -Z (b +Z c) -> (odd (a -Z b) <-> odd (a +Z c -Z (b +Z c)))
        
        
          2
          1
          conv zlt
          a -Z b = a +Z c -Z (b +Z c) -> (a <Z b <-> a +Z c <Z b +Z c)
        
        
          3
          
          eqcom
          a +Z c -Z (b +Z c) = a -Z b -> a -Z b = a +Z c -Z (b +Z c)
        
        
          4
          
          zpnpcan1
          a +Z c -Z (b +Z c) = a -Z b
        
        
          5
          3, 4
          ax_mp
          a -Z b = a +Z c -Z (b +Z c)
        
        
          6
          2, 5
          ax_mp
          a <Z b <-> a +Z c <Z b +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)

Step	Hyp	Ref	Expression
1		oddeq	a -Z b = a +Z c -Z (b +Z c) -> (odd (a -Z b) <-> odd (a +Z c -Z (b +Z c)))
2	1	conv zlt	a -Z b = a +Z c -Z (b +Z c) -> (a <Z b <-> a +Z c <Z b +Z c)
3		eqcom	a +Z c -Z (b +Z c) = a -Z b -> a -Z b = a +Z c -Z (b +Z c)
4		zpnpcan1	a +Z c -Z (b +Z c) = a -Z b
5	3, 4	ax_mp	a -Z b = a +Z c -Z (b +Z c)
6	2, 5	ax_mp	a <Z b <-> a +Z c <Z b +Z c