Theorem zmuladd ≪ | index | src | ≫ 

theorem zmuladd (a b c: nat): $ a *Z (b +Z c) = a *Z b +Z a *Z c $;
StepHypRefExpression
1 eqtr3 
(zfst a -ZN zsnd a) *Z (b +Z c) = a *Z (b +Z c) -> (zfst a -ZN zsnd a) *Z (b +Z c) = a *Z b +Z a *Z c -> a *Z (b +Z c) = a *Z b +Z a *Z c
2 zmuleq1 
zfst a -ZN zsnd a = a -> (zfst a -ZN zsnd a) *Z (b +Z c) = a *Z (b +Z c)
3 zfstsnd 
zfst a -ZN zsnd a = a
4 2, 3 ax_mp 
(zfst a -ZN zsnd a) *Z (b +Z c) = a *Z (b +Z c)
5 1, 4 ax_mp 
(zfst a -ZN zsnd a) *Z (b +Z c) = a *Z b +Z a *Z c -> a *Z (b +Z c) = a *Z b +Z a *Z c
6 eqcom 
a *Z b +Z a *Z c = (zfst a -ZN zsnd a) *Z (b +Z c) -> (zfst a -ZN zsnd a) *Z (b +Z c) = a *Z b +Z a *Z c
7 eqtr4 
a *Z b +Z a *Z c =
    zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) ->
  (zfst a -ZN zsnd a) *Z (b +Z c) =
    zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) ->
  a *Z b +Z a *Z c = (zfst a -ZN zsnd a) *Z (b +Z c)
8 zaddzn 
zfst a * zfst b + zsnd a * zsnd b -ZN (zfst a * zsnd b + zsnd a * zfst b) +Z (zfst a * zfst c + zsnd a * zsnd c -ZN (zfst a * zsnd c + zsnd a * zfst c)) =
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c))
9 8 conv zmul 
a *Z b +Z a *Z c =
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c))
10 7, 9 ax_mp 
(zfst a -ZN zsnd a) *Z (b +Z c) =
    zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) ->
  a *Z b +Z a *Z c = (zfst a -ZN zsnd a) *Z (b +Z c)
11 eqtr4 
(zfst a -ZN zsnd a) *Z (b +Z c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a) ->
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) =
    zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a) ->
  (zfst a -ZN zsnd a) *Z (b +Z c) =
    zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c))
12 zmulzn 
(zfst a -ZN zsnd a) *Z (zfst b + zfst c -ZN (zsnd b + zsnd c)) =
  zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a)
13 12 conv zadd 
(zfst a -ZN zsnd a) *Z (b +Z c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a)
14 11, 13 ax_mp 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) =
    zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a) ->
  (zfst a -ZN zsnd a) *Z (b +Z c) =
    zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c))
15 znsubeq 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) ->
  zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a ->
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) =
    zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a)
16 eqtr4 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c) ->
  zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c) ->
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c)
17 add4 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c)
18 16, 17 ax_mp 
zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c) ->
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c)
19 addeq 
zfst a * (zfst b + zfst c) = zfst a * zfst b + zfst a * zfst c ->
  zsnd a * (zsnd b + zsnd c) = zsnd a * zsnd b + zsnd a * zsnd c ->
  zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c)
20 muladd 
zfst a * (zfst b + zfst c) = zfst a * zfst b + zfst a * zfst c
21 19, 20 ax_mp 
zsnd a * (zsnd b + zsnd c) = zsnd a * zsnd b + zsnd a * zsnd c ->
  zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c)
22 muladd 
zsnd a * (zsnd b + zsnd c) = zsnd a * zsnd b + zsnd a * zsnd c
23 21, 22 ax_mp 
zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) = zfst a * zfst b + zfst a * zfst c + (zsnd a * zsnd b + zsnd a * zsnd c)
24 18, 23 ax_mp 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) = zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c)
25 15, 24 ax_mp 
zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a ->
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) =
    zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a)
26 eqtr4 
zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c) ->
  zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c) ->
  zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a
27 add4 
zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c)
28 26, 27 ax_mp 
zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c) ->
  zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a
29 addeq 
zfst a * (zsnd b + zsnd c) = zfst a * zsnd b + zfst a * zsnd c ->
  (zfst b + zfst c) * zsnd a = zsnd a * zfst b + zsnd a * zfst c ->
  zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c)
30 muladd 
zfst a * (zsnd b + zsnd c) = zfst a * zsnd b + zfst a * zsnd c
31 29, 30 ax_mp 
(zfst b + zfst c) * zsnd a = zsnd a * zfst b + zsnd a * zfst c ->
  zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c)
32 eqtr 
(zfst b + zfst c) * zsnd a = zsnd a * (zfst b + zfst c) ->
  zsnd a * (zfst b + zfst c) = zsnd a * zfst b + zsnd a * zfst c ->
  (zfst b + zfst c) * zsnd a = zsnd a * zfst b + zsnd a * zfst c
33 mulcom 
(zfst b + zfst c) * zsnd a = zsnd a * (zfst b + zfst c)
34 32, 33 ax_mp 
zsnd a * (zfst b + zfst c) = zsnd a * zfst b + zsnd a * zfst c -> (zfst b + zfst c) * zsnd a = zsnd a * zfst b + zsnd a * zfst c
35 muladd 
zsnd a * (zfst b + zfst c) = zsnd a * zfst b + zsnd a * zfst c
36 34, 35 ax_mp 
(zfst b + zfst c) * zsnd a = zsnd a * zfst b + zsnd a * zfst c
37 31, 36 ax_mp 
zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a = zfst a * zsnd b + zfst a * zsnd c + (zsnd a * zfst b + zsnd a * zfst c)
38 28, 37 ax_mp 
zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c) = zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a
39 25, 38 ax_mp 
zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c)) =
  zfst a * (zfst b + zfst c) + zsnd a * (zsnd b + zsnd c) -ZN (zfst a * (zsnd b + zsnd c) + (zfst b + zfst c) * zsnd a)
40 14, 39 ax_mp 
(zfst a -ZN zsnd a) *Z (b +Z c) =
  zfst a * zfst b + zsnd a * zsnd b + (zfst a * zfst c + zsnd a * zsnd c) -ZN (zfst a * zsnd b + zsnd a * zfst b + (zfst a * zsnd c + zsnd a * zfst c))
41 10, 40 ax_mp 
a *Z b +Z a *Z c = (zfst a -ZN zsnd a) *Z (b +Z c)
42 6, 41 ax_mp 
(zfst a -ZN zsnd a) *Z (b +Z c) = a *Z b +Z a *Z c
43 5, 42 ax_mp 
a *Z (b +Z c) = a *Z b +Z a *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)