Theorem zmulznlem ≪ | index | src | ≫ 

theorem zmulznlem (a1 b1 c1 d1 a2 b2 c2 d2: nat):
  $ a1 + c2 = a2 + c1 $ >
  $ b1 + d2 = b2 + d1 $ >
  $ a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) =
    a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) $;
StepHypRefExpression
1 eqtr 
a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) = a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) ->
  a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
2 add4 
a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) = a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)
3 1, 2 ax_mp 
a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
4 eqtr 
a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) ->
  a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
5 addcan2 
b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) <->
  a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)
6 eqtr3 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)) ->
  b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
7 addass 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2))
8 6, 7 ax_mp 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
9 eqtr 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) ->
  a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
10 addeq1 
b1 * c2 + (a1 * b1 + a2 * d2) = a2 * b2 + c1 * b1 + a2 * d1 ->
  b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2)
11 eqtr 
b1 * c2 + (a1 * b1 + a2 * d2) = a1 * b1 + a2 * d2 + b1 * c2 ->
  a1 * b1 + a2 * d2 + b1 * c2 = a2 * b2 + c1 * b1 + a2 * d1 ->
  b1 * c2 + (a1 * b1 + a2 * d2) = a2 * b2 + c1 * b1 + a2 * d1
12 addcom 
b1 * c2 + (a1 * b1 + a2 * d2) = a1 * b1 + a2 * d2 + b1 * c2
13 11, 12 ax_mp 
a1 * b1 + a2 * d2 + b1 * c2 = a2 * b2 + c1 * b1 + a2 * d1 -> b1 * c2 + (a1 * b1 + a2 * d2) = a2 * b2 + c1 * b1 + a2 * d1
14 eqtr 
a1 * b1 + a2 * d2 + b1 * c2 = a1 * b1 + b1 * c2 + a2 * d2 ->
  a1 * b1 + b1 * c2 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1 ->
  a1 * b1 + a2 * d2 + b1 * c2 = a2 * b2 + c1 * b1 + a2 * d1
15 addrass 
a1 * b1 + a2 * d2 + b1 * c2 = a1 * b1 + b1 * c2 + a2 * d2
16 14, 15 ax_mp 
a1 * b1 + b1 * c2 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1 -> a1 * b1 + a2 * d2 + b1 * c2 = a2 * b2 + c1 * b1 + a2 * d1
17 eqtr 
a1 * b1 + b1 * c2 + a2 * d2 = a2 * b1 + c1 * b1 + a2 * d2 ->
  a2 * b1 + c1 * b1 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1 ->
  a1 * b1 + b1 * c2 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
18 addeq1 
a1 * b1 + b1 * c2 = a2 * b1 + c1 * b1 -> a1 * b1 + b1 * c2 + a2 * d2 = a2 * b1 + c1 * b1 + a2 * d2
19 eqtr 
a1 * b1 + b1 * c2 = a1 * b1 + c2 * b1 -> a1 * b1 + c2 * b1 = a2 * b1 + c1 * b1 -> a1 * b1 + b1 * c2 = a2 * b1 + c1 * b1
20 addeq2 
b1 * c2 = c2 * b1 -> a1 * b1 + b1 * c2 = a1 * b1 + c2 * b1
21 mulcom 
b1 * c2 = c2 * b1
22 20, 21 ax_mp 
a1 * b1 + b1 * c2 = a1 * b1 + c2 * b1
23 19, 22 ax_mp 
a1 * b1 + c2 * b1 = a2 * b1 + c1 * b1 -> a1 * b1 + b1 * c2 = a2 * b1 + c1 * b1
24 eqtr3 
(a1 + c2) * b1 = a1 * b1 + c2 * b1 -> (a1 + c2) * b1 = a2 * b1 + c1 * b1 -> a1 * b1 + c2 * b1 = a2 * b1 + c1 * b1
25 addmul 
(a1 + c2) * b1 = a1 * b1 + c2 * b1
26 24, 25 ax_mp 
(a1 + c2) * b1 = a2 * b1 + c1 * b1 -> a1 * b1 + c2 * b1 = a2 * b1 + c1 * b1
27 eqtr 
(a1 + c2) * b1 = (a2 + c1) * b1 -> (a2 + c1) * b1 = a2 * b1 + c1 * b1 -> (a1 + c2) * b1 = a2 * b1 + c1 * b1
28 muleq1 
a1 + c2 = a2 + c1 -> (a1 + c2) * b1 = (a2 + c1) * b1
29 hyp h1 
a1 + c2 = a2 + c1
30 28, 29 ax_mp 
(a1 + c2) * b1 = (a2 + c1) * b1
31 27, 30 ax_mp 
(a2 + c1) * b1 = a2 * b1 + c1 * b1 -> (a1 + c2) * b1 = a2 * b1 + c1 * b1
32 addmul 
(a2 + c1) * b1 = a2 * b1 + c1 * b1
33 31, 32 ax_mp 
(a1 + c2) * b1 = a2 * b1 + c1 * b1
34 26, 33 ax_mp 
a1 * b1 + c2 * b1 = a2 * b1 + c1 * b1
35 23, 34 ax_mp 
a1 * b1 + b1 * c2 = a2 * b1 + c1 * b1
36 18, 35 ax_mp 
a1 * b1 + b1 * c2 + a2 * d2 = a2 * b1 + c1 * b1 + a2 * d2
37 17, 36 ax_mp 
a2 * b1 + c1 * b1 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1 -> a1 * b1 + b1 * c2 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
38 eqtr 
a2 * b1 + c1 * b1 + a2 * d2 = a2 * b1 + a2 * d2 + c1 * b1 ->
  a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1 ->
  a2 * b1 + c1 * b1 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
