Theorem zltsubadd ≪ | index | src | ≫

theorem zltsubadd (a b c: nat): $ a -Z b  a 
    

      

        
Step
Hyp
Ref
Expression
        

          
1
          

          
bitr2
          
(a <Z c +Z b <-> a +Z -uZ b <Z c +Z b +Z -uZ b) -> (a +Z -uZ b <Z c +Z b +Z -uZ b <-> a -Z b <Z c) -> (a -Z b <Z c <-> a <Z c +Z b)
        
        

          
2
          

          
zltadd1
          
a <Z c +Z b <-> a +Z -uZ b <Z c +Z b +Z -uZ b
        
        

          
3
          
2
          
bitr2*
          
(a +Z -uZ b <Z c +Z b +Z -uZ b <-> a -Z b <Z c) -> (a -Z b <Z c <-> a <Z c +Z b)
        
        

          
4
          

          
zlteq2
          
c +Z b +Z -uZ b = c -> (a +Z -uZ b <Z c +Z b +Z -uZ b <-> a +Z -uZ b <Z c)
        
        

          
5
          
4
          
conv zsub
          
c +Z b +Z -uZ b = c -> (a +Z -uZ b <Z c +Z b +Z -uZ b <-> a -Z b <Z c)
        
        

          
6
          

          
zpncan
          
c +Z b -Z b = c
        
        

          
7
          
6
          
conv zsub
          
c +Z b +Z -uZ b = c
        
        

          
8
          
5, 7
          
ax_mp
          
a +Z -uZ b <Z c +Z b +Z -uZ b <-> a -Z b <Z c
        
        

          
9
          
2, 8
          
bitr2*
          
a -Z b <Z c <-> a <Z c +Z b
        
      
    
    
Axiom use
    axs_prop_calc (+5)
     (ax_1,
      ax_2,
      ax_3,
      ax_mp,
      itru),
    axs_pred_calc (+8)
     (ax_gen,
      ax_4,
      ax_5,
      ax_6,
      ax_7,
      ax_10,
      ax_11,
      ax_12),
    axs_set (+2)
     (elab,
      ax_8),
    axs_the (+2)
     (theid,
      the0),
    axs_peano (+9)
     (peano1,
      peano2,
      peano5,
      addeq,
      muleq,
      add0,
      addS,
      mul0,
      mulS)