Theorem bgcddvd2lem ≪ | index | src | ≫

theorem bgcddvd2lem (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 = b $ >
  $ G -> x * q <= u $ >
  $ G -> y * q < u $ >
  $ G -> (u * b - x * q) * a = (u * a - suc (y * q)) * b + r $;

Step	Hyp	Ref	Expression
1		addcan1	(u * b - x * q) * a + (x * q * a + suc (y * q) * b) = (u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b) <-> (u * b - x * q) * a = (u * a - suc (y * q)) * b + r
2		addass	(u * b - x * q) * a + x * q * a + suc (y * q) * b = (u * b - x * q) * a + (x * q * a + suc (y * q) * b)
3		addmul	(u * b - x * q + x * q) * a = (u * b - x * q) * a + x * q * a
4		npcan	x * q <= u * b -> u * b - x * q + x * q = u * b
5		hyp h5	G -> x * q <= u
6		leeq1	u * 1 = u -> (u * 1 <= u * b <-> u <= u * b)
7		mul12	u * 1 = u
8	6, 7	ax_mp	u * 1 <= u * b <-> u <= u * b
9		lemul2a	1 <= b -> u * 1 <= u * b
10		lt01	0 < b <-> b != 0
11	10	conv d1, lt	1 <= b <-> b != 0
12		hyp h3	G -> b != 0
13	11, 12	sylibr	G -> 1 <= b
14	9, 13	syl	G -> u * 1 <= u * b
15	8, 14	sylib	G -> u <= u * b
16	5, 15	letrd	G -> x * q <= u * b
17	4, 16	syl	G -> u * b - x * q + x * q = u * b
18	17	muleq1d	G -> (u * b - x * q + x * q) * a = u * b * a
19	3, 18	syl5eqr	G -> (u * b - x * q) * a + x * q * a = u * b * a
20	19	addeq1d	G -> (u * b - x * q) * a + x * q * a + suc (y * q) * b = u * b * a + suc (y * q) * b
21		addeq2	x * q * a + suc (y * q) * b = suc (y * q) * b + x * q * a -> (u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b) = (u * a - suc (y * q)) * b + r + (suc (y * q) * b + x * q * a)
22		addcom	x * q * a + suc (y * q) * b = suc (y * q) * b + x * q * a
23	21, 22	ax_mp	(u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b) = (u * a - suc (y * q)) * b + r + (suc (y * q) * b + x * q * a)
24		addass	(u * a - suc (y * q)) * b + r + suc (y * q) * b + x * q * a = (u * a - suc (y * q)) * b + r + (suc (y * q) * b + x * q * a)
25		addrass	(u * a - suc (y * q)) * b + r + suc (y * q) * b = (u * a - suc (y * q)) * b + suc (y * q) * b + r
26		addmul	(u * a - suc (y * q) + suc (y * q)) * b = (u * a - suc (y * q)) * b + suc (y * q) * b
27		npcan	suc (y * q) <= u * a -> u * a - suc (y * q) + suc (y * q) = u * a
28		hyp h6	G -> y * q < u
29	28	conv lt	G -> suc (y * q) <= u
30		leeq1	u * 1 = u -> (u * 1 <= u * a <-> u <= u * a)
31	30, 7	ax_mp	u * 1 <= u * a <-> u <= u * a
32		lemul2a	1 <= a -> u * 1 <= u * a
33		lt01	0 < a <-> a != 0
34	33	conv d1, lt	1 <= a <-> a != 0
35		hyp h1	G -> a != 0
36	34, 35	sylibr	G -> 1 <= a
37	32, 36	syl	G -> u * 1 <= u * a
38	31, 37	sylib	G -> u <= u * a
39	29, 38	letrd	G -> suc (y * q) <= u * a
40	27, 39	syl	G -> u * a - suc (y * q) + suc (y * q) = u * a
41	40	muleq1d	G -> (u * a - suc (y * q) + suc (y * q)) * b = u * a * b
42	26, 41	syl5eqr	G -> (u * a - suc (y * q)) * b + suc (y * q) * b = u * a * b
43	42	addeq1d	G -> (u * a - suc (y * q)) * b + suc (y * q) * b + r = u * a * b + r
44	25, 43	syl5eq	G -> (u * a - suc (y * q)) * b + r + suc (y * q) * b = u * a * b + r
45	44	addeq1d	G -> (u * a - suc (y * q)) * b + r + suc (y * q) * b + x * q * a = u * a * b + r + x * q * a
46		addrass	u * a * b + r + x * q * a = u * a * b + x * q * a + r
47		addass	u * a * b + x * q * a + r = u * a * b + (x * q * a + r)
48		addeq1	u * b * a = u * a * b -> u * b * a + suc (y * q) * b = u * a * b + suc (y * q) * b
49		mulrass	u * b * a = u * a * b
50	48, 49	ax_mp	u * b * a + suc (y * q) * b = u * a * b + suc (y * q) * b
51		mulS1	suc (y * q) * b = y * q * b + b
52		hyp h4	G -> d * q + r = b
53	52	addeq2d	G -> y * q * b + (d * q + r) = y * q * b + b
54		addass	y * q * b + d * q + r = y * q * b + (d * q + r)
55		addeq1	y * q * b = y * b * q -> y * q * b + d * q = y * b * q + d * q
56		mulrass	y * q * b = y * b * q
57	55, 56	ax_mp	y * q * b + d * q = y * b * q + d * q
58		addmul	(y * b + d) * q = y * b * q + d * q
59		mulrass	x * a * q = x * q * a
60		hyp h2	G -> x * a = y * b + d
61	60	eqcomd	G -> y * b + d = x * a
62	61	muleq1d	G -> (y * b + d) * q = x * a * q
63	59, 62	syl6eq	G -> (y * b + d) * q = x * q * a
64	58, 63	syl5eqr	G -> y * b * q + d * q = x * q * a
65	57, 64	syl5eq	G -> y * q * b + d * q = x * q * a
66	65	addeq1d	G -> y * q * b + d * q + r = x * q * a + r
67	54, 66	syl5eqr	G -> y * q * b + (d * q + r) = x * q * a + r
68	53, 67	eqtr3d	G -> y * q * b + b = x * q * a + r
69	51, 68	syl5eq	G -> suc (y * q) * b = x * q * a + r
70	69	addeq2d	G -> u * a * b + suc (y * q) * b = u * a * b + (x * q * a + r)
71	50, 70	syl5eq	G -> u * b * a + suc (y * q) * b = u * a * b + (x * q * a + r)
72	47, 71	syl6eqr	G -> u * b * a + suc (y * q) * b = u * a * b + x * q * a + r
73	46, 72	syl6eqr	G -> u * b * a + suc (y * q) * b = u * a * b + r + x * q * a
74	45, 73	eqtr4d	G -> (u * a - suc (y * q)) * b + r + suc (y * q) * b + x * q * a = u * b * a + suc (y * q) * b
75	24, 74	syl5eqr	G -> (u * a - suc (y * q)) * b + r + (suc (y * q) * b + x * q * a) = u * b * a + suc (y * q) * b
76	23, 75	syl5eq	G -> (u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b) = u * b * a + suc (y * q) * b
77	20, 76	eqtr4d	G -> (u * b - x * q) * a + x * q * a + suc (y * q) * b = (u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b)
78	2, 77	syl5eqr	G -> (u * b - x * q) * a + (x * q * a + suc (y * q) * b) = (u * a - suc (y * q)) * b + r + (x * q * a + suc (y * q) * b)
79	1, 78	sylib	G -> (u * b - x * q) * a = (u * a - suc (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)