MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bezoutlem4 Structured version   Visualization version   GIF version

Theorem bezoutlem4 15186
Description: Lemma for bezout 15187. (Contributed by Mario Carneiro, 22-Feb-2014.)
Hypotheses
Ref Expression
bezout.1 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}
bezout.3 (𝜑𝐴 ∈ ℤ)
bezout.4 (𝜑𝐵 ∈ ℤ)
bezout.2 𝐺 = inf(𝑀, ℝ, < )
bezout.5 (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
Assertion
Ref Expression
bezoutlem4 (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐺,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝑀,𝑦
Allowed substitution hint:   𝑀(𝑧)

Proof of Theorem bezoutlem4
Dummy variables 𝑡 𝑠 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bezout.3 . . . . . . . 8 (𝜑𝐴 ∈ ℤ)
2 bezout.4 . . . . . . . 8 (𝜑𝐵 ∈ ℤ)
3 gcddvds 15152 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
41, 2, 3syl2anc 692 . . . . . . 7 (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))
54simpld 475 . . . . . 6 (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐴)
61, 2gcdcld 15157 . . . . . . . 8 (𝜑 → (𝐴 gcd 𝐵) ∈ ℕ0)
76nn0zd 11427 . . . . . . 7 (𝜑 → (𝐴 gcd 𝐵) ∈ ℤ)
8 divides 14912 . . . . . . 7 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴))
97, 1, 8syl2anc 692 . . . . . 6 (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴))
105, 9mpbid 222 . . . . 5 (𝜑 → ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴)
114simprd 479 . . . . . 6 (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐵)
12 divides 14912 . . . . . . 7 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵))
137, 2, 12syl2anc 692 . . . . . 6 (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵))
1411, 13mpbid 222 . . . . 5 (𝜑 → ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)
15 reeanv 3097 . . . . . 6 (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) ↔ (∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵))
16 bezout.1 . . . . . . . . . . 11 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}
17 bezout.2 . . . . . . . . . . 11 𝐺 = inf(𝑀, ℝ, < )
18 bezout.5 . . . . . . . . . . 11 (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))
1916, 1, 2, 17, 18bezoutlem2 15184 . . . . . . . . . 10 (𝜑𝐺𝑀)
20 oveq2 6615 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢))
2120oveq1d 6622 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑦)))
2221eqeq2d 2631 . . . . . . . . . . . . 13 (𝑥 = 𝑢 → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦))))
23 oveq2 6615 . . . . . . . . . . . . . . 15 (𝑦 = 𝑣 → (𝐵 · 𝑦) = (𝐵 · 𝑣))
2423oveq2d 6623 . . . . . . . . . . . . . 14 (𝑦 = 𝑣 → ((𝐴 · 𝑢) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))
2524eqeq2d 2631 . . . . . . . . . . . . 13 (𝑦 = 𝑣 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
2622, 25cbvrex2v 3168 . . . . . . . . . . . 12 (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))
27 eqeq1 2625 . . . . . . . . . . . . 13 (𝑧 = 𝐺 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
28272rexbidv 3050 . . . . . . . . . . . 12 (𝑧 = 𝐺 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
2926, 28syl5bb 272 . . . . . . . . . . 11 (𝑧 = 𝐺 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
3029, 16elrab2 3349 . . . . . . . . . 10 (𝐺𝑀 ↔ (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
3119, 30sylib 208 . . . . . . . . 9 (𝜑 → (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
3231simprd 479 . . . . . . . 8 (𝜑 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))
33 simprrl 803 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℤ)
34 simprll 801 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℤ)
3533, 34zmulcld 11435 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℤ)
36 simprrr 804 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℤ)
37 simprlr 802 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℤ)
3836, 37zmulcld 11435 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℤ)
3935, 38zaddcld 11433 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ)
407adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℤ)
41 dvdsmul2 14931 . . . . . . . . . . . . . . 15 ((((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)))
4239, 40, 41syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)))
4335zcnd 11430 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℂ)
4438zcnd 11430 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℂ)
4540zcnd 11430 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℂ)
4643, 44, 45adddird 10012 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)) = (((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) + ((𝑡 · 𝑣) · (𝐴 gcd 𝐵))))
4733zcnd 11430 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℂ)
4834zcnd 11430 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℂ)
4947, 48, 45mul32d 10193 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) = ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢))
5036zcnd 11430 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℂ)
5137zcnd 11430 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℂ)
5250, 51, 45mul32d 10193 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑡 · 𝑣) · (𝐴 gcd 𝐵)) = ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))
5349, 52oveq12d 6625 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) + ((𝑡 · 𝑣) · (𝐴 gcd 𝐵))) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)))
5446, 53eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)))
5542, 54breqtrd 4641 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)))
56 oveq1 6614 . . . . . . . . . . . . . . 15 ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) = (𝐴 · 𝑢))
57 oveq1 6614 . . . . . . . . . . . . . . 15 ((𝑡 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣) = (𝐵 · 𝑣))
5856, 57oveqan12d 6626 . . . . . . . . . . . . . 14 (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))
5958breq2d 4627 . . . . . . . . . . . . 13 (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → ((𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
6055, 59syl5ibcom 235 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
61 breq2 4619 . . . . . . . . . . . . 13 (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝐴 gcd 𝐵) ∥ 𝐺 ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣))))
6261imbi2d 330 . . . . . . . . . . . 12 (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺) ↔ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))))
6360, 62syl5ibrcom 237 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))
6463expr 642 . . . . . . . . . 10 ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))))
6564com23 86 . . . . . . . . 9 ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))))
6665rexlimdvva 3031 . . . . . . . 8 (𝜑 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))))
6732, 66mpd 15 . . . . . . 7 (𝜑 → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))
6867rexlimdvv 3030 . . . . . 6 (𝜑 → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))
6915, 68syl5bir 233 . . . . 5 (𝜑 → ((∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))
7010, 14, 69mp2and 714 . . . 4 (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐺)
7131simpld 475 . . . . 5 (𝜑𝐺 ∈ ℕ)
72 dvdsle 14959 . . . . 5 (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐺 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺))
737, 71, 72syl2anc 692 . . . 4 (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺))
7470, 73mpd 15 . . 3 (𝜑 → (𝐴 gcd 𝐵) ≤ 𝐺)
75 breq2 4619 . . . . 5 (𝐴 = 0 → (𝐺𝐴𝐺 ∥ 0))
7616, 1, 2bezoutlem1 15183 . . . . . . . 8 (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀))
7716, 1, 2, 17, 18bezoutlem3 15185 . . . . . . . 8 (𝜑 → ((abs‘𝐴) ∈ 𝑀𝐺 ∥ (abs‘𝐴)))
7876, 77syld 47 . . . . . . 7 (𝜑 → (𝐴 ≠ 0 → 𝐺 ∥ (abs‘𝐴)))
7971nnzd 11428 . . . . . . . 8 (𝜑𝐺 ∈ ℤ)
80 dvdsabsb 14928 . . . . . . . 8 ((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐺𝐴𝐺 ∥ (abs‘𝐴)))
8179, 1, 80syl2anc 692 . . . . . . 7 (𝜑 → (𝐺𝐴𝐺 ∥ (abs‘𝐴)))
8278, 81sylibrd 249 . . . . . 6 (𝜑 → (𝐴 ≠ 0 → 𝐺𝐴))
8382imp 445 . . . . 5 ((𝜑𝐴 ≠ 0) → 𝐺𝐴)
84 dvds0 14924 . . . . . 6 (𝐺 ∈ ℤ → 𝐺 ∥ 0)
8579, 84syl 17 . . . . 5 (𝜑𝐺 ∥ 0)
8675, 83, 85pm2.61ne 2875 . . . 4 (𝜑𝐺𝐴)
87 breq2 4619 . . . . 5 (𝐵 = 0 → (𝐺𝐵𝐺 ∥ 0))
88 eqid 2621 . . . . . . . . . 10 {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}
8988, 2, 1bezoutlem1 15183 . . . . . . . . 9 (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}))
90 rexcom 3091 . . . . . . . . . . . . 13 (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
911zcnd 11430 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ ℂ)
9291adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐴 ∈ ℂ)
93 zcn 11329 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
9493ad2antll 764 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑥 ∈ ℂ)
9592, 94mulcld 10007 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐴 · 𝑥) ∈ ℂ)
962zcnd 11430 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℂ)
9796adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐵 ∈ ℂ)
98 zcn 11329 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
9998ad2antrl 763 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑦 ∈ ℂ)
10097, 99mulcld 10007 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℂ)
10195, 100addcomd 10185 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))
102101eqeq2d 2631 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))))
1031022rexbidva 3049 . . . . . . . . . . . . 13 (𝜑 → (∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))))
10490, 103syl5bb 272 . . . . . . . . . . . 12 (𝜑 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))))
105104rabbidv 3177 . . . . . . . . . . 11 (𝜑 → {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})
10616, 105syl5eq 2667 . . . . . . . . . 10 (𝜑𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})
107106eleq2d 2684 . . . . . . . . 9 (𝜑 → ((abs‘𝐵) ∈ 𝑀 ↔ (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}))
10889, 107sylibrd 249 . . . . . . . 8 (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ 𝑀))
10916, 1, 2, 17, 18bezoutlem3 15185 . . . . . . . 8 (𝜑 → ((abs‘𝐵) ∈ 𝑀𝐺 ∥ (abs‘𝐵)))
110108, 109syld 47 . . . . . . 7 (𝜑 → (𝐵 ≠ 0 → 𝐺 ∥ (abs‘𝐵)))
111 dvdsabsb 14928 . . . . . . . 8 ((𝐺 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐺𝐵𝐺 ∥ (abs‘𝐵)))
11279, 2, 111syl2anc 692 . . . . . . 7 (𝜑 → (𝐺𝐵𝐺 ∥ (abs‘𝐵)))
113110, 112sylibrd 249 . . . . . 6 (𝜑 → (𝐵 ≠ 0 → 𝐺𝐵))
114113imp 445 . . . . 5 ((𝜑𝐵 ≠ 0) → 𝐺𝐵)
11587, 114, 85pm2.61ne 2875 . . . 4 (𝜑𝐺𝐵)
116 dvdslegcd 15153 . . . . 5 (((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐺𝐴𝐺𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵)))
11779, 1, 2, 18, 116syl31anc 1326 . . . 4 (𝜑 → ((𝐺𝐴𝐺𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵)))
11886, 115, 117mp2and 714 . . 3 (𝜑𝐺 ≤ (𝐴 gcd 𝐵))
1196nn0red 11299 . . . 4 (𝜑 → (𝐴 gcd 𝐵) ∈ ℝ)
12071nnred 10982 . . . 4 (𝜑𝐺 ∈ ℝ)
121119, 120letri3d 10126 . . 3 (𝜑 → ((𝐴 gcd 𝐵) = 𝐺 ↔ ((𝐴 gcd 𝐵) ≤ 𝐺𝐺 ≤ (𝐴 gcd 𝐵))))
12274, 118, 121mpbir2and 956 . 2 (𝜑 → (𝐴 gcd 𝐵) = 𝐺)
123122, 19eqeltrd 2698 1 (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wrex 2908  {crab 2911   class class class wbr 4615  cfv 5849  (class class class)co 6607  infcinf 8294  cc 9881  cr 9882  0cc0 9883   + caddc 9886   · cmul 9888   < clt 10021  cle 10022  cn 10967  cz 11324  abscabs 13911  cdvds 14910   gcd cgcd 15143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-er 7690  df-en 7903  df-dom 7904  df-sdom 7905  df-sup 8295  df-inf 8296  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-n0 11240  df-z 11325  df-uz 11635  df-rp 11780  df-fl 12536  df-mod 12612  df-seq 12745  df-exp 12804  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-dvds 14911  df-gcd 15144
This theorem is referenced by:  bezout  15187
  Copyright terms: Public domain W3C validator