| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpll1 1063 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ∈ ℤ) |
| 2 | 1 | zred 9699 |
. . . 4
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ∈ ℝ) |
| 3 | | simpll2 1064 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝑀 ∈ ℤ) |
| 4 | | simpll3 1065 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝑁 ∈ ℤ) |
| 5 | | simplr 529 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → ¬ (𝑀 = 0 ∧ 𝑁 = 0)) |
| 6 | | lttri3 8352 |
. . . . . . 7
⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
| 7 | 6 | adantl 277 |
. . . . . 6
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓))) |
| 8 | | zssre 9583 |
. . . . . . 7
⊢ ℤ
⊆ ℝ |
| 9 | | gcdsupex 12649 |
. . . . . . 7
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧))) |
| 10 | | ssrexv 3302 |
. . . . . . 7
⊢ (ℤ
⊆ ℝ → (∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧)))) |
| 11 | 8, 9, 10 | mpsyl 65 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}𝑦 < 𝑧))) |
| 12 | 7, 11 | supclti 7288 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) ∈
ℝ) |
| 13 | 3, 4, 5, 12 | syl21anc 1273 |
. . . 4
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) ∈
ℝ) |
| 14 | | simpr 110 |
. . . . . 6
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) |
| 15 | | breq1 4111 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑛 ∥ 𝑀 ↔ 𝐾 ∥ 𝑀)) |
| 16 | | breq1 4111 |
. . . . . . . . 9
⊢ (𝑛 = 𝐾 → (𝑛 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁)) |
| 17 | 15, 16 | anbi12d 473 |
. . . . . . . 8
⊢ (𝑛 = 𝐾 → ((𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁) ↔ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
| 18 | 17 | elrab3 2973 |
. . . . . . 7
⊢ (𝐾 ∈ ℤ → (𝐾 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
| 19 | 1, 18 | syl 14 |
. . . . . 6
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → (𝐾 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} ↔ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁))) |
| 20 | 14, 19 | mpbird 167 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}) |
| 21 | 7, 11 | supubti 7289 |
. . . . . 6
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝐾 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ¬ sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) < 𝐾)) |
| 22 | 3, 4, 5, 21 | syl21anc 1273 |
. . . . 5
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → (𝐾 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)} → ¬ sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) < 𝐾)) |
| 23 | 20, 22 | mpd 13 |
. . . 4
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → ¬ sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ) < 𝐾) |
| 24 | 2, 13, 23 | nltled 8393 |
. . 3
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ≤ sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
| 25 | | gcdn0val 12653 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
| 26 | 3, 4, 5, 25 | syl21anc 1273 |
. . 3
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → (𝑀 gcd 𝑁) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) |
| 27 | 24, 26 | breqtrrd 4136 |
. 2
⊢ ((((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) ∧ (𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁)) → 𝐾 ≤ (𝑀 gcd 𝑁)) |
| 28 | 27 | ex 115 |
1
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑀 = 0 ∧ 𝑁 = 0)) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ (𝑀 gcd 𝑁))) |
