Step | Hyp | Ref
| Expression |
1 | | bezout.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
2 | | bezout.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) |
3 | | gcddvds 15063 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
4 | 1, 2, 3 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
5 | 4 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐴) |
6 | 1, 2 | gcdcld 15068 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈
ℕ0) |
7 | 6 | nn0zd 11356 |
. . . . . . 7
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℤ) |
8 | | divides 14823 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴)) |
9 | 7, 1, 8 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴)) |
10 | 5, 9 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴) |
11 | 4 | simprd 478 |
. . . . . 6
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐵) |
12 | | divides 14823 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)) |
13 | 7, 2, 12 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)) |
14 | 11, 13 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) |
15 | | reeanv 3086 |
. . . . . 6
⊢
(∃𝑠 ∈
ℤ ∃𝑡 ∈
ℤ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) ↔ (∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)) |
16 | | bezout.1 |
. . . . . . . . . . 11
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} |
17 | | bezout.2 |
. . . . . . . . . . 11
⊢ 𝐺 = inf(𝑀, ℝ, < ) |
18 | | bezout.5 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
19 | 16, 1, 2, 17, 18 | bezoutlem2 15095 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ 𝑀) |
20 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) |
21 | 20 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑦))) |
22 | 21 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦)))) |
23 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (𝐵 · 𝑦) = (𝐵 · 𝑣)) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → ((𝐴 · 𝑢) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
25 | 24 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
26 | 22, 25 | cbvrex2v 3156 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
27 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐺 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
28 | 27 | 2rexbidv 3039 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐺 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
29 | 26, 28 | syl5bb 271 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐺 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
30 | 29, 16 | elrab2 3333 |
. . . . . . . . . 10
⊢ (𝐺 ∈ 𝑀 ↔ (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
31 | 19, 30 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
32 | 31 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
33 | | simprrl 800 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℤ) |
34 | | simprll 798 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℤ) |
35 | 33, 34 | zmulcld 11364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℤ) |
36 | | simprrr 801 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℤ) |
37 | | simprlr 799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℤ) |
38 | 36, 37 | zmulcld 11364 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℤ) |
39 | 35, 38 | zaddcld 11362 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ) |
40 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℤ) |
41 | | dvdsmul2 14842 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵))) |
42 | 39, 40, 41 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵))) |
43 | 35 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℂ) |
44 | 38 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℂ) |
45 | 40 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℂ) |
46 | 43, 44, 45 | adddird 9944 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)) = (((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) + ((𝑡 · 𝑣) · (𝐴 gcd 𝐵)))) |
47 | 33 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℂ) |
48 | 34 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℂ) |
49 | 47, 48, 45 | mul32d 10125 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) = ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢)) |
50 | 36 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℂ) |
51 | 37 | zcnd 11359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℂ) |
52 | 50, 51, 45 | mul32d 10125 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑡 · 𝑣) · (𝐴 gcd 𝐵)) = ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) |
53 | 49, 52 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) + ((𝑡 · 𝑣) · (𝐴 gcd 𝐵))) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
54 | 46, 53 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
55 | 42, 54 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
56 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) = (𝐴 · 𝑢)) |
57 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣) = (𝐵 · 𝑣)) |
58 | 56, 57 | oveqan12d 6568 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
59 | 58 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → ((𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
60 | 55, 59 | syl5ibcom 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
61 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝐴 gcd 𝐵) ∥ 𝐺 ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
62 | 61 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺) ↔ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣))))) |
63 | 60, 62 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))) |
64 | 63 | expr 641 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
65 | 64 | com23 84 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
66 | 65 | rexlimdvva 3020 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
67 | 32, 66 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))) |
68 | 67 | rexlimdvv 3019 |
. . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)) |
69 | 15, 68 | syl5bir 232 |
. . . . 5
⊢ (𝜑 → ((∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)) |
70 | 10, 14, 69 | mp2and 711 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐺) |
71 | 31 | simpld 474 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ℕ) |
72 | | dvdsle 14870 |
. . . . 5
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐺 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺)) |
73 | 7, 71, 72 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺)) |
74 | 70, 73 | mpd 15 |
. . 3
⊢ (𝜑 → (𝐴 gcd 𝐵) ≤ 𝐺) |
75 | | breq2 4587 |
. . . . 5
⊢ (𝐴 = 0 → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ 0)) |
76 | 16, 1, 2 | bezoutlem1 15094 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) |
77 | 16, 1, 2, 17, 18 | bezoutlem3 15096 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐴) ∈ 𝑀 → 𝐺 ∥ (abs‘𝐴))) |
78 | 76, 77 | syld 46 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ≠ 0 → 𝐺 ∥ (abs‘𝐴))) |
79 | 71 | nnzd 11357 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ℤ) |
80 | | dvdsabsb 14839 |
. . . . . . . 8
⊢ ((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ (abs‘𝐴))) |
81 | 79, 1, 80 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ (abs‘𝐴))) |
82 | 78, 81 | sylibrd 248 |
. . . . . 6
⊢ (𝜑 → (𝐴 ≠ 0 → 𝐺 ∥ 𝐴)) |
83 | 82 | imp 444 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐺 ∥ 𝐴) |
84 | | dvds0 14835 |
. . . . . 6
⊢ (𝐺 ∈ ℤ → 𝐺 ∥ 0) |
85 | 79, 84 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∥ 0) |
86 | 75, 83, 85 | pm2.61ne 2867 |
. . . 4
⊢ (𝜑 → 𝐺 ∥ 𝐴) |
87 | | breq2 4587 |
. . . . 5
⊢ (𝐵 = 0 → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ 0)) |
88 | | eqid 2610 |
. . . . . . . . . 10
⊢ {𝑧 ∈ ℕ ∣
∃𝑦 ∈ ℤ
∃𝑥 ∈ ℤ
𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} |
89 | 88, 2, 1 | bezoutlem1 15094 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
90 | | rexcom 3080 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) |
91 | 1 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ ℂ) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐴 ∈ ℂ) |
93 | | zcn 11259 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
94 | 93 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑥 ∈ ℂ) |
95 | 92, 94 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐴 · 𝑥) ∈ ℂ) |
96 | 2 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ ℂ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐵 ∈ ℂ) |
98 | | zcn 11259 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
99 | 98 | ad2antrl 760 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑦 ∈ ℂ) |
100 | 97, 99 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℂ) |
101 | 95, 100 | addcomd 10117 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐵 · 𝑦) + (𝐴 · 𝑥))) |
102 | 101 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
103 | 102 | 2rexbidva 3038 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
104 | 90, 103 | syl5bb 271 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
105 | 104 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
106 | 16, 105 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
107 | 106 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐵) ∈ 𝑀 ↔ (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
108 | 89, 107 | sylibrd 248 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ 𝑀)) |
109 | 16, 1, 2, 17, 18 | bezoutlem3 15096 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐵) ∈ 𝑀 → 𝐺 ∥ (abs‘𝐵))) |
110 | 108, 109 | syld 46 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ≠ 0 → 𝐺 ∥ (abs‘𝐵))) |
111 | | dvdsabsb 14839 |
. . . . . . . 8
⊢ ((𝐺 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ (abs‘𝐵))) |
112 | 79, 2, 111 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ (abs‘𝐵))) |
113 | 110, 112 | sylibrd 248 |
. . . . . 6
⊢ (𝜑 → (𝐵 ≠ 0 → 𝐺 ∥ 𝐵)) |
114 | 113 | imp 444 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 0) → 𝐺 ∥ 𝐵) |
115 | 87, 114, 85 | pm2.61ne 2867 |
. . . 4
⊢ (𝜑 → 𝐺 ∥ 𝐵) |
116 | | dvdslegcd 15064 |
. . . . 5
⊢ (((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵))) |
117 | 79, 1, 2, 18, 116 | syl31anc 1321 |
. . . 4
⊢ (𝜑 → ((𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵))) |
118 | 86, 115, 117 | mp2and 711 |
. . 3
⊢ (𝜑 → 𝐺 ≤ (𝐴 gcd 𝐵)) |
119 | 6 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℝ) |
120 | 71 | nnred 10912 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ℝ) |
121 | 119, 120 | letri3d 10058 |
. . 3
⊢ (𝜑 → ((𝐴 gcd 𝐵) = 𝐺 ↔ ((𝐴 gcd 𝐵) ≤ 𝐺 ∧ 𝐺 ≤ (𝐴 gcd 𝐵)))) |
122 | 74, 118, 121 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝐴 gcd 𝐵) = 𝐺) |
123 | 122, 19 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀) |