Theorem zsubb0 ≪ | index | src | ≫ 

theorem zsubb0 (m n: nat): $ b0 m -Z b0 n = m -ZN n $;
StepHypRefExpression
1 eqtr3 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = b0 m -Z b0 n -> zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = m -ZN n -> b0 m -Z b0 n = m -ZN n
2 zsubeq1 
zfst (b0 m) -ZN zsnd (b0 m) = b0 m -> zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = b0 m -Z b0 n
3 zfstsnd 
zfst (b0 m) -ZN zsnd (b0 m) = b0 m
4 2, 3 ax_mp 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = b0 m -Z b0 n
5 1, 4 ax_mp 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = m -ZN n -> b0 m -Z b0 n = m -ZN n
6 eqtr 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) ->
  zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) = m -ZN n ->
  zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = m -ZN n
7 zaddzn 
zfst (b0 m) -ZN zsnd (b0 m) +Z (zsnd (b0 n) -ZN zfst (b0 n)) = zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n))
8 7 conv zneg, zsub 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n))
9 6, 8 ax_mp 
zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) = m -ZN n -> zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = m -ZN n
10 znsubeq 
zfst (b0 m) + zsnd (b0 n) = m -> zsnd (b0 m) + zfst (b0 n) = n -> zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) = m -ZN n
11 eqtr 
zfst (b0 m) + zsnd (b0 n) = m + 0 -> m + 0 = m -> zfst (b0 m) + zsnd (b0 n) = m
12 addeq 
zfst (b0 m) = m -> zsnd (b0 n) = 0 -> zfst (b0 m) + zsnd (b0 n) = m + 0
13 zfstb0 
zfst (b0 m) = m
14 12, 13 ax_mp 
zsnd (b0 n) = 0 -> zfst (b0 m) + zsnd (b0 n) = m + 0
15 zsndb0 
zsnd (b0 n) = 0
16 14, 15 ax_mp 
zfst (b0 m) + zsnd (b0 n) = m + 0
17 11, 16 ax_mp 
m + 0 = m -> zfst (b0 m) + zsnd (b0 n) = m
18 add0 
m + 0 = m
19 17, 18 ax_mp 
zfst (b0 m) + zsnd (b0 n) = m
20 10, 19 ax_mp 
zsnd (b0 m) + zfst (b0 n) = n -> zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) = m -ZN n
21 eqtr 
zsnd (b0 m) + zfst (b0 n) = 0 + n -> 0 + n = n -> zsnd (b0 m) + zfst (b0 n) = n
22 addeq 
zsnd (b0 m) = 0 -> zfst (b0 n) = n -> zsnd (b0 m) + zfst (b0 n) = 0 + n
23 zsndb0 
zsnd (b0 m) = 0
24 22, 23 ax_mp 
zfst (b0 n) = n -> zsnd (b0 m) + zfst (b0 n) = 0 + n
25 zfstb0 
zfst (b0 n) = n
26 24, 25 ax_mp 
zsnd (b0 m) + zfst (b0 n) = 0 + n
27 21, 26 ax_mp 
0 + n = n -> zsnd (b0 m) + zfst (b0 n) = n
28 add01 
0 + n = n
29 27, 28 ax_mp 
zsnd (b0 m) + zfst (b0 n) = n
30 20, 29 ax_mp 
zfst (b0 m) + zsnd (b0 n) -ZN (zsnd (b0 m) + zfst (b0 n)) = m -ZN n
31 9, 30 ax_mp 
zfst (b0 m) -ZN zsnd (b0 m) -Z b0 n = m -ZN n
32 5, 31 ax_mp 
b0 m -Z b0 n = m -ZN n

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)