Step | Hyp | Ref
| Expression |
1 | | gcdcllem2.2 |
. . . . 5
⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} |
2 | | ssrab2 3650 |
. . . . 5
⊢ {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} ⊆ ℤ |
3 | 1, 2 | eqsstri 3598 |
. . . 4
⊢ 𝑅 ⊆
ℤ |
4 | | prssi 4293 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → {𝑀, 𝑁} ⊆ ℤ) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → {𝑀, 𝑁} ⊆ ℤ) |
6 | | neorian 2876 |
. . . . . . . 8
⊢ ((𝑀 ≠ 0 ∨ 𝑁 ≠ 0) ↔ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) |
7 | | prid1g 4239 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → 𝑀 ∈ {𝑀, 𝑁}) |
8 | | neeq1 2844 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑀 → (𝑛 ≠ 0 ↔ 𝑀 ≠ 0)) |
9 | 8 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ {𝑀, 𝑁} ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
10 | 7, 9 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
11 | 10 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
12 | | prid2g 4240 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈ {𝑀, 𝑁}) |
13 | | neeq1 2844 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑛 ≠ 0 ↔ 𝑁 ≠ 0)) |
14 | 13 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ {𝑀, 𝑁} ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
15 | 12, 14 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
16 | 15 | adantll 746 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑁 ≠ 0) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
17 | 11, 16 | jaodan 822 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≠ 0 ∨ 𝑁 ≠ 0)) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
18 | 6, 17 | sylan2br 492 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) |
19 | | gcdcllem2.1 |
. . . . . . . 8
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} |
20 | 19 | gcdcllem1 15059 |
. . . . . . 7
⊢ (({𝑀, 𝑁} ⊆ ℤ ∧ ∃𝑛 ∈ {𝑀, 𝑁}𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
21 | 5, 18, 20 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
22 | 19, 1 | gcdcllem2 15060 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆) |
23 | | neeq1 2844 |
. . . . . . . . 9
⊢ (𝑅 = 𝑆 → (𝑅 ≠ ∅ ↔ 𝑆 ≠ ∅)) |
24 | | raleq 3115 |
. . . . . . . . . 10
⊢ (𝑅 = 𝑆 → (∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
25 | 24 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑅 = 𝑆 → (∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ↔ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) |
26 | 23, 25 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑅 = 𝑆 → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
27 | 22, 26 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
28 | 27 | adantr 480 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) ↔ (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))) |
29 | 21, 28 | mpbird 246 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥)) |
30 | | suprzcl2 11654 |
. . . . . 6
⊢ ((𝑅 ⊆ ℤ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
31 | 3, 30 | mp3an1 1403 |
. . . . 5
⊢ ((𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
32 | 29, 31 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈ 𝑅) |
33 | 3, 32 | sseldi 3566 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈
ℤ) |
34 | 3 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → 𝑅 ⊆ ℤ) |
35 | 29 | simprd 478 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) |
36 | | 1dvds 14834 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 1 ∥
𝑀) |
37 | | 1dvds 14834 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 1 ∥
𝑁) |
38 | 36, 37 | anim12i 588 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1
∥ 𝑀 ∧ 1 ∥
𝑁)) |
39 | | 1z 11284 |
. . . . . . 7
⊢ 1 ∈
ℤ |
40 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑧 ∥ 𝑀 ↔ 1 ∥ 𝑀)) |
41 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑧 = 1 → (𝑧 ∥ 𝑁 ↔ 1 ∥ 𝑁)) |
42 | 40, 41 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = 1 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (1 ∥ 𝑀 ∧ 1 ∥ 𝑁))) |
43 | 42, 1 | elrab2 3333 |
. . . . . . 7
⊢ (1 ∈
𝑅 ↔ (1 ∈ ℤ
∧ (1 ∥ 𝑀 ∧ 1
∥ 𝑁))) |
44 | 39, 43 | mpbiran 955 |
. . . . . 6
⊢ (1 ∈
𝑅 ↔ (1 ∥ 𝑀 ∧ 1 ∥ 𝑁)) |
45 | 38, 44 | sylibr 223 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 1 ∈
𝑅) |
46 | 45 | adantr 480 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → 1 ∈ 𝑅) |
47 | | suprzub 11655 |
. . . 4
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 1 ∈ 𝑅) → 1 ≤ sup(𝑅, ℝ, < )) |
48 | 34, 35, 46, 47 | syl3anc 1318 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → 1 ≤ sup(𝑅, ℝ, <
)) |
49 | | elnnz1 11280 |
. . 3
⊢
(sup(𝑅, ℝ,
< ) ∈ ℕ ↔ (sup(𝑅, ℝ, < ) ∈ ℤ ∧ 1
≤ sup(𝑅, ℝ, <
))) |
50 | 33, 48, 49 | sylanbrc 695 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup(𝑅, ℝ, < ) ∈
ℕ) |
51 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = sup(𝑅, ℝ, < ) → (𝑥 ∥ 𝑀 ↔ sup(𝑅, ℝ, < ) ∥ 𝑀)) |
52 | | breq1 4586 |
. . . . . 6
⊢ (𝑥 = sup(𝑅, ℝ, < ) → (𝑥 ∥ 𝑁 ↔ sup(𝑅, ℝ, < ) ∥ 𝑁)) |
53 | 51, 52 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = sup(𝑅, ℝ, < ) → ((𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁) ↔ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
54 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ∥ 𝑀 ↔ 𝑥 ∥ 𝑀)) |
55 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑧 ∥ 𝑁 ↔ 𝑥 ∥ 𝑁)) |
56 | 54, 55 | anbi12d 743 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁))) |
57 | 56 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁)} |
58 | 1, 57 | eqtri 2632 |
. . . . 5
⊢ 𝑅 = {𝑥 ∈ ℤ ∣ (𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁)} |
59 | 53, 58 | elrab2 3333 |
. . . 4
⊢
(sup(𝑅, ℝ,
< ) ∈ 𝑅 ↔
(sup(𝑅, ℝ, < )
∈ ℤ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
60 | 32, 59 | sylib 207 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℤ
∧ (sup(𝑅, ℝ, <
) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁))) |
61 | 60 | simprd 478 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁)) |
62 | | breq1 4586 |
. . . . . . 7
⊢ (𝑧 = 𝐾 → (𝑧 ∥ 𝑀 ↔ 𝐾 ∥ 𝑀)) |
63 | | breq1 4586 |
. . . . . . 7
⊢ (𝑧 = 𝐾 → (𝑧 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁)) |
64 | 62, 63 | anbi12d 743 |
. . . . . 6
⊢ (𝑧 = 𝐾 → ((𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁) ↔ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
65 | 64, 1 | elrab2 3333 |
. . . . 5
⊢ (𝐾 ∈ 𝑅 ↔ (𝐾 ∈ ℤ ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
66 | 65 | biimpri 217 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ∈ 𝑅) |
67 | 66 | 3impb 1252 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∈ 𝑅) |
68 | | suprzub 11655 |
. . . . 5
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥 ∧ 𝐾 ∈ 𝑅) → 𝐾 ≤ sup(𝑅, ℝ, < )) |
69 | 68 | 3expia 1259 |
. . . 4
⊢ ((𝑅 ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑦 ∈ 𝑅 𝑦 ≤ 𝑥) → (𝐾 ∈ 𝑅 → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
70 | 3, 69 | mpan 702 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∀𝑦 ∈
𝑅 𝑦 ≤ 𝑥 → (𝐾 ∈ 𝑅 → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
71 | 35, 67, 70 | syl2im 39 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < ))) |
72 | 50, 61, 71 | 3jca 1235 |
1
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ
∧ (sup(𝑅, ℝ, <
) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < )))) |