Theorem zaddzn ≪ | index | src | ≫ 

theorem zaddzn (a b c d: nat): $ a -ZN c +Z (b -ZN d) = a + b -ZN (c + d) $;
StepHypRefExpression
1 zneqb 
zfst (a -ZN c) + zfst (b -ZN d) -ZN (zsnd (a -ZN c) + zsnd (b -ZN d)) = a + b -ZN (c + d) <->
  zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
2 1 conv zadd 
a -ZN c +Z (b -ZN d) = a + b -ZN (c + d) <-> zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
3 eqtr 
zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = zfst (a -ZN c) + c + (zfst (b -ZN d) + d) ->
  zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d)) ->
  zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
4 add4 
zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = zfst (a -ZN c) + c + (zfst (b -ZN d) + d)
5 3, 4 ax_mp 
zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d)) ->
  zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
6 eqtr 
zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + zsnd (a -ZN c) + (b + zsnd (b -ZN d)) ->
  a + zsnd (a -ZN c) + (b + zsnd (b -ZN d)) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d)) ->
  zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
7 addeq 
zfst (a -ZN c) + c = a + zsnd (a -ZN c) ->
  zfst (b -ZN d) + d = b + zsnd (b -ZN d) ->
  zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + zsnd (a -ZN c) + (b + zsnd (b -ZN d))
8 zneqb 
zfst (a -ZN c) -ZN zsnd (a -ZN c) = a -ZN c <-> zfst (a -ZN c) + c = a + zsnd (a -ZN c)
9 zfstsnd 
zfst (a -ZN c) -ZN zsnd (a -ZN c) = a -ZN c
10 8, 9 mpbi 
zfst (a -ZN c) + c = a + zsnd (a -ZN c)
11 7, 10 ax_mp 
zfst (b -ZN d) + d = b + zsnd (b -ZN d) -> zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + zsnd (a -ZN c) + (b + zsnd (b -ZN d))
12 zneqb 
zfst (b -ZN d) -ZN zsnd (b -ZN d) = b -ZN d <-> zfst (b -ZN d) + d = b + zsnd (b -ZN d)
13 zfstsnd 
zfst (b -ZN d) -ZN zsnd (b -ZN d) = b -ZN d
14 12, 13 mpbi 
zfst (b -ZN d) + d = b + zsnd (b -ZN d)
15 11, 14 ax_mp 
zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + zsnd (a -ZN c) + (b + zsnd (b -ZN d))
16 6, 15 ax_mp 
a + zsnd (a -ZN c) + (b + zsnd (b -ZN d)) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d)) ->
  zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
17 add4 
a + zsnd (a -ZN c) + (b + zsnd (b -ZN d)) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
18 16, 17 ax_mp 
zfst (a -ZN c) + c + (zfst (b -ZN d) + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
19 5, 18 ax_mp 
zfst (a -ZN c) + zfst (b -ZN d) + (c + d) = a + b + (zsnd (a -ZN c) + zsnd (b -ZN d))
20 2, 19 mpbir 
a -ZN c +Z (b -ZN d) = a + b -ZN (c + d)

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)