Theorem zaddb0 ≪ | index | src | ≫ 

theorem zaddb0 (m n: nat): $ b0 m +Z b0 n = b0 (m + n) $;
StepHypRefExpression
1 eqtr 
b0 m +Z b0 n = m + n -ZN 0 -> m + n -ZN 0 = b0 (m + n) -> b0 m +Z b0 n = b0 (m + n)
2 znsubeq 
zfst (b0 m) + zfst (b0 n) = m + n -> zsnd (b0 m) + zsnd (b0 n) = 0 -> zfst (b0 m) + zfst (b0 n) -ZN (zsnd (b0 m) + zsnd (b0 n)) = m + n -ZN 0
3 2 conv zadd 
zfst (b0 m) + zfst (b0 n) = m + n -> zsnd (b0 m) + zsnd (b0 n) = 0 -> b0 m +Z b0 n = m + n -ZN 0
4 addeq 
zfst (b0 m) = m -> zfst (b0 n) = n -> zfst (b0 m) + zfst (b0 n) = m + n
5 zfstb0 
zfst (b0 m) = m
6 4, 5 ax_mp 
zfst (b0 n) = n -> zfst (b0 m) + zfst (b0 n) = m + n
7 zfstb0 
zfst (b0 n) = n
8 6, 7 ax_mp 
zfst (b0 m) + zfst (b0 n) = m + n
9 3, 8 ax_mp 
zsnd (b0 m) + zsnd (b0 n) = 0 -> b0 m +Z b0 n = m + n -ZN 0
10 eqtr 
zsnd (b0 m) + zsnd (b0 n) = 0 + 0 -> 0 + 0 = 0 -> zsnd (b0 m) + zsnd (b0 n) = 0
11 addeq 
zsnd (b0 m) = 0 -> zsnd (b0 n) = 0 -> zsnd (b0 m) + zsnd (b0 n) = 0 + 0
12 zsndb0 
zsnd (b0 m) = 0
13 11, 12 ax_mp 
zsnd (b0 n) = 0 -> zsnd (b0 m) + zsnd (b0 n) = 0 + 0
14 zsndb0 
zsnd (b0 n) = 0
15 13, 14 ax_mp 
zsnd (b0 m) + zsnd (b0 n) = 0 + 0
16 10, 15 ax_mp 
0 + 0 = 0 -> zsnd (b0 m) + zsnd (b0 n) = 0
17 add0 
0 + 0 = 0
18 16, 17 ax_mp 
zsnd (b0 m) + zsnd (b0 n) = 0
19 9, 18 ax_mp 
b0 m +Z b0 n = m + n -ZN 0
20 1, 19 ax_mp 
m + n -ZN 0 = b0 (m + n) -> b0 m +Z b0 n = b0 (m + n)
21 znsub02 
m + n -ZN 0 = b0 (m + n)
22 20, 21 ax_mp 
b0 m +Z b0 n = b0 (m + 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)