| Step | Hyp | Ref
| Expression |
| 1 | | ssrab2 4080 |
. . 3
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆
ℕ |
| 2 | | breq2 5147 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑟↑2) ∥ 𝑛 ↔ (𝑟↑2) ∥ 𝑁)) |
| 3 | 2 | rabbidv 3444 |
. . . . . 6
⊢ (𝑛 = 𝑁 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
| 4 | 3 | supeq1d 9486 |
. . . . 5
⊢ (𝑛 = 𝑁 → sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
| 5 | | prmreclem1.1 |
. . . . 5
⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, <
)) |
| 6 | | ltso 11341 |
. . . . . 6
⊢ < Or
ℝ |
| 7 | 6 | supex 9503 |
. . . . 5
⊢
sup({𝑟 ∈
ℕ ∣ (𝑟↑2)
∥ 𝑁}, ℝ, < )
∈ V |
| 8 | 4, 5, 7 | fvmpt 7016 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
| 9 | | nnssz 12635 |
. . . . . 6
⊢ ℕ
⊆ ℤ |
| 10 | 1, 9 | sstri 3993 |
. . . . 5
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆
ℤ |
| 11 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑟 = 1 → (𝑟↑2) = (1↑2)) |
| 12 | | sq1 14234 |
. . . . . . . . 9
⊢
(1↑2) = 1 |
| 13 | 11, 12 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑟 = 1 → (𝑟↑2) = 1) |
| 14 | 13 | breq1d 5153 |
. . . . . . 7
⊢ (𝑟 = 1 → ((𝑟↑2) ∥ 𝑁 ↔ 1 ∥ 𝑁)) |
| 15 | | 1nn 12277 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
| 16 | 15 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ) |
| 17 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
| 18 | | 1dvds 16308 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 1 ∥
𝑁) |
| 19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∥
𝑁) |
| 20 | 14, 16, 19 | elrabd 3694 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}) |
| 21 | 20 | ne0d 4342 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ≠ ∅) |
| 22 | | nnz 12634 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
| 23 | | zsqcl 14169 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (𝑧↑2) ∈
ℤ) |
| 25 | | id 22 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
| 26 | | dvdsle 16347 |
. . . . . . . . . 10
⊢ (((𝑧↑2) ∈ ℤ ∧
𝑁 ∈ ℕ) →
((𝑧↑2) ∥ 𝑁 → (𝑧↑2) ≤ 𝑁)) |
| 27 | 24, 25, 26 | syl2anr 597 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ∥ 𝑁 → (𝑧↑2) ≤ 𝑁)) |
| 28 | | nnlesq 14244 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ≤ (𝑧↑2)) |
| 29 | 28 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑧 ≤ (𝑧↑2)) |
| 30 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑧 ∈
ℝ) |
| 32 | 31 | resqcld 14165 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧↑2) ∈
ℝ) |
| 33 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑁 ∈
ℝ) |
| 35 | | letr 11355 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ (𝑧↑2) ∈ ℝ ∧
𝑁 ∈ ℝ) →
((𝑧 ≤ (𝑧↑2) ∧ (𝑧↑2) ≤ 𝑁) → 𝑧 ≤ 𝑁)) |
| 36 | 31, 32, 34, 35 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 ≤ (𝑧↑2) ∧ (𝑧↑2) ≤ 𝑁) → 𝑧 ≤ 𝑁)) |
| 37 | 29, 36 | mpand 695 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ≤ 𝑁 → 𝑧 ≤ 𝑁)) |
| 38 | 27, 37 | syld 47 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
| 39 | 38 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ ℕ
((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
| 40 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑟 = 𝑧 → (𝑟↑2) = (𝑧↑2)) |
| 41 | 40 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑟 = 𝑧 → ((𝑟↑2) ∥ 𝑁 ↔ (𝑧↑2) ∥ 𝑁)) |
| 42 | 41 | ralrab 3699 |
. . . . . . 7
⊢
(∀𝑧 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁 ↔ ∀𝑧 ∈ ℕ ((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
| 43 | 39, 42 | sylibr 234 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁) |
| 44 | | brralrspcev 5203 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℤ ∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
| 45 | 17, 43, 44 | syl2anc 584 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
| 46 | | suprzcl2 12980 |
. . . . 5
⊢ (({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆ ℤ ∧ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ≠ ∅ ∧
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) → sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < ) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
| 47 | 10, 21, 45, 46 | mp3an2i 1468 |
. . . 4
⊢ (𝑁 ∈ ℕ →
sup({𝑟 ∈ ℕ
∣ (𝑟↑2) ∥
𝑁}, ℝ, < ) ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}) |
| 48 | 8, 47 | eqeltrd 2841 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
| 49 | 1, 48 | sselid 3981 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) ∈ ℕ) |
| 50 | | oveq1 7438 |
. . . . . 6
⊢ (𝑧 = (𝑄‘𝑁) → (𝑧↑2) = ((𝑄‘𝑁)↑2)) |
| 51 | 50 | breq1d 5153 |
. . . . 5
⊢ (𝑧 = (𝑄‘𝑁) → ((𝑧↑2) ∥ 𝑁 ↔ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
| 52 | 41 | cbvrabv 3447 |
. . . . 5
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} = {𝑧 ∈ ℕ ∣ (𝑧↑2) ∥ 𝑁} |
| 53 | 51, 52 | elrab2 3695 |
. . . 4
⊢ ((𝑄‘𝑁) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ↔ ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
| 54 | 48, 53 | sylib 218 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
| 55 | 54 | simprd 495 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∥ 𝑁) |
| 56 | 49 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℕ) |
| 57 | 56 | nncnd 12282 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℂ) |
| 58 | 57 | mulridd 11278 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 1) = (𝑄‘𝑁)) |
| 59 | | eluz2gt1 12962 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘2) → 1 < 𝐾) |
| 60 | 59 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 1 < 𝐾) |
| 61 | | 1red 11262 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 1 ∈ ℝ) |
| 62 | | eluz2nn 12924 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
| 63 | 62 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 𝐾 ∈ ℕ) |
| 64 | 63 | nnred 12281 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 𝐾 ∈ ℝ) |
| 65 | 56 | nnred 12281 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℝ) |
| 66 | 56 | nngt0d 12315 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 0 < (𝑄‘𝑁)) |
| 67 | | ltmul2 12118 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ ((𝑄‘𝑁) ∈ ℝ ∧ 0 < (𝑄‘𝑁))) → (1 < 𝐾 ↔ ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾))) |
| 68 | 61, 64, 65, 66, 67 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (1 < 𝐾 ↔ ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾))) |
| 69 | 60, 68 | mpbid 232 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾)) |
| 70 | 58, 69 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) < ((𝑄‘𝑁) · 𝐾)) |
| 71 | | nnmulcl 12290 |
. . . . . . . 8
⊢ (((𝑄‘𝑁) ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
| 72 | 49, 62, 71 | syl2an 596 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
| 73 | 72 | nnred 12281 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 𝐾) ∈ ℝ) |
| 74 | 65, 73 | ltnled 11408 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) < ((𝑄‘𝑁) · 𝐾) ↔ ¬ ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁))) |
| 75 | 70, 74 | mpbid 232 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ¬ ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁)) |
| 76 | 45 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ∃𝑥 ∈ ℤ ∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
| 77 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑟 = ((𝑄‘𝑁) · 𝐾) → (𝑟↑2) = (((𝑄‘𝑁) · 𝐾)↑2)) |
| 78 | 77 | breq1d 5153 |
. . . . . . 7
⊢ (𝑟 = ((𝑄‘𝑁) · 𝐾) → ((𝑟↑2) ∥ 𝑁 ↔ (((𝑄‘𝑁) · 𝐾)↑2) ∥ 𝑁)) |
| 79 | 72 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
| 80 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) |
| 81 | 63 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝐾 ∈ ℕ) |
| 82 | 81 | nnsqcld 14283 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∈ ℕ) |
| 83 | | nnz 12634 |
. . . . . . . . . . 11
⊢ ((𝐾↑2) ∈ ℕ →
(𝐾↑2) ∈
ℤ) |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∈ ℤ) |
| 85 | 49 | nnsqcld 14283 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∈ ℕ) |
| 86 | 9, 85 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∈ ℤ) |
| 87 | 85 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ≠ 0) |
| 88 | | dvdsval2 16293 |
. . . . . . . . . . . . 13
⊢ ((((𝑄‘𝑁)↑2) ∈ ℤ ∧ ((𝑄‘𝑁)↑2) ≠ 0 ∧ 𝑁 ∈ ℤ) → (((𝑄‘𝑁)↑2) ∥ 𝑁 ↔ (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ)) |
| 89 | 86, 87, 17, 88 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑄‘𝑁)↑2) ∥ 𝑁 ↔ (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ)) |
| 90 | 55, 89 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ) |
| 91 | 90 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ) |
| 92 | 86 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℤ) |
| 93 | | dvdscmul 16320 |
. . . . . . . . . 10
⊢ (((𝐾↑2) ∈ ℤ ∧
(𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ ∧ ((𝑄‘𝑁)↑2) ∈ ℤ) → ((𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))))) |
| 94 | 84, 91, 92, 93 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))))) |
| 95 | 80, 94 | mpd 15 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2)))) |
| 96 | 57 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑄‘𝑁) ∈ ℂ) |
| 97 | 81 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝐾 ∈ ℂ) |
| 98 | 96, 97 | sqmuld 14198 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁) · 𝐾)↑2) = (((𝑄‘𝑁)↑2) · (𝐾↑2))) |
| 99 | 98 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) = (((𝑄‘𝑁) · 𝐾)↑2)) |
| 100 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 101 | 100 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝑁 ∈ ℂ) |
| 102 | 85 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℕ) |
| 103 | 102 | nncnd 12282 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℂ) |
| 104 | 87 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ≠ 0) |
| 105 | 101, 103,
104 | divcan2d 12045 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))) = 𝑁) |
| 106 | 95, 99, 105 | 3brtr3d 5174 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁) · 𝐾)↑2) ∥ 𝑁) |
| 107 | 78, 79, 106 | elrabd 3694 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
| 108 | | suprzub 12981 |
. . . . . 6
⊢ (({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥 ∧ ((𝑄‘𝑁) · 𝐾) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) → ((𝑄‘𝑁) · 𝐾) ≤ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
| 109 | 10, 76, 107, 108 | mp3an2i 1468 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ≤ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
| 110 | 8 | ad2antrr 726 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑄‘𝑁) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
| 111 | 109, 110 | breqtrrd 5171 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁)) |
| 112 | 75, 111 | mtand 816 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ¬ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) |
| 113 | 112 | ex 412 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐾 ∈
(ℤ≥‘2) → ¬ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)))) |
| 114 | 49, 55, 113 | 3jca 1129 |
1
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁 ∧ (𝐾 ∈ (ℤ≥‘2)
→ ¬ (𝐾↑2)
∥ (𝑁 / ((𝑄‘𝑁)↑2))))) |