39 addrass 
a2 * b1 + c1 * b1 + a2 * d2 = a2 * b1 + a2 * d2 + c1 * b1
40 38, 39 ax_mp 
a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1 -> a2 * b1 + c1 * b1 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
41 eqtr 
a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + a2 * d1 + c1 * b1 ->
  a2 * b2 + a2 * d1 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1 ->
  a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1
42 addeq1 
a2 * b1 + a2 * d2 = a2 * b2 + a2 * d1 -> a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + a2 * d1 + c1 * b1
43 eqtr3 
a2 * (b1 + d2) = a2 * b1 + a2 * d2 -> a2 * (b1 + d2) = a2 * b2 + a2 * d1 -> a2 * b1 + a2 * d2 = a2 * b2 + a2 * d1
44 muladd 
a2 * (b1 + d2) = a2 * b1 + a2 * d2
45 43, 44 ax_mp 
a2 * (b1 + d2) = a2 * b2 + a2 * d1 -> a2 * b1 + a2 * d2 = a2 * b2 + a2 * d1
46 eqtr 
a2 * (b1 + d2) = a2 * (b2 + d1) -> a2 * (b2 + d1) = a2 * b2 + a2 * d1 -> a2 * (b1 + d2) = a2 * b2 + a2 * d1
47 muleq2 
b1 + d2 = b2 + d1 -> a2 * (b1 + d2) = a2 * (b2 + d1)
48 hyp h2 
b1 + d2 = b2 + d1
49 47, 48 ax_mp 
a2 * (b1 + d2) = a2 * (b2 + d1)
50 46, 49 ax_mp 
a2 * (b2 + d1) = a2 * b2 + a2 * d1 -> a2 * (b1 + d2) = a2 * b2 + a2 * d1
51 muladd 
a2 * (b2 + d1) = a2 * b2 + a2 * d1
52 50, 51 ax_mp 
a2 * (b1 + d2) = a2 * b2 + a2 * d1
53 45, 52 ax_mp 
a2 * b1 + a2 * d2 = a2 * b2 + a2 * d1
54 42, 53 ax_mp 
a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + a2 * d1 + c1 * b1
55 41, 54 ax_mp 
a2 * b2 + a2 * d1 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1 -> a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1
56 addrass 
a2 * b2 + a2 * d1 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1
57 55, 56 ax_mp 
a2 * b1 + a2 * d2 + c1 * b1 = a2 * b2 + c1 * b1 + a2 * d1
58 40, 57 ax_mp 
a2 * b1 + c1 * b1 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
59 37, 58 ax_mp 
a1 * b1 + b1 * c2 + a2 * d2 = a2 * b2 + c1 * b1 + a2 * d1
60 16, 59 ax_mp 
a1 * b1 + a2 * d2 + b1 * c2 = a2 * b2 + c1 * b1 + a2 * d1
61 13, 60 ax_mp 
b1 * c2 + (a1 * b1 + a2 * d2) = a2 * b2 + c1 * b1 + a2 * d1
62 10, 61 ax_mp 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2)
63 9, 62 ax_mp 
a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
64 eqtr 
a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) ->
  a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
65 addass 
a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2))
66 64, 65 ax_mp 
a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
67 eqtr3 
a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) ->
  a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
68 addeq2 
b1 * c2 + (c2 * d2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2) ->
  a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2))
69 eqtr3 
b1 * c2 + c2 * d2 + a1 * d1 = b1 * c2 + (c2 * d2 + a1 * d1) ->
  b1 * c2 + c2 * d2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2) ->
  b1 * c2 + (c2 * d2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
70 addass 
b1 * c2 + c2 * d2 + a1 * d1 = b1 * c2 + (c2 * d2 + a1 * d1)
71 69, 70 ax_mp 
b1 * c2 + c2 * d2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2) -> b1 * c2 + (c2 * d2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
72 eqtr 
b1 * c2 + c2 * d2 + a1 * d1 = b2 * c2 + d1 * c2 + a1 * d1 ->
  b2 * c2 + d1 * c2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2) ->
  b1 * c2 + c2 * d2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
73 addeq1 
b1 * c2 + c2 * d2 = b2 * c2 + d1 * c2 -> b1 * c2 + c2 * d2 + a1 * d1 = b2 * c2 + d1 * c2 + a1 * d1
74 eqtr 
b1 * c2 + c2 * d2 = b1 * c2 + d2 * c2 -> b1 * c2 + d2 * c2 = b2 * c2 + d1 * c2 -> b1 * c2 + c2 * d2 = b2 * c2 + d1 * c2
75 addeq2 
c2 * d2 = d2 * c2 -> b1 * c2 + c2 * d2 = b1 * c2 + d2 * c2
76 mulcom 
c2 * d2 = d2 * c2
77 75, 76 ax_mp 
b1 * c2 + c2 * d2 = b1 * c2 + d2 * c2
78 74, 77 ax_mp 
b1 * c2 + d2 * c2 = b2 * c2 + d1 * c2 -> b1 * c2 + c2 * d2 = b2 * c2 + d1 * c2
79 eqtr3 
(b1 + d2) * c2 = b1 * c2 + d2 * c2 -> (b1 + d2) * c2 = b2 * c2 + d1 * c2 -> b1 * c2 + d2 * c2 = b2 * c2 + d1 * c2
80 addmul 
(b1 + d2) * c2 = b1 * c2 + d2 * c2
81 79, 80 ax_mp 
(b1 + d2) * c2 = b2 * c2 + d1 * c2 -> b1 * c2 + d2 * c2 = b2 * c2 + d1 * c2
82 eqtr 
(b1 + d2) * c2 = (b2 + d1) * c2 -> (b2 + d1) * c2 = b2 * c2 + d1 * c2 -> (b1 + d2) * c2 = b2 * c2 + d1 * c2
83 muleq1 
b1 + d2 = b2 + d1 -> (b1 + d2) * c2 = (b2 + d1) * c2
84 83, 48 ax_mp 
(b1 + d2) * c2 = (b2 + d1) * c2
85 82, 84 ax_mp 
(b2 + d1) * c2 = b2 * c2 + d1 * c2 -> (b1 + d2) * c2 = b2 * c2 + d1 * c2
86 addmul 
(b2 + d1) * c2 = b2 * c2 + d1 * c2
87 85, 86 ax_mp 
(b1 + d2) * c2 = b2 * c2 + d1 * c2
88 81, 87 ax_mp 
b1 * c2 + d2 * c2 = b2 * c2 + d1 * c2
89 78, 88 ax_mp 
b1 * c2 + c2 * d2 = b2 * c2 + d1 * c2
90 73, 89 ax_mp 
b1 * c2 + c2 * d2 + a1 * d1 = b2 * c2 + d1 * c2 + a1 * d1
91 72, 90 ax_mp 
b2 * c2 + d1 * c2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2) -> b1 * c2 + c2 * d2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
92 eqtr 
b2 * c2 + d1 * c2 + a1 * d1 = b2 * c2 + (d1 * c2 + a1 * d1) ->
  b2 * c2 + (d1 * c2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2) ->
  b2 * c2 + d1 * c2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
