Step | Hyp | Ref
| Expression |
1 | | gcd0val 11902 |
. . 3
⊢ (0 gcd 0)
= 0 |
2 | | simprl 526 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑀 = 0) |
3 | | simprr 527 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → 𝑁 = 0) |
4 | 2, 3 | oveq12d 5868 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (0 gcd 0)) |
5 | | 0nn0 9137 |
. . . . 5
⊢ 0 ∈
ℕ0 |
6 | 5 | a1i 9 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → 0 ∈
ℕ0) |
7 | | 0dvds 11760 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (0
∥ 𝑀 ↔ 𝑀 = 0)) |
8 | 7 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (0 ∥ 𝑀 ↔ 𝑀 = 0)) |
9 | 2, 8 | mpbird 166 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → 0 ∥ 𝑀) |
10 | | 0dvds 11760 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) |
11 | 10 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (0 ∥ 𝑁 ↔ 𝑁 = 0)) |
12 | 3, 11 | mpbird 166 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → 0 ∥ 𝑁) |
13 | 9, 12 | jca 304 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) |
14 | 13 | ad2antrr 485 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)) |
15 | | 0z 9210 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
16 | | breq1 3990 |
. . . . . . . . . . 11
⊢ (𝑧 = 0 → (𝑧 ∥ 𝑑 ↔ 0 ∥ 𝑑)) |
17 | | breq1 3990 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → (𝑧 ∥ 𝑀 ↔ 0 ∥ 𝑀)) |
18 | | breq1 3990 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → (𝑧 ∥ 𝑁 ↔ 0 ∥ 𝑁)) |
19 | 17, 18 | anbi12d 470 |
. . . . . . . . . . 11
⊢ (𝑧 = 0 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))) |
20 | 16, 19 | bibi12d 234 |
. . . . . . . . . 10
⊢ (𝑧 = 0 → ((𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ (0 ∥ 𝑑 ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))) |
21 | 20 | rspcv 2830 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → (∀𝑧
∈ ℤ (𝑧 ∥
𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → (0 ∥ 𝑑 ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁)))) |
22 | 15, 21 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) → (0 ∥ 𝑑 ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))) |
23 | 22 | adantl 275 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (0 ∥ 𝑑 ↔ (0 ∥ 𝑀 ∧ 0 ∥ 𝑁))) |
24 | 14, 23 | mpbird 166 |
. . . . . 6
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 0 ∥ 𝑑) |
25 | | simplr 525 |
. . . . . . . 8
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 ∈ ℕ0) |
26 | 25 | nn0zd 9319 |
. . . . . . 7
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 ∈ ℤ) |
27 | | 0dvds 11760 |
. . . . . . 7
⊢ (𝑑 ∈ ℤ → (0
∥ 𝑑 ↔ 𝑑 = 0)) |
28 | 26, 27 | syl 14 |
. . . . . 6
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → (0 ∥ 𝑑 ↔ 𝑑 = 0)) |
29 | 24, 28 | mpbid 146 |
. . . . 5
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ ∀𝑧 ∈
ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) → 𝑑 = 0) |
30 | | dvds0 11755 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℤ → 𝑧 ∥ 0) |
31 | 30 | adantl 275 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ 0) |
32 | | breq2 3991 |
. . . . . . . . 9
⊢ (𝑑 = 0 → (𝑧 ∥ 𝑑 ↔ 𝑧 ∥ 0)) |
33 | 32 | ad2antlr 486 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ 𝑑 ↔ 𝑧 ∥ 0)) |
34 | 31, 33 | mpbird 166 |
. . . . . . 7
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ 𝑑) |
35 | 2 | ad3antrrr 489 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑀 = 0) |
36 | 31, 35 | breqtrrd 4015 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ 𝑀) |
37 | 3 | ad3antrrr 489 |
. . . . . . . . 9
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑁 = 0) |
38 | 31, 37 | breqtrrd 4015 |
. . . . . . . 8
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → 𝑧 ∥ 𝑁) |
39 | 36, 38 | jca 304 |
. . . . . . 7
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) |
40 | 34, 39 | 2thd 174 |
. . . . . 6
⊢
((((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) ∧ 𝑧 ∈ ℤ) → (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
41 | 40 | ralrimiva 2543 |
. . . . 5
⊢
(((((𝑀 ∈
ℤ ∧ 𝑁 ∈
ℤ) ∧ (𝑀 = 0 ∧
𝑁 = 0)) ∧ 𝑑 ∈ ℕ0)
∧ 𝑑 = 0) →
∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
42 | 29, 41 | impbida 591 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) ∧ 𝑑 ∈ ℕ0) →
(∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)) ↔ 𝑑 = 0)) |
43 | 6, 42 | riota5 5831 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (℩𝑑 ∈ ℕ0
∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) = 0) |
44 | 1, 4, 43 | 3eqtr4a 2229 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
45 | | bezoutlembi 11947 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∃𝑟 ∈
ℕ0 (∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑟 = ((𝑀 · 𝑎) + (𝑁 · 𝑏)))) |
46 | | simpl 108 |
. . . . . 6
⊢
((∀𝑤 ∈
ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑟 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))) → ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
47 | 46 | reximi 2567 |
. . . . 5
⊢
(∃𝑟 ∈
ℕ0 (∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑟 = ((𝑀 · 𝑎) + (𝑁 · 𝑏))) → ∃𝑟 ∈ ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
48 | 45, 47 | syl 14 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∃𝑟 ∈
ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
49 | 48 | adantr 274 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑟 ∈ ℕ0
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
50 | | simplll 528 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → 𝑀 ∈ ℤ) |
51 | | simpllr 529 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → 𝑁 ∈ ℤ) |
52 | | simprl 526 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → 𝑟 ∈ ℕ0) |
53 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∥ 𝑟 ↔ 𝑧 ∥ 𝑟)) |
54 | | breq1 3990 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑤 ∥ 𝑀 ↔ 𝑧 ∥ 𝑀)) |
55 | | breq1 3990 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (𝑤 ∥ 𝑁 ↔ 𝑧 ∥ 𝑁)) |
56 | 54, 55 | anbi12d 470 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁) ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
57 | 53, 56 | bibi12d 234 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ((𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ (𝑧 ∥ 𝑟 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
58 | 57 | cbvralv 2696 |
. . . . . . 7
⊢
(∀𝑤 ∈
ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑟 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
59 | 58 | biimpi 119 |
. . . . . 6
⊢
(∀𝑤 ∈
ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑟 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
60 | 59 | ad2antll 488 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑟 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
61 | | simplr 525 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → ¬ (𝑀 = 0 ∧ 𝑁 = 0)) |
62 | 50, 51, 52, 60, 61 | bezoutlemsup 11951 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → 𝑟 = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}, ℝ, < )) |
63 | | breq1 3990 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑤 ∥ 𝑑 ↔ 𝑧 ∥ 𝑑)) |
64 | 63, 56 | bibi12d 234 |
. . . . . . . 8
⊢ (𝑤 = 𝑧 → ((𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
65 | 64 | cbvralv 2696 |
. . . . . . 7
⊢
(∀𝑤 ∈
ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
66 | 65 | a1i 9 |
. . . . . 6
⊢ (𝑑 ∈ ℕ0
→ (∀𝑤 ∈
ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
67 | 66 | riotabiia 5823 |
. . . . 5
⊢
(℩𝑑
∈ ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) |
68 | | simprr 527 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
69 | 50, 51, 52, 68 | bezoutlemeu 11949 |
. . . . . . 7
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → ∃!𝑑 ∈ ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) |
70 | | breq2 3991 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑟 → (𝑤 ∥ 𝑑 ↔ 𝑤 ∥ 𝑟)) |
71 | 70 | bibi1d 232 |
. . . . . . . . 9
⊢ (𝑑 = 𝑟 → ((𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) |
72 | 71 | ralbidv 2470 |
. . . . . . . 8
⊢ (𝑑 = 𝑟 → (∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) |
73 | 72 | riota2 5828 |
. . . . . . 7
⊢ ((𝑟 ∈ ℕ0
∧ ∃!𝑑 ∈
ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) → (∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ (℩𝑑 ∈ ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) = 𝑟)) |
74 | 52, 69, 73 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → (∀𝑤 ∈ ℤ (𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)) ↔ (℩𝑑 ∈ ℕ0 ∀𝑤 ∈ ℤ (𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) = 𝑟)) |
75 | 68, 74 | mpbid 146 |
. . . . 5
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → (℩𝑑 ∈ ℕ0
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑑 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁))) = 𝑟) |
76 | 67, 75 | eqtr3id 2217 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → (℩𝑑 ∈ ℕ0
∀𝑧 ∈ ℤ
(𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))) = 𝑟) |
77 | | gcdn0val 11903 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}, ℝ, < )) |
78 | 77 | adantr 274 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → (𝑀 gcd 𝑁) = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}, ℝ, < )) |
79 | 62, 76, 78 | 3eqtr4rd 2214 |
. . 3
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑟 ∈ ℕ0 ∧
∀𝑤 ∈ ℤ
(𝑤 ∥ 𝑟 ↔ (𝑤 ∥ 𝑀 ∧ 𝑤 ∥ 𝑁)))) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
80 | 49, 79 | rexlimddv 2592 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |
81 | | gcdmndc 11886 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
DECID (𝑀 = 0
∧ 𝑁 =
0)) |
82 | | exmiddc 831 |
. . 3
⊢
(DECID (𝑀 = 0 ∧ 𝑁 = 0) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) |
83 | 81, 82 | syl 14 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 = 0 ∧ 𝑁 = 0) ∨ ¬ (𝑀 = 0 ∧ 𝑁 = 0))) |
84 | 44, 80, 83 | mpjaodan 793 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) |