Theorem zaddass ≪ | index | src | ≫ 

theorem zaddass (a b c: nat): $ a +Z b +Z c = a +Z (b +Z c) $;
StepHypRefExpression
1 eqtr3 
a +Z b +Z (zfst c -ZN zsnd c) = a +Z b +Z c -> a +Z b +Z (zfst c -ZN zsnd c) = a +Z (b +Z c) -> a +Z b +Z c = a +Z (b +Z c)
2 zaddeq2 
zfst c -ZN zsnd c = c -> a +Z b +Z (zfst c -ZN zsnd c) = a +Z b +Z c
3 zfstsnd 
zfst c -ZN zsnd c = c
4 2, 3 ax_mp 
a +Z b +Z (zfst c -ZN zsnd c) = a +Z b +Z c
5 1, 4 ax_mp 
a +Z b +Z (zfst c -ZN zsnd c) = a +Z (b +Z c) -> a +Z b +Z c = a +Z (b +Z c)
6 eqtr4 
a +Z b +Z (zfst c -ZN zsnd c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) ->
  a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) ->
  a +Z b +Z (zfst c -ZN zsnd c) = a +Z (b +Z c)
7 zaddzn 
zfst a + zfst b -ZN (zsnd a + zsnd b) +Z (zfst c -ZN zsnd c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
8 7 conv zadd 
a +Z b +Z (zfst c -ZN zsnd c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
9 6, 8 ax_mp 
a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) -> a +Z b +Z (zfst c -ZN zsnd c) = a +Z (b +Z c)
10 eqtr3 
zfst a -ZN zsnd a +Z (b +Z c) = a +Z (b +Z c) ->
  zfst a -ZN zsnd a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) ->
  a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
11 zaddeq1 
zfst a -ZN zsnd a = a -> zfst a -ZN zsnd a +Z (b +Z c) = a +Z (b +Z c)
12 zfstsnd 
zfst a -ZN zsnd a = a
13 11, 12 ax_mp 
zfst a -ZN zsnd a +Z (b +Z c) = a +Z (b +Z c)
14 10, 13 ax_mp 
zfst a -ZN zsnd a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) ->
  a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
15 eqtr4 
zfst a -ZN zsnd a +Z (b +Z c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c)) ->
  zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c)) ->
  zfst a -ZN zsnd a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
16 zaddzn 
zfst a -ZN zsnd a +Z (zfst b + zfst c -ZN (zsnd b + zsnd c)) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c))
17 16 conv zadd 
zfst a -ZN zsnd a +Z (b +Z c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c))
18 15, 17 ax_mp 
zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c)) ->
  zfst a -ZN zsnd a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
19 znsubeq 
zfst a + zfst b + zfst c = zfst a + (zfst b + zfst c) ->
  zsnd a + zsnd b + zsnd c = zsnd a + (zsnd b + zsnd c) ->
  zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c))
20 addass 
zfst a + zfst b + zfst c = zfst a + (zfst b + zfst c)
21 19, 20 ax_mp 
zsnd a + zsnd b + zsnd c = zsnd a + (zsnd b + zsnd c) ->
  zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c))
22 addass 
zsnd a + zsnd b + zsnd c = zsnd a + (zsnd b + zsnd c)
23 21, 22 ax_mp 
zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c) = zfst a + (zfst b + zfst c) -ZN (zsnd a + (zsnd b + zsnd c))
24 18, 23 ax_mp 
zfst a -ZN zsnd a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
25 14, 24 ax_mp 
a +Z (b +Z c) = zfst a + zfst b + zfst c -ZN (zsnd a + zsnd b + zsnd c)
26 9, 25 ax_mp 
a +Z b +Z (zfst c -ZN zsnd c) = a +Z (b +Z c)
27 5, 26 ax_mp 
a +Z b +Z c = a +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)