93 addass 
b2 * c2 + d1 * c2 + a1 * d1 = b2 * c2 + (d1 * c2 + a1 * d1)
94 92, 93 ax_mp 
b2 * c2 + (d1 * c2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2) -> b2 * c2 + d1 * c2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
95 eqtr4 
b2 * c2 + (d1 * c2 + a1 * d1) = b2 * c2 + (a2 * d1 + c1 * d1) ->
  a2 * d1 + (c1 * d1 + b2 * c2) = b2 * c2 + (a2 * d1 + c1 * d1) ->
  b2 * c2 + (d1 * c2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
96 addeq2 
d1 * c2 + a1 * d1 = a2 * d1 + c1 * d1 -> b2 * c2 + (d1 * c2 + a1 * d1) = b2 * c2 + (a2 * d1 + c1 * d1)
97 eqtr 
d1 * c2 + a1 * d1 = c2 * d1 + a1 * d1 -> c2 * d1 + a1 * d1 = a2 * d1 + c1 * d1 -> d1 * c2 + a1 * d1 = a2 * d1 + c1 * d1
98 addeq1 
d1 * c2 = c2 * d1 -> d1 * c2 + a1 * d1 = c2 * d1 + a1 * d1
99 mulcom 
d1 * c2 = c2 * d1
100 98, 99 ax_mp 
d1 * c2 + a1 * d1 = c2 * d1 + a1 * d1
101 97, 100 ax_mp 
c2 * d1 + a1 * d1 = a2 * d1 + c1 * d1 -> d1 * c2 + a1 * d1 = a2 * d1 + c1 * d1
102 eqtr 
c2 * d1 + a1 * d1 = a1 * d1 + c2 * d1 -> a1 * d1 + c2 * d1 = a2 * d1 + c1 * d1 -> c2 * d1 + a1 * d1 = a2 * d1 + c1 * d1
103 addcom 
c2 * d1 + a1 * d1 = a1 * d1 + c2 * d1
104 102, 103 ax_mp 
a1 * d1 + c2 * d1 = a2 * d1 + c1 * d1 -> c2 * d1 + a1 * d1 = a2 * d1 + c1 * d1
105 eqtr3 
(a1 + c2) * d1 = a1 * d1 + c2 * d1 -> (a1 + c2) * d1 = a2 * d1 + c1 * d1 -> a1 * d1 + c2 * d1 = a2 * d1 + c1 * d1
106 addmul 
(a1 + c2) * d1 = a1 * d1 + c2 * d1
107 105, 106 ax_mp 
(a1 + c2) * d1 = a2 * d1 + c1 * d1 -> a1 * d1 + c2 * d1 = a2 * d1 + c1 * d1
108 eqtr 
(a1 + c2) * d1 = (a2 + c1) * d1 -> (a2 + c1) * d1 = a2 * d1 + c1 * d1 -> (a1 + c2) * d1 = a2 * d1 + c1 * d1
109 muleq1 
a1 + c2 = a2 + c1 -> (a1 + c2) * d1 = (a2 + c1) * d1
110 109, 29 ax_mp 
(a1 + c2) * d1 = (a2 + c1) * d1
111 108, 110 ax_mp 
(a2 + c1) * d1 = a2 * d1 + c1 * d1 -> (a1 + c2) * d1 = a2 * d1 + c1 * d1
112 addmul 
(a2 + c1) * d1 = a2 * d1 + c1 * d1
113 111, 112 ax_mp 
(a1 + c2) * d1 = a2 * d1 + c1 * d1
114 107, 113 ax_mp 
a1 * d1 + c2 * d1 = a2 * d1 + c1 * d1
115 104, 114 ax_mp 
c2 * d1 + a1 * d1 = a2 * d1 + c1 * d1
116 101, 115 ax_mp 
d1 * c2 + a1 * d1 = a2 * d1 + c1 * d1
117 96, 116 ax_mp 
b2 * c2 + (d1 * c2 + a1 * d1) = b2 * c2 + (a2 * d1 + c1 * d1)
118 95, 117 ax_mp 
a2 * d1 + (c1 * d1 + b2 * c2) = b2 * c2 + (a2 * d1 + c1 * d1) -> b2 * c2 + (d1 * c2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
119 eqtr3 
a2 * d1 + c1 * d1 + b2 * c2 = a2 * d1 + (c1 * d1 + b2 * c2) ->
  a2 * d1 + c1 * d1 + b2 * c2 = b2 * c2 + (a2 * d1 + c1 * d1) ->
  a2 * d1 + (c1 * d1 + b2 * c2) = b2 * c2 + (a2 * d1 + c1 * d1)
120 addass 
a2 * d1 + c1 * d1 + b2 * c2 = a2 * d1 + (c1 * d1 + b2 * c2)
121 119, 120 ax_mp 
a2 * d1 + c1 * d1 + b2 * c2 = b2 * c2 + (a2 * d1 + c1 * d1) -> a2 * d1 + (c1 * d1 + b2 * c2) = b2 * c2 + (a2 * d1 + c1 * d1)
122 addcom 
a2 * d1 + c1 * d1 + b2 * c2 = b2 * c2 + (a2 * d1 + c1 * d1)
123 121, 122 ax_mp 
a2 * d1 + (c1 * d1 + b2 * c2) = b2 * c2 + (a2 * d1 + c1 * d1)
124 118, 123 ax_mp 
b2 * c2 + (d1 * c2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
125 94, 124 ax_mp 
b2 * c2 + d1 * c2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
126 91, 125 ax_mp 
b1 * c2 + c2 * d2 + a1 * d1 = a2 * d1 + (c1 * d1 + b2 * c2)
127 71, 126 ax_mp 
b1 * c2 + (c2 * d2 + a1 * d1) = a2 * d1 + (c1 * d1 + b2 * c2)
128 68, 127 ax_mp 
a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2))
129 67, 128 ax_mp 
a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
130 eqtr3 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
131 addass 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1))
132 130, 131 ax_mp 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
133 eqtr 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1) ->
  b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
134 addeq1 
a2 * b2 + c1 * b1 + b1 * c2 = b1 * c2 + (a2 * b2 + c1 * b1) ->
  a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1)
135 addcom 
a2 * b2 + c1 * b1 + b1 * c2 = b1 * c2 + (a2 * b2 + c1 * b1)
136 134, 135 ax_mp 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1)
137 133, 136 ax_mp 
b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)) ->
  a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
138 addass 
b1 * c2 + (a2 * b2 + c1 * b1) + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
139 137, 138 ax_mp 
a2 * b2 + c1 * b1 + b1 * c2 + (c2 * d2 + a1 * d1) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
140 132, 139 ax_mp 
a2 * b2 + c1 * b1 + (b1 * c2 + (c2 * d2 + a1 * d1)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
141 129, 140 ax_mp 
a2 * b2 + c1 * b1 + (a2 * d1 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
142 66, 141 ax_mp 
a2 * b2 + c1 * b1 + a2 * d1 + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
143 63, 142 ax_mp 
b1 * c2 + (a1 * b1 + a2 * d2) + (c1 * d1 + b2 * c2) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
144 8, 143 ax_mp 
b1 * c2 + (a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2)) = b1 * c2 + (a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1))
145 5, 144 mpbi 
a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1)
146 4, 145 ax_mp 
a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
147 eqtr 
a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1) ->
  a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
148 add4 
a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1)
149 147, 148 ax_mp 
a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1) ->
  a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
150 addeq2 
c1 * b1 + a1 * d1 = a1 * d1 + c1 * b1 -> a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
151 addcom 
c1 * b1 + a1 * d1 = a1 * d1 + c1 * b1
152 150, 151 ax_mp 
a2 * b2 + c2 * d2 + (c1 * b1 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
153 149, 152 ax_mp 
a2 * b2 + c1 * b1 + (c2 * d2 + a1 * d1) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
154 146, 153 ax_mp 
a1 * b1 + a2 * d2 + (c1 * d1 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)
155 3, 154 ax_mp 
a1 * b1 + c1 * d1 + (a2 * d2 + b2 * c2) = a2 * b2 + c2 * d2 + (a1 * d1 + c1 * b1)

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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)