Theorem bgcddvd1lem ≪ | index | src | ≫ 

theorem bgcddvd1lem (G: wff) (a b d q r u x y: nat):
  $ G -> a != 0 $ >
  $ G -> x * a = y * b + d $ >
  $ G -> b != 0 $ >
  $ G -> d * q + r = a $ >
  $ G -> x <= u $ >
  $ G -> y <= u $ >
  $ G -> suc ((u * b - x) * q) * a = (u * a - y) * q * b + r $;
StepHypRefExpression
1 addcan1 
suc ((u * b - x) * q) * a + (x * q * a + y * q * b) = (u * a - y) * q * b + r + (x * q * a + y * q * b) <-> suc ((u * b - x) * q) * a = (u * a - y) * q * b + r
2 addass 
suc ((u * b - x) * q) * a + x * q * a + y * q * b = suc ((u * b - x) * q) * a + (x * q * a + y * q * b)
3 addmul 
(suc ((u * b - x) * q) + x * q) * a = suc ((u * b - x) * q) * a + x * q * a
4 addS1 
suc ((u * b - x) * q) + x * q = suc ((u * b - x) * q + x * q)
5 addmul 
(u * b - x + x) * q = (u * b - x) * q + x * q
6 npcan 
x <= u * b -> u * b - x + x = u * b
7 hyp h5 
G -> x <= u
8 leeq1 
u * 1 = u -> (u * 1 <= u * b <-> u <= u * b)
9 mul12 
u * 1 = u
10 8, 9 ax_mp 
u * 1 <= u * b <-> u <= u * b
11 lemul2a 
1 <= b -> u * 1 <= u * b
12 lt01 
0 < b <-> b != 0
13 12 conv d1, lt 
1 <= b <-> b != 0
14 hyp h3 
G -> b != 0
15 13, 14 sylibr 
G -> 1 <= b
16 11, 15 syl 
G -> u * 1 <= u * b
17 10, 16 sylib 
G -> u <= u * b
18 7, 17 letrd 
G -> x <= u * b
19 6, 18 syl 
G -> u * b - x + x = u * b
20 19 muleq1d 
G -> (u * b - x + x) * q = u * b * q
21 5, 20 syl5eqr 
G -> (u * b - x) * q + x * q = u * b * q
22 21 suceqd 
G -> suc ((u * b - x) * q + x * q) = suc (u * b * q)
23 4, 22 syl5eq 
G -> suc ((u * b - x) * q) + x * q = suc (u * b * q)
24 23 muleq1d 
G -> (suc ((u * b - x) * q) + x * q) * a = suc (u * b * q) * a
25 3, 24 syl5eqr 
G -> suc ((u * b - x) * q) * a + x * q * a = suc (u * b * q) * a
26 25 addeq1d 
G -> suc ((u * b - x) * q) * a + x * q * a + y * q * b = suc (u * b * q) * a + y * q * b
27 addeq2 
x * q * a + y * q * b = y * q * b + x * q * a -> (u * a - y) * q * b + r + (x * q * a + y * q * b) = (u * a - y) * q * b + r + (y * q * b + x * q * a)
28 addcom 
x * q * a + y * q * b = y * q * b + x * q * a
29 27, 28 ax_mp 
(u * a - y) * q * b + r + (x * q * a + y * q * b) = (u * a - y) * q * b + r + (y * q * b + x * q * a)
30 addass 
(u * a - y) * q * b + r + y * q * b + x * q * a = (u * a - y) * q * b + r + (y * q * b + x * q * a)
31 addrass 
(u * a - y) * q * b + r + y * q * b = (u * a - y) * q * b + y * q * b + r
32 addmul 
((u * a - y) * q + y * q) * b = (u * a - y) * q * b + y * q * b
33 addmul 
(u * a - y + y) * q = (u * a - y) * q + y * q
34 npcan 
y <= u * a -> u * a - y + y = u * a
35 hyp h6 
G -> y <= u
36 leeq1 
u * 1 = u -> (u * 1 <= u * a <-> u <= u * a)
37 36, 9 ax_mp 
u * 1 <= u * a <-> u <= u * a
38 lemul2a 
1 <= a -> u * 1 <= u * a
39 lt01 
0 < a <-> a != 0
40 39 conv d1, lt 
1 <= a <-> a != 0
41 hyp h1 
G -> a != 0
42 40, 41 sylibr 
G -> 1 <= a
43 38, 42 syl 
G -> u * 1 <= u * a
44 37, 43 sylib 
G -> u <= u * a
45 35, 44 letrd 
G -> y <= u * a
46 34, 45 syl 
G -> u * a - y + y = u * a
47 46 muleq1d 
G -> (u * a - y + y) * q = u * a * q
48 33, 47 syl5eqr 
G -> (u * a - y) * q + y * q = u * a * q
49 48 muleq1d 
G -> ((u * a - y) * q + y * q) * b = u * a * q * b
50 32, 49 syl5eqr 
G -> (u * a - y) * q * b + y * q * b = u * a * q * b
51 50 addeq1d 
G -> (u * a - y) * q * b + y * q * b + r = u * a * q * b + r
52 31, 51 syl5eq 
G -> (u * a - y) * q * b + r + y * q * b = u * a * q * b + r
53 52 addeq1d 
G -> (u * a - y) * q * b + r + y * q * b + x * q * a = u * a * q * b + r + x * q * a
54 addrass 
u * a * q * b + r + x * q * a = u * a * q * b + x * q * a + r
55 addass 
u * a * q * b + x * q * a + r = u * a * q * b + (x * q * a + r)
56 addeq1 
suc (u * b * q) * a = u * a * q * b + a -> suc (u * b * q) * a + y * q * b = u * a * q * b + a + y * q * b
57 eqtr 
suc (u * b * q) * a = u * b * q * a + a -> u * b * q * a + a = u * a * q * b + a -> suc (u * b * q) * a = u * a * q * b + a
58 mulS1 
suc (u * b * q) * a = u * b * q * a + a
59 57, 58 ax_mp 
u * b * q * a + a = u * a * q * b + a -> suc (u * b * q) * a = u * a * q * b + a
60 addeq1 
u * b * q * a = u * a * q * b -> u * b * q * a + a = u * a * q * b + a
61 eqtr 
u * b * q * a = u * b * (q * a) -> u * b * (q * a) = u * a * q * b -> u * b * q * a = u * a * q * b
62 mulass 
u * b * q * a = u * b * (q * a)
63 61, 62 ax_mp 
u * b * (q * a) = u * a * q * b -> u * b * q * a = u * a * q * b
64 eqtr 
u * b * (q * a) = u * (b * (q * a)) -> u * (b * (q * a)) = u * a * q * b -> u * b * (q * a) = u * a * q * b
65 mulass 
u * b * (q * a) = u * (b * (q * a))
66 64, 65 ax_mp 
u * (b * (q * a)) = u * a * q * b -> u * b * (q * a) = u * a * q * b
67 eqtr4 
u * (b * (q * a)) = u * (a * q * b) -> u * a * q * b = u * (a * q * b) -> u * (b * (q * a)) = u * a * q * b
68 muleq2 
b * (q * a) = a * q * b -> u * (b * (q * a)) = u * (a * q * b)
69 eqtr 
b * (q * a) = q * a * b -> q * a * b = a * q * b -> b * (q * a) = a * q * b
70 mulcom 
b * (q * a) = q * a * b
71 69, 70 ax_mp 
q * a * b = a * q * b -> b * (q * a) = a * q * b
72 muleq1 
q * a = a * q -> q * a * b = a * q * b
73 mulcom 
q * a = a * q
74 72, 73 ax_mp 
q * a * b = a * q * b
75 71, 74 ax_mp 
b * (q * a) = a * q * b
76 68, 75 ax_mp 
u * (b * (q * a)) = u * (a * q * b)
77 67, 76 ax_mp 
u * a * q * b = u * (a * q * b) -> u * (b * (q * a)) = u * a * q * b
78 eqtr 
u * a * q * b = u * (a * q) * b -> u * (a * q) * b = u * (a * q * b) -> u * a * q * b = u * (a * q * b)
79 muleq1 
u * a * q = u * (a * q) -> u * a * q * b = u * (a * q) * b
80 mulass 
u * a * q = u * (a * q)
81 79, 80 ax_mp 
u * a * q * b = u * (a * q) * b
82 78, 81 ax_mp 
u * (a * q) * b = u * (a * q * b) -> u * a * q * b = u * (a * q * b)
83 mulass 
u * (a * q) * b = u * (a * q * b)
84 82, 83 ax_mp 
u * a * q * b = u * (a * q * b)
85 77, 84 ax_mp 
u * (b * (q * a)) = u * a * q * b
86 66, 85 ax_mp 
u * b * (q * a) = u * a * q * b
87 63, 86 ax_mp 
u * b * q * a = u * a * q * b
88 60, 87 ax_mp 
u * b * q * a + a = u * a * q * b + a
89 59, 88 ax_mp 
suc (u * b * q) * a = u * a * q * b + a
90 56, 89 ax_mp 
suc (u * b * q) * a + y * q * b = u * a * q * b + a + y * q * b
91 addass 
u * a * q * b + a + y * q * b = u * a * q * b + (a + y * q * b)
92 addcom 
a + y * q * b = y * q * b + a
93 hyp h4 
G -> d * q + r = a
94 93 addeq2d 
G -> y * q * b + (d * q + r) = y * q * b + a
95 addass 
y * q * b + d * q + r = y * q * b + (d * q + r)
96 addeq1 
y * q * b = y * b * q -> y * q * b + d * q = y * b * q + d * q
97 mulrass 
y * q * b = y * b * q
98 96, 97 ax_mp 
y * q * b + d * q = y * b * q + d * q
99 addmul 
(y * b + d) * q = y * b * q + d * q
100 mulrass 
x * a * q = x * q * a
101 hyp h2 
G -> x * a = y * b + d
102 101 eqcomd 
G -> y * b + d = x * a
103 102 muleq1d 
G -> (y * b + d) * q = x * a * q
104 100, 103 syl6eq 
G -> (y * b + d) * q = x * q * a
105 99, 104 syl5eqr 
G -> y * b * q + d * q = x * q * a
106 98, 105 syl5eq 
G -> y * q * b + d * q = x * q * a
107 106 addeq1d 
G -> y * q * b + d * q + r = x * q * a + r
108 95, 107 syl5eqr 
G -> y * q * b + (d * q + r) = x * q * a + r
109 94, 108 eqtr3d 
G -> y * q * b + a = x * q * a + r
110 92, 109 syl5eq 
G -> a + y * q * b = x * q * a + r
111 110 addeq2d 
G -> u * a * q * b + (a + y * q * b) = u * a * q * b + (x * q * a + r)
112 91, 111 syl5eq 
G -> u * a * q * b + a + y * q * b = u * a * q * b + (x * q * a + r)
113 90, 112 syl5eq 
G -> suc (u * b * q) * a + y * q * b = u * a * q * b + (x * q * a + r)
114 55, 113 syl6eqr 
G -> suc (u * b * q) * a + y * q * b = u * a * q * b + x * q * a + r
115 54, 114 syl6eqr 
G -> suc (u * b * q) * a + y * q * b = u * a * q * b + r + x * q * a
116 53, 115 eqtr4d 
G -> (u * a - y) * q * b + r + y * q * b + x * q * a = suc (u * b * q) * a + y * q * b
117 30, 116 syl5eqr 
G -> (u * a - y) * q * b + r + (y * q * b + x * q * a) = suc (u * b * q) * a + y * q * b
118 29, 117 syl5eq 
G -> (u * a - y) * q * b + r + (x * q * a + y * q * b) = suc (u * b * q) * a + y * q * b
119 26, 118 eqtr4d 
G -> suc ((u * b - x) * q) * a + x * q * a + y * q * b = (u * a - y) * q * b + r + (x * q * a + y * q * b)
120 2, 119 syl5eqr 
G -> suc ((u * b - x) * q) * a + (x * q * a + y * q * b) = (u * a - y) * q * b + r + (x * q * a + y * q * b)
121 1, 120 sylib 
G -> suc ((u * b - x) * q) * a = (u * a - y) * q * b + r

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)