Theorem zmulass ≪ | index | src | ≫ 

theorem zmulass (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 zmuleq2 
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 eqcom 
a *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c) -> a *Z b *Z (zfst c -ZN zsnd c) = a *Z (b *Z c)
7 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 (zfst c -ZN zsnd c) ->
  a *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
8 zmuleq1 
zfst a -ZN zsnd a = a -> (zfst a -ZN zsnd a) *Z (b *Z c) = a *Z (b *Z c)
9 zfstsnd 
zfst a -ZN zsnd a = a
10 8, 9 ax_mp 
(zfst a -ZN zsnd a) *Z (b *Z c) = a *Z (b *Z c)
11 7, 10 ax_mp 
(zfst a -ZN zsnd a) *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c) -> a *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
12 eqtr4 
(zfst a -ZN zsnd a) *Z (b *Z c) =
    zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) ->
  a *Z b *Z (zfst c -ZN zsnd c) =
    zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) ->
  (zfst a -ZN zsnd a) *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
13 zmulzn 
(zfst a -ZN zsnd a) *Z (zfst b * zfst c + zsnd b * zsnd c -ZN (zfst b * zsnd c + zsnd b * zfst c)) =
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
    (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a)
14 13 conv zmul 
(zfst a -ZN zsnd a) *Z (b *Z c) =
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
    (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a)
15 12, 14 ax_mp 
a *Z b *Z (zfst c -ZN zsnd c) =
    zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) ->
  (zfst a -ZN zsnd a) *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
16 eqtr4 
a *Z b *Z (zfst c -ZN zsnd c) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
      ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
      ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)) ->
  a *Z b *Z (zfst c -ZN zsnd c) =
    zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a)
17 zmulzn 
(zfst a * zfst b + zsnd a * zsnd b -ZN (zfst a * zsnd b + zsnd a * zfst b)) *Z (zfst c -ZN zsnd c) =
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
    ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b))
18 17 conv zmul 
a *Z b *Z (zfst c -ZN zsnd c) =
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
    ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b))
19 16, 18 ax_mp 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
      ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)) ->
  a *Z b *Z (zfst c -ZN zsnd c) =
    zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a)
20 znsubeq 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c ->
  zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
      ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b))
21 eqtr4 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c
22 addeq 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) = zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) ->
  zsnd a * (zfst b * zsnd c + zsnd b * zfst c) = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
23 muladd 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) = zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c)
24 22, 23 ax_mp 
zsnd a * (zfst b * zsnd c + zsnd b * zfst c) = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
25 muladd 
zsnd a * (zfst b * zsnd c + zsnd b * zfst c) = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
26 24, 25 ax_mp 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
  zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
27 21, 26 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c
28 eqtr4 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) ->
  zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
29 addeq 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c = zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c ->
  (zfst a * zsnd b + zsnd a * zfst b) * zsnd c = zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c ->
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
30 addmul 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c = zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c
31 29, 30 ax_mp 
(zfst a * zsnd b + zsnd a * zfst b) * zsnd c = zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c ->
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
32 addmul 
(zfst a * zsnd b + zsnd a * zfst b) * zsnd c = zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c
33 31, 32 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
  zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
34 28, 33 ax_mp 
zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
    zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
35 eqtr4 
zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) ->
  zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) ->
  zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
36 addass 
zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
  zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
37 35, 36 ax_mp 
zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) ->
  zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
    zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
38 eqtr4 
zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) ->
  zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) =
    zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) ->
  zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
39 addass 
zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
  zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c))
40 38, 39 ax_mp 
zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) =
    zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) ->
  zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
41 eqcom 
zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) ->
  zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) =
    zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c))
42 addeq 
zfst a * zfst b * zfst c = zfst a * (zfst b * zfst c) ->
  zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
43 mulass 
zfst a * zfst b * zfst c = zfst a * (zfst b * zfst c)
44 42, 43 ax_mp 
zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) =
    zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
45 eqtr 
zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) ->
  zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
46 addlass 
zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
  zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c)
47 45, 46 ax_mp 
zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) ->
  zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
48 addeq 
zfst a * zsnd b * zsnd c = zfst a * (zsnd b * zsnd c) ->
  zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
49 mulass 
zfst a * zsnd b * zsnd c = zfst a * (zsnd b * zsnd c)
50 48, 49 ax_mp 
zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) =
    zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
51 eqtr 
zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c ->
  zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
52 addcom 
zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c
53 51, 52 ax_mp 
zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c) ->
  zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
54 addeq 
zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) ->
  zsnd a * zsnd b * zfst c = zsnd a * (zsnd b * zfst c) ->
  zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
55 mulass 
zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c)
56 54, 55 ax_mp 
zsnd a * zsnd b * zfst c = zsnd a * (zsnd b * zfst c) ->
  zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
