Step | Hyp | Ref
| Expression |
1 | | gcdcllem2.2 |
. . . . 5
⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} |
2 | 1 | ssrab3 3995 |
. . . 4
⊢ 𝑅 ⊆
ℤ |
3 | | prssi 4734 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → {𝑀, 𝑁} ⊆ ℤ) |
4 | | neorian 3036 |
. . . . . . . 8
⊢ ((𝑀 ≠ 0 ∨ 𝑁 ≠ 0) ↔ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) |
5 | | prid1g 4676 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ {𝑀, 𝑁}) |
6 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑀 → (𝑛 ≠ 0 ↔ 𝑀 ≠ 0)) |
7 | 6 | rspcev 3537 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ {𝑀, 𝑁} ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
8 | 5, 7 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
9 | 8 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
10 | | prid2g 4677 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ {𝑀, 𝑁}) |
11 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑛 ≠ 0 ↔ 𝑁 ≠ 0)) |
12 | 11 | rspcev 3537 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ {𝑀, 𝑁} ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
13 | 10, 12 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
14 | 13 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
15 | 9, 14 | jaodan 958 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∨ 𝑁 ≠ 0)) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
16 | 4, 15 | sylan2br 598 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
17 | | gcdcllem2.1 |
. . . . . . . 8
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} |
18 | 17 | gcdcllem1 16058 |
. . . . . . 7
⊢ (({𝑀, 𝑁} ⊆ ℤ ∧ ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
19 | 3, 16, 18 | syl2an2r 685 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
20 | 17, 1 | gcdcllem2 16059 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆) |
21 | | neeq1 3003 |
. . . . . . . . 9
⊢ (𝑅 = 𝑆 → (𝑅 ≠ ∅ ↔ 𝑆 ≠ ∅)) |
22 | | raleq 3319 |
. . . . . . . . . 10
⊢ (𝑅 = 𝑆 → (∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
23 | 22 | rexbidv 3216 |
. . . . . . . . 9
⊢ (𝑅 = 𝑆 → (∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
24 | 21, 23 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑅 = 𝑆 → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
25 | 20, 24 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
26 | 25 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
27 | 19, 26 | mpbird 260 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥)) |
28 | | suprzcl2 12534 |
. . . . . 6
⊢ ((𝑅 ⊆ ℤ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
29 | 2, 28 | mp3an1 1450 |
. . . . 5
⊢ ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
30 | 27, 29 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
31 | 2, 30 | sselid 3898 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈
ℤ) |
32 | 27 | simprd 499 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) |
33 | | 1dvds 15832 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 1 ∥
𝑀) |
34 | | 1dvds 15832 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∥
𝑁) |
35 | 33, 34 | anim12i 616 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1
∥ 𝑀 ∧ 1 ∥
𝑁)) |
36 | | 1z 12207 |
. . . . . . 7
⊢ 1 ∈
ℤ |
37 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑧 ∥ 𝑀 ↔ 1 ∥ 𝑀)) |
38 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑧 ∥ 𝑁 ↔ 1 ∥ 𝑁)) |
39 | 37, 38 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑧 = 1 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (1 ∥ 𝑀 ∧ 1 ∥ 𝑁))) |
40 | 39, 1 | elrab2 3605 |
. . . . . . 7
⊢ (1 ∈
𝑅 ↔ (1 ∈ ℤ
∧ (1 ∥ 𝑀 ∧ 1
∥ 𝑁))) |
41 | 36, 40 | mpbiran 709 |
. . . . . 6
⊢ (1 ∈
𝑅 ↔ (1 ∥ 𝑀 ∧ 1 ∥ 𝑁)) |
42 | 35, 41 | sylibr 237 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈
𝑅) |
43 | 42 | adantr 484 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → 1 ∈ 𝑅) |
44 | | suprzub 12535 |
. . . 4
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 1 ∈ 𝑅) → 1 ≤ sup(𝑅, ℝ, < )) |
45 | 2, 32, 43, 44 | mp3an2i 1468 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → 1 ≤ sup(𝑅, ℝ, <
)) |
46 | | elnnz1 12203 |
. . 3
⊢
(sup(𝑅, ℝ,
< ) ∈ ℕ ↔ (sup(𝑅, ℝ, < ) ∈ ℤ ∧ 1
≤ sup(𝑅, ℝ, <
))) |
47 | 31, 45, 46 | sylanbrc 586 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈
ℕ) |
48 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = sup(𝑅, ℝ, < ) → (𝑥 ∥ 𝑀 ↔ sup(𝑅, ℝ, < ) ∥ 𝑀)) |
49 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = sup(𝑅, ℝ, < ) → (𝑥 ∥ 𝑁 ↔ sup(𝑅, ℝ, < ) ∥ 𝑁)) |
50 | 48, 49 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = sup(𝑅, ℝ, < ) → ((𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁) ↔ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
51 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ∥ 𝑀 ↔ 𝑥 ∥ 𝑀)) |
52 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ∥ 𝑁 ↔ 𝑥 ∥ 𝑁)) |
53 | 51, 52 | anbi12d 634 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁))) |
54 | 53 | cbvrabv 3402 |
. . . . . 6
⊢ {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁)} |
55 | 1, 54 | eqtri 2765 |
. . . . 5
⊢ 𝑅 = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁)} |
56 | 50, 55 | elrab2 3605 |
. . . 4
⊢
(sup(𝑅, ℝ,
< ) ∈ 𝑅 ↔
(sup(𝑅, ℝ, < )
∈ ℤ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
57 | 30, 56 | sylib 221 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℤ
∧ (sup(𝑅, ℝ, <
) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
58 | 57 | simprd 499 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁)) |
59 | | breq1 5056 |
. . . . . . 7
⊢ (𝑧 = 𝐾 → (𝑧 ∥ 𝑀 ↔ 𝐾 ∥ 𝑀)) |
60 | | breq1 5056 |
. . . . . . 7
⊢ (𝑧 = 𝐾 → (𝑧 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁)) |
61 | 59, 60 | anbi12d 634 |
. . . . . 6
⊢ (𝑧 = 𝐾 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
62 | 61, 1 | elrab2 3605 |
. . . . 5
⊢ (𝐾 ∈ 𝑅 ↔ (𝐾 ∈ ℤ ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
63 | 62 | biimpri 231 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ∈ 𝑅) |
64 | 63 | 3impb 1117 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∈ 𝑅) |
65 | | suprzub 12535 |
. . . . 5
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 𝐾 ∈ 𝑅) → 𝐾 ≤ sup(𝑅, ℝ, < )) |
66 | 65 | 3expia 1123 |
. . . 4
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → (𝐾 ∈ 𝑅 → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
67 | 2, 66 | mpan 690 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∀𝑦 ∈
𝑅 𝑦 ≤ 𝑥 → (𝐾 ∈ 𝑅 → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
68 | 32, 64, 67 | syl2im 40 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
69 | 47, 58, 68 | 3jca 1130 |
1
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ
∧ (sup(𝑅, ℝ, <
) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < )))) |