Theorem zltsub0 ≪ | index | src | ≫ 

theorem zltsub0 (a b: nat): $ a -Z b  a 
    

      
        
StepHypRefExpression

        

          1
          
          bitr3
          
(0 <Z -uZ (a -Z b) <-> a -Z b <Z 0) -> (0 <Z -uZ (a -Z b) <-> a <Z b) -> (a -Z b <Z 0 <-> a <Z b)

        

        

          2
          
          zlt0neg
          
0 <Z -uZ (a -Z b) <-> a -Z b <Z 0

        

        

          3
          1, 2
          ax_mp
          
(0 <Z -uZ (a -Z b) <-> a <Z b) -> (a -Z b <Z 0 <-> a <Z b)

        

        

          4
          
          bitr
          
(0 <Z -uZ (a -Z b) <-> 0 <Z b -Z a) -> (0 <Z b -Z a <-> a <Z b) -> (0 <Z -uZ (a -Z b) <-> a <Z b)

        

        

          5
          
          zlteq2
          
-uZ (a -Z b) = b -Z a -> (0 <Z -uZ (a -Z b) <-> 0 <Z b -Z a)

        

        

          6
          
          znegsub
          
-uZ (a -Z b) = b -Z a

        

        

          7
          5, 6
          ax_mp
          
0 <Z -uZ (a -Z b) <-> 0 <Z b -Z a

        

        

          8
          4, 7
          ax_mp
          
(0 <Z b -Z a <-> a <Z b) -> (0 <Z -uZ (a -Z b) <-> a <Z b)

        

        

          9
          
          zlt0sub
          
0 <Z b -Z a <-> a <Z b

        

        

          10
          8, 9
          ax_mp
          
0 <Z -uZ (a -Z b) <-> a <Z b

        

        

          11
          3, 10
          ax_mp
          
a -Z b <Z 0 <-> a <Z b

        

      
    

    
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)