57 mulass 
zsnd a * zsnd b * zfst c = zsnd a * (zsnd b * zfst c)
58 56, 57 ax_mp 
zsnd a * zfst b * zsnd c + zsnd a * zsnd b * zfst c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
59 53, 58 ax_mp 
zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c = zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)
60 50, 59 ax_mp 
zfst a * zsnd b * zsnd c + (zsnd a * zsnd b * zfst c + zsnd a * zfst b * zsnd c) =
  zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
61 47, 60 ax_mp 
zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
  zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
62 44, 61 ax_mp 
zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)) =
  zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
63 41, 62 ax_mp 
zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))) =
  zfst a * zfst b * zfst c + (zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c))
64 40, 63 ax_mp 
zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c) =
  zfst a * (zfst b * zfst c) + (zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)))
65 37, 64 ax_mp 
zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c)) =
  zfst a * zfst b * zfst c + zsnd a * zsnd b * zfst c + (zfst a * zsnd b * zsnd c + zsnd a * zfst b * zsnd c)
66 34, 65 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c =
  zfst a * (zfst b * zfst c) + zfst a * (zsnd b * zsnd c) + (zsnd a * (zfst b * zsnd c) + zsnd a * (zsnd b * zfst c))
67 27, 66 ax_mp 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) =
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c
68 20, 67 ax_mp 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) ->
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
      (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) =
    (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
      ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b))
69 eqtr4 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)
70 addeq 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) = zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) ->
  (zfst b * zfst c + zsnd b * zsnd c) * zsnd a = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
71 muladd 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) = zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c)
72 70, 71 ax_mp 
(zfst b * zfst c + zsnd b * zsnd c) * zsnd a = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
73 addmul 
(zfst b * zfst c + zsnd b * zsnd c) * zsnd a = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
74 72, 73 ax_mp 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
  zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
75 69, 74 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
    (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)
76 eqtr4 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) ->
  zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
77 addeq 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c = zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c ->
  zfst c * (zfst a * zsnd b + zsnd a * zfst b) = zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
78 addmul 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c = zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c
79 77, 78 ax_mp 
zfst c * (zfst a * zsnd b + zsnd a * zfst b) = zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
80 muladd 
zfst c * (zfst a * zsnd b + zsnd a * zfst b) = zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)
81 79, 80 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
  zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
82 76, 81 ax_mp 
zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) ->
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
    zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
83 eqtr4 
zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) ->
  zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) ->
  zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
84 addass 
zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
  zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
85 83, 84 ax_mp 
zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) ->
  zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
    zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
86 eqtr4 
zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) ->
  zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) =
    zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) ->
  zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
87 addass 
zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
  zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)))
88 86, 87 ax_mp 
zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) =
    zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) ->
  zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
89 eqcom 
zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) ->
  zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) =
    zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)))
90 addeq 
zfst a * zfst b * zsnd c = zfst a * (zfst b * zsnd c) ->
  zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
91 mulass 
zfst a * zfst b * zsnd c = zfst a * (zfst b * zsnd c)
92 90, 91 ax_mp 
zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) =
    zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
93 eqtr 
zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) ->
  zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
94 addlass 
zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
  zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b))
95 93, 94 ax_mp 
zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) ->
  zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
96 addeq 
zfst c * (zfst a * zsnd b) = zfst a * (zsnd b * zfst c) ->
  zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
97 eqtr 
zfst c * (zfst a * zsnd b) = zfst a * zsnd b * zfst c ->
  zfst a * zsnd b * zfst c = zfst a * (zsnd b * zfst c) ->
  zfst c * (zfst a * zsnd b) = zfst a * (zsnd b * zfst c)
98 mulcom 
zfst c * (zfst a * zsnd b) = zfst a * zsnd b * zfst c
99 97, 98 ax_mp 
zfst a * zsnd b * zfst c = zfst a * (zsnd b * zfst c) -> zfst c * (zfst a * zsnd b) = zfst a * (zsnd b * zfst c)
100 mulass 
zfst a * zsnd b * zfst c = zfst a * (zsnd b * zfst c)
101 99, 100 ax_mp 
zfst c * (zfst a * zsnd b) = zfst a * (zsnd b * zfst c)
102 96, 101 ax_mp 
zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) =
    zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
103 eqtr 
zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c ->
  zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
104 addcom 
zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c
105 103, 104 ax_mp 
zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a ->
  zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
106 addeq 
zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a ->
  zsnd a * zsnd b * zsnd c = zsnd b * zsnd c * zsnd a ->
  zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
107 eqtr3 
zfst c * zsnd a * zfst b = zfst c * (zsnd a * zfst b) ->
  zfst c * zsnd a * zfst b = zfst b * zfst c * zsnd a ->
  zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a
108 mulass 
zfst c * zsnd a * zfst b = zfst c * (zsnd a * zfst b)
109 107, 108 ax_mp 
zfst c * zsnd a * zfst b = zfst b * zfst c * zsnd a -> zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a
110 eqtr 
zfst c * zsnd a * zfst b = zfst c * zfst b * zsnd a ->
  zfst c * zfst b * zsnd a = zfst b * zfst c * zsnd a ->
  zfst c * zsnd a * zfst b = zfst b * zfst c * zsnd a
111 mulrass 
zfst c * zsnd a * zfst b = zfst c * zfst b * zsnd a
112 110, 111 ax_mp 
zfst c * zfst b * zsnd a = zfst b * zfst c * zsnd a -> zfst c * zsnd a * zfst b = zfst b * zfst c * zsnd a
113 muleq1 
zfst c * zfst b = zfst b * zfst c -> zfst c * zfst b * zsnd a = zfst b * zfst c * zsnd a
114 mulcom 
zfst c * zfst b = zfst b * zfst c
115 113, 114 ax_mp 
zfst c * zfst b * zsnd a = zfst b * zfst c * zsnd a
116 112, 115 ax_mp 
zfst c * zsnd a * zfst b = zfst b * zfst c * zsnd a
117 109, 116 ax_mp 
zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a
118 106, 117 ax_mp 
zsnd a * zsnd b * zsnd c = zsnd b * zsnd c * zsnd a ->
  zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
119 eqtr 
zsnd a * zsnd b * zsnd c = zsnd b * zsnd a * zsnd c ->
  zsnd b * zsnd a * zsnd c = zsnd b * zsnd c * zsnd a ->
  zsnd a * zsnd b * zsnd c = zsnd b * zsnd c * zsnd a
120 muleq1 
zsnd a * zsnd b = zsnd b * zsnd a -> zsnd a * zsnd b * zsnd c = zsnd b * zsnd a * zsnd c
121 mulcom 
zsnd a * zsnd b = zsnd b * zsnd a
122 120, 121 ax_mp 
zsnd a * zsnd b * zsnd c = zsnd b * zsnd a * zsnd c
123 119, 122 ax_mp 
zsnd b * zsnd a * zsnd c = zsnd b * zsnd c * zsnd a -> zsnd a * zsnd b * zsnd c = zsnd b * zsnd c * zsnd a
124 mulrass 
zsnd b * zsnd a * zsnd c = zsnd b * zsnd c * zsnd a
125 123, 124 ax_mp 
zsnd a * zsnd b * zsnd c = zsnd b * zsnd c * zsnd a
126 118, 125 ax_mp 
zfst c * (zsnd a * zfst b) + zsnd a * zsnd b * zsnd c = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
127 105, 126 ax_mp 
zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b) = zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a
128 102, 127 ax_mp 
zfst c * (zfst a * zsnd b) + (zsnd a * zsnd b * zsnd c + zfst c * (zsnd a * zfst b)) =
  zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
129 95, 128 ax_mp 
zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
  zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
130 92, 129 ax_mp 
zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))) =
  zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
131 89, 130 ax_mp 
zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)) =
  zfst a * zfst b * zsnd c + (zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)))
132 88, 131 ax_mp 
zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b)) =
  zfst a * (zfst b * zsnd c) + (zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a))
133 85, 132 ax_mp 
zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a) =
  zfst a * zfst b * zsnd c + zsnd a * zsnd b * zsnd c + (zfst c * (zfst a * zsnd b) + zfst c * (zsnd a * zfst b))
134 82, 133 ax_mp 
(zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b) =
  zfst a * (zfst b * zsnd c) + zfst a * (zsnd b * zfst c) + (zfst b * zfst c * zsnd a + zsnd b * zsnd c * zsnd a)
135 75, 134 ax_mp 
zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a =
  (zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b)
136 68, 135 ax_mp 
zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
    (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a) =
  (zfst a * zfst b + zsnd a * zsnd b) * zfst c + (zfst a * zsnd b + zsnd a * zfst b) * zsnd c -ZN
    ((zfst a * zfst b + zsnd a * zsnd b) * zsnd c + zfst c * (zfst a * zsnd b + zsnd a * zfst b))
137 19, 136 ax_mp 
a *Z b *Z (zfst c -ZN zsnd c) =
  zfst a * (zfst b * zfst c + zsnd b * zsnd c) + zsnd a * (zfst b * zsnd c + zsnd b * zfst c) -ZN
    (zfst a * (zfst b * zsnd c + zsnd b * zfst c) + (zfst b * zfst c + zsnd b * zsnd c) * zsnd a)
138 15, 137 ax_mp 
(zfst a -ZN zsnd a) *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
139 11, 138 ax_mp 
a *Z (b *Z c) = a *Z b *Z (zfst c -ZN zsnd c)
140 6, 139 ax_mp 
a *Z b *Z (zfst c -ZN zsnd c) = a *Z (b *Z c)
141 5, 140 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)