Step | Hyp | Ref
| Expression |
1 | | bezout.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
2 | | bezout.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) |
3 | | gcddvds 16062 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
4 | 1, 2, 3 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
5 | 4 | simpld 498 |
. . . . . 6
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐴) |
6 | 1, 2 | gcdcld 16067 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈
ℕ0) |
7 | 6 | nn0zd 12280 |
. . . . . . 7
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℤ) |
8 | | divides 15817 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴)) |
9 | 7, 1, 8 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐴 ↔ ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴)) |
10 | 5, 9 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴) |
11 | 4 | simprd 499 |
. . . . . 6
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐵) |
12 | | divides 15817 |
. . . . . . 7
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)) |
13 | 7, 2, 12 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐵 ↔ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵)) |
14 | 11, 13 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) |
15 | | reeanv 3279 |
. . . . . 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 16100 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ 𝑀) |
20 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) |
21 | 20 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑦))) |
22 | 21 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦)))) |
23 | | oveq2 7221 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑣 → (𝐵 · 𝑦) = (𝐵 · 𝑣)) |
24 | 23 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑣 → ((𝐴 · 𝑢) + (𝐵 · 𝑦)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
25 | 24 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑣 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
26 | 22, 25 | cbvrex2vw 3372 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
27 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐺 → (𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
28 | 27 | 2rexbidv 3219 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐺 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝑧 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
29 | 26, 28 | syl5bb 286 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐺 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
30 | 29, 16 | elrab2 3605 |
. . . . . . . . . 10
⊢ (𝐺 ∈ 𝑀 ↔ (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
31 | 19, 30 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 ∈ ℕ ∧ ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
32 | 31 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
33 | | simprrl 781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℤ) |
34 | | simprll 779 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℤ) |
35 | 33, 34 | zmulcld 12288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℤ) |
36 | | simprrr 782 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℤ) |
37 | | simprlr 780 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℤ) |
38 | 36, 37 | zmulcld 12288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℤ) |
39 | 35, 38 | zaddcld 12286 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ) |
40 | 7 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℤ) |
41 | | dvdsmul2 15840 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑠 · 𝑢) + (𝑡 · 𝑣)) ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℤ) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵))) |
42 | 39, 40, 41 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵))) |
43 | 35 | zcnd 12283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑠 · 𝑢) ∈ ℂ) |
44 | 40 | zcnd 12283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∈ ℂ) |
45 | 38 | zcnd 12283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝑡 · 𝑣) ∈ ℂ) |
46 | 33 | zcnd 12283 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑠 ∈ ℂ) |
47 | 34 | zcnd 12283 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑢 ∈ ℂ) |
48 | 46, 47, 44 | mul32d 11042 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) = ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢)) |
49 | 36 | zcnd 12283 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑡 ∈ ℂ) |
50 | 37 | zcnd 12283 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → 𝑣 ∈ ℂ) |
51 | 49, 50, 44 | mul32d 11042 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → ((𝑡 · 𝑣) · (𝐴 gcd 𝐵)) = ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) |
52 | 48, 51 | oveq12d 7231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) · (𝐴 gcd 𝐵)) + ((𝑡 · 𝑣) · (𝐴 gcd 𝐵))) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
53 | 43, 44, 45, 52 | joinlmuladdmuld 10860 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · 𝑢) + (𝑡 · 𝑣)) · (𝐴 gcd 𝐵)) = (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
54 | 42, 53 | breqtrd 5079 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣))) |
55 | | oveq1 7220 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 → ((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) = (𝐴 · 𝑢)) |
56 | | oveq1 7220 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 · (𝐴 gcd 𝐵)) = 𝐵 → ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣) = (𝐵 · 𝑣)) |
57 | 55, 56 | oveqan12d 7232 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) = ((𝐴 · 𝑢) + (𝐵 · 𝑣))) |
58 | 57 | breq2d 5065 |
. . . . . . . . . . . . 13
⊢ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → ((𝐴 gcd 𝐵) ∥ (((𝑠 · (𝐴 gcd 𝐵)) · 𝑢) + ((𝑡 · (𝐴 gcd 𝐵)) · 𝑣)) ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
59 | 54, 58 | syl5ibcom 248 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
60 | | breq2 5057 |
. . . . . . . . . . . . 13
⊢ (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝐴 gcd 𝐵) ∥ 𝐺 ↔ (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣)))) |
61 | 60 | imbi2d 344 |
. . . . . . . . . . . 12
⊢ (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺) ↔ (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑢) + (𝐵 · 𝑣))))) |
62 | 59, 61 | syl5ibrcom 250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ) ∧ (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ))) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))) |
63 | 62 | expr 460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
64 | 63 | com23 86 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ ℤ ∧ 𝑣 ∈ ℤ)) → (𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
65 | 64 | rexlimdvva 3213 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑢 ∈ ℤ ∃𝑣 ∈ ℤ 𝐺 = ((𝐴 · 𝑢) + (𝐵 · 𝑣)) → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)))) |
66 | 32, 65 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → ((𝑠 ∈ ℤ ∧ 𝑡 ∈ ℤ) → (((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺))) |
67 | 66 | rexlimdvv 3212 |
. . . . . 6
⊢ (𝜑 → (∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ ((𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)) |
68 | 15, 67 | syl5bir 246 |
. . . . 5
⊢ (𝜑 → ((∃𝑠 ∈ ℤ (𝑠 · (𝐴 gcd 𝐵)) = 𝐴 ∧ ∃𝑡 ∈ ℤ (𝑡 · (𝐴 gcd 𝐵)) = 𝐵) → (𝐴 gcd 𝐵) ∥ 𝐺)) |
69 | 10, 14, 68 | mp2and 699 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐺) |
70 | 31 | simpld 498 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ℕ) |
71 | | dvdsle 15871 |
. . . . 5
⊢ (((𝐴 gcd 𝐵) ∈ ℤ ∧ 𝐺 ∈ ℕ) → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺)) |
72 | 7, 70, 71 | syl2anc 587 |
. . . 4
⊢ (𝜑 → ((𝐴 gcd 𝐵) ∥ 𝐺 → (𝐴 gcd 𝐵) ≤ 𝐺)) |
73 | 69, 72 | mpd 15 |
. . 3
⊢ (𝜑 → (𝐴 gcd 𝐵) ≤ 𝐺) |
74 | | breq2 5057 |
. . . . 5
⊢ (𝐴 = 0 → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ 0)) |
75 | 16, 1, 2 | bezoutlem1 16099 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) |
76 | 16, 1, 2, 17, 18 | bezoutlem3 16101 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐴) ∈ 𝑀 → 𝐺 ∥ (abs‘𝐴))) |
77 | 75, 76 | syld 47 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ≠ 0 → 𝐺 ∥ (abs‘𝐴))) |
78 | 70 | nnzd 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ℤ) |
79 | | dvdsabsb 15837 |
. . . . . . . 8
⊢ ((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ (abs‘𝐴))) |
80 | 78, 1, 79 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∥ 𝐴 ↔ 𝐺 ∥ (abs‘𝐴))) |
81 | 77, 80 | sylibrd 262 |
. . . . . 6
⊢ (𝜑 → (𝐴 ≠ 0 → 𝐺 ∥ 𝐴)) |
82 | 81 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → 𝐺 ∥ 𝐴) |
83 | | dvds0 15833 |
. . . . . 6
⊢ (𝐺 ∈ ℤ → 𝐺 ∥ 0) |
84 | 78, 83 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∥ 0) |
85 | 74, 82, 84 | pm2.61ne 3027 |
. . . 4
⊢ (𝜑 → 𝐺 ∥ 𝐴) |
86 | | breq2 5057 |
. . . . 5
⊢ (𝐵 = 0 → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ 0)) |
87 | | eqid 2737 |
. . . . . . . . . 10
⊢ {𝑧 ∈ ℕ ∣
∃𝑦 ∈ ℤ
∃𝑥 ∈ ℤ
𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))} |
88 | 87, 2, 1 | bezoutlem1 16099 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
89 | | rexcom 3268 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ ∃𝑦 ∈
ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) |
90 | 1 | zcnd 12283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ ℂ) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐴 ∈ ℂ) |
92 | | zcn 12181 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
93 | 92 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑥 ∈ ℂ) |
94 | 91, 93 | mulcld 10853 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐴 · 𝑥) ∈ ℂ) |
95 | 2 | zcnd 12283 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ ℂ) |
96 | 95 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝐵 ∈ ℂ) |
97 | | zcn 12181 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
98 | 97 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → 𝑦 ∈ ℂ) |
99 | 96, 98 | mulcld 10853 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝐵 · 𝑦) ∈ ℂ) |
100 | 94, 99 | addcomd 11034 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → ((𝐴 · 𝑥) + (𝐵 · 𝑦)) = ((𝐵 · 𝑦) + (𝐴 · 𝑥))) |
101 | 100 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ)) → (𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
102 | 101 | 2rexbidva 3218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
103 | 89, 102 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)) ↔ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥)))) |
104 | 103 | rabbidv 3390 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
105 | 16, 104 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))}) |
106 | 105 | eleq2d 2823 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐵) ∈ 𝑀 ↔ (abs‘𝐵) ∈ {𝑧 ∈ ℕ ∣ ∃𝑦 ∈ ℤ ∃𝑥 ∈ ℤ 𝑧 = ((𝐵 · 𝑦) + (𝐴 · 𝑥))})) |
107 | 88, 106 | sylibrd 262 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ≠ 0 → (abs‘𝐵) ∈ 𝑀)) |
108 | 16, 1, 2, 17, 18 | bezoutlem3 16101 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝐵) ∈ 𝑀 → 𝐺 ∥ (abs‘𝐵))) |
109 | 107, 108 | syld 47 |
. . . . . . 7
⊢ (𝜑 → (𝐵 ≠ 0 → 𝐺 ∥ (abs‘𝐵))) |
110 | | dvdsabsb 15837 |
. . . . . . . 8
⊢ ((𝐺 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ (abs‘𝐵))) |
111 | 78, 2, 110 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∥ 𝐵 ↔ 𝐺 ∥ (abs‘𝐵))) |
112 | 109, 111 | sylibrd 262 |
. . . . . 6
⊢ (𝜑 → (𝐵 ≠ 0 → 𝐺 ∥ 𝐵)) |
113 | 112 | imp 410 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ≠ 0) → 𝐺 ∥ 𝐵) |
114 | 86, 113, 84 | pm2.61ne 3027 |
. . . 4
⊢ (𝜑 → 𝐺 ∥ 𝐵) |
115 | | dvdslegcd 16063 |
. . . . 5
⊢ (((𝐺 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬
(𝐴 = 0 ∧ 𝐵 = 0)) → ((𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵))) |
116 | 78, 1, 2, 18, 115 | syl31anc 1375 |
. . . 4
⊢ (𝜑 → ((𝐺 ∥ 𝐴 ∧ 𝐺 ∥ 𝐵) → 𝐺 ≤ (𝐴 gcd 𝐵))) |
117 | 85, 114, 116 | mp2and 699 |
. . 3
⊢ (𝜑 → 𝐺 ≤ (𝐴 gcd 𝐵)) |
118 | 6 | nn0red 12151 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ ℝ) |
119 | 70 | nnred 11845 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ℝ) |
120 | 118, 119 | letri3d 10974 |
. . 3
⊢ (𝜑 → ((𝐴 gcd 𝐵) = 𝐺 ↔ ((𝐴 gcd 𝐵) ≤ 𝐺 ∧ 𝐺 ≤ (𝐴 gcd 𝐵)))) |
121 | 73, 117, 120 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝐴 gcd 𝐵) = 𝐺) |
122 | 121, 19 | eqeltrd 2838 |
1
⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀) |