Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. . 3
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆
ℕ |
2 | | breq2 4587 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑟↑2) ∥ 𝑛 ↔ (𝑟↑2) ∥ 𝑁)) |
3 | 2 | rabbidv 3164 |
. . . . . 6
⊢ (𝑛 = 𝑁 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
4 | 3 | supeq1d 8235 |
. . . . 5
⊢ (𝑛 = 𝑁 → sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
5 | | prmreclem1.1 |
. . . . 5
⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, <
)) |
6 | | ltso 9997 |
. . . . . 6
⊢ < Or
ℝ |
7 | 6 | supex 8252 |
. . . . 5
⊢
sup({𝑟 ∈
ℕ ∣ (𝑟↑2)
∥ 𝑁}, ℝ, < )
∈ V |
8 | 4, 5, 7 | fvmpt 6191 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
9 | | nnssz 11274 |
. . . . . . 7
⊢ ℕ
⊆ ℤ |
10 | 1, 9 | sstri 3577 |
. . . . . 6
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆
ℤ |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆
ℤ) |
12 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∈
ℕ) |
14 | | nnz 11276 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
15 | | 1dvds 14834 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → 1 ∥
𝑁) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 1 ∥
𝑁) |
17 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑟 = 1 → (𝑟↑2) = (1↑2)) |
18 | | sq1 12820 |
. . . . . . . . . 10
⊢
(1↑2) = 1 |
19 | 17, 18 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑟 = 1 → (𝑟↑2) = 1) |
20 | 19 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑟 = 1 → ((𝑟↑2) ∥ 𝑁 ↔ 1 ∥ 𝑁)) |
21 | 20 | elrab 3331 |
. . . . . . 7
⊢ (1 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁} ↔ (1 ∈ ℕ ∧
1 ∥ 𝑁)) |
22 | 13, 16, 21 | sylanbrc 695 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}) |
23 | | ne0i 3880 |
. . . . . 6
⊢ (1 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁} → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ≠ ∅) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ≠ ∅) |
25 | | nnz 11276 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
26 | | zsqcl 12796 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈
ℤ) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℕ → (𝑧↑2) ∈
ℤ) |
28 | | id 22 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
29 | | dvdsle 14870 |
. . . . . . . . . 10
⊢ (((𝑧↑2) ∈ ℤ ∧
𝑁 ∈ ℕ) →
((𝑧↑2) ∥ 𝑁 → (𝑧↑2) ≤ 𝑁)) |
30 | 27, 28, 29 | syl2anr 494 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ∥ 𝑁 → (𝑧↑2) ≤ 𝑁)) |
31 | | nnlesq 12830 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ≤ (𝑧↑2)) |
32 | 31 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑧 ≤ (𝑧↑2)) |
33 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
34 | 33 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑧 ∈
ℝ) |
35 | 34 | resqcld 12897 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧↑2) ∈
ℝ) |
36 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
37 | 36 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → 𝑁 ∈
ℝ) |
38 | | letr 10010 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ (𝑧↑2) ∈ ℝ ∧
𝑁 ∈ ℝ) →
((𝑧 ≤ (𝑧↑2) ∧ (𝑧↑2) ≤ 𝑁) → 𝑧 ≤ 𝑁)) |
39 | 34, 35, 37, 38 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 ≤ (𝑧↑2) ∧ (𝑧↑2) ≤ 𝑁) → 𝑧 ≤ 𝑁)) |
40 | 32, 39 | mpand 707 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ≤ 𝑁 → 𝑧 ≤ 𝑁)) |
41 | 30, 40 | syld 46 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
42 | 41 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ ℕ
((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
43 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑟 = 𝑧 → (𝑟↑2) = (𝑧↑2)) |
44 | 43 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑟 = 𝑧 → ((𝑟↑2) ∥ 𝑁 ↔ (𝑧↑2) ∥ 𝑁)) |
45 | 44 | ralrab 3335 |
. . . . . . 7
⊢
(∀𝑧 ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁 ↔ ∀𝑧 ∈ ℕ ((𝑧↑2) ∥ 𝑁 → 𝑧 ≤ 𝑁)) |
46 | 42, 45 | sylibr 223 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁) |
47 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑧 ≤ 𝑥 ↔ 𝑧 ≤ 𝑁)) |
48 | 47 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥 ↔ ∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁)) |
49 | 48 | rspcev 3282 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑁) → ∃𝑥 ∈ ℤ ∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
50 | 14, 46, 49 | syl2anc 691 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
51 | | suprzcl2 11654 |
. . . . 5
⊢ (({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆ ℤ ∧ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ≠ ∅ ∧
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) → sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < ) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
52 | 11, 24, 50, 51 | syl3anc 1318 |
. . . 4
⊢ (𝑁 ∈ ℕ →
sup({𝑟 ∈ ℕ
∣ (𝑟↑2) ∥
𝑁}, ℝ, < ) ∈
{𝑟 ∈ ℕ ∣
(𝑟↑2) ∥ 𝑁}) |
53 | 8, 52 | eqeltrd 2688 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
54 | 1, 53 | sseldi 3566 |
. 2
⊢ (𝑁 ∈ ℕ → (𝑄‘𝑁) ∈ ℕ) |
55 | | oveq1 6556 |
. . . . . 6
⊢ (𝑧 = (𝑄‘𝑁) → (𝑧↑2) = ((𝑄‘𝑁)↑2)) |
56 | 55 | breq1d 4593 |
. . . . 5
⊢ (𝑧 = (𝑄‘𝑁) → ((𝑧↑2) ∥ 𝑁 ↔ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
57 | 44 | cbvrabv 3172 |
. . . . 5
⊢ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} = {𝑧 ∈ ℕ ∣ (𝑧↑2) ∥ 𝑁} |
58 | 56, 57 | elrab2 3333 |
. . . 4
⊢ ((𝑄‘𝑁) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ↔ ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
59 | 53, 58 | sylib 207 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁)) |
60 | 59 | simprd 478 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∥ 𝑁) |
61 | 54 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℕ) |
62 | 61 | nncnd 10913 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℂ) |
63 | 62 | mulid1d 9936 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 1) = (𝑄‘𝑁)) |
64 | | eluz2b2 11637 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘2) ↔ (𝐾 ∈ ℕ ∧ 1 < 𝐾)) |
65 | 64 | simprbi 479 |
. . . . . . . 8
⊢ (𝐾 ∈
(ℤ≥‘2) → 1 < 𝐾) |
66 | 65 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 1 < 𝐾) |
67 | | 1red 9934 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 1 ∈ ℝ) |
68 | | eluz2nn 11602 |
. . . . . . . . . 10
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
69 | 68 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 𝐾 ∈ ℕ) |
70 | 69 | nnred 10912 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 𝐾 ∈ ℝ) |
71 | 61 | nnred 10912 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) ∈ ℝ) |
72 | 61 | nngt0d 10941 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → 0 < (𝑄‘𝑁)) |
73 | | ltmul2 10753 |
. . . . . . . 8
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ ((𝑄‘𝑁) ∈ ℝ ∧ 0 < (𝑄‘𝑁))) → (1 < 𝐾 ↔ ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾))) |
74 | 67, 70, 71, 72, 73 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (1 < 𝐾 ↔ ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾))) |
75 | 66, 74 | mpbid 221 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 1) < ((𝑄‘𝑁) · 𝐾)) |
76 | 63, 75 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → (𝑄‘𝑁) < ((𝑄‘𝑁) · 𝐾)) |
77 | | nnmulcl 10920 |
. . . . . . . 8
⊢ (((𝑄‘𝑁) ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
78 | 54, 68, 77 | syl2an 493 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
79 | 78 | nnred 10912 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) · 𝐾) ∈ ℝ) |
80 | 71, 79 | ltnled 10063 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ((𝑄‘𝑁) < ((𝑄‘𝑁) · 𝐾) ↔ ¬ ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁))) |
81 | 76, 80 | mpbid 221 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ¬ ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁)) |
82 | 10 | a1i 11 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆ ℤ) |
83 | 50 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ∃𝑥 ∈ ℤ ∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥) |
84 | 78 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ∈ ℕ) |
85 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) |
86 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝐾 ∈ ℕ) |
87 | 86 | nnsqcld 12891 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∈ ℕ) |
88 | | nnz 11276 |
. . . . . . . . . . 11
⊢ ((𝐾↑2) ∈ ℕ →
(𝐾↑2) ∈
ℤ) |
89 | 87, 88 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝐾↑2) ∈ ℤ) |
90 | 54 | nnsqcld 12891 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∈ ℕ) |
91 | 9, 90 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ∈ ℤ) |
92 | 90 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁)↑2) ≠ 0) |
93 | | dvdsval2 14824 |
. . . . . . . . . . . . 13
⊢ ((((𝑄‘𝑁)↑2) ∈ ℤ ∧ ((𝑄‘𝑁)↑2) ≠ 0 ∧ 𝑁 ∈ ℤ) → (((𝑄‘𝑁)↑2) ∥ 𝑁 ↔ (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ)) |
94 | 91, 92, 14, 93 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (((𝑄‘𝑁)↑2) ∥ 𝑁 ↔ (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ)) |
95 | 60, 94 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ) |
97 | 91 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℤ) |
98 | | dvdscmul 14846 |
. . . . . . . . . 10
⊢ (((𝐾↑2) ∈ ℤ ∧
(𝑁 / ((𝑄‘𝑁)↑2)) ∈ ℤ ∧ ((𝑄‘𝑁)↑2) ∈ ℤ) → ((𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))))) |
99 | 89, 96, 97, 98 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))))) |
100 | 85, 99 | mpd 15 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) ∥ (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2)))) |
101 | 62 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑄‘𝑁) ∈ ℂ) |
102 | 86 | nncnd 10913 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝐾 ∈ ℂ) |
103 | 101, 102 | sqmuld 12882 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁) · 𝐾)↑2) = (((𝑄‘𝑁)↑2) · (𝐾↑2))) |
104 | 103 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝐾↑2)) = (((𝑄‘𝑁) · 𝐾)↑2)) |
105 | | nncn 10905 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
106 | 105 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → 𝑁 ∈ ℂ) |
107 | 90 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℕ) |
108 | 107 | nncnd 10913 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ∈ ℂ) |
109 | 92 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁)↑2) ≠ 0) |
110 | 106, 108,
109 | divcan2d 10682 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁)↑2) · (𝑁 / ((𝑄‘𝑁)↑2))) = 𝑁) |
111 | 100, 104,
110 | 3brtr3d 4614 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (((𝑄‘𝑁) · 𝐾)↑2) ∥ 𝑁) |
112 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑟 = ((𝑄‘𝑁) · 𝐾) → (𝑟↑2) = (((𝑄‘𝑁) · 𝐾)↑2)) |
113 | 112 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑟 = ((𝑄‘𝑁) · 𝐾) → ((𝑟↑2) ∥ 𝑁 ↔ (((𝑄‘𝑁) · 𝐾)↑2) ∥ 𝑁)) |
114 | 113 | elrab 3331 |
. . . . . . 7
⊢ (((𝑄‘𝑁) · 𝐾) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ↔ (((𝑄‘𝑁) · 𝐾) ∈ ℕ ∧ (((𝑄‘𝑁) · 𝐾)↑2) ∥ 𝑁)) |
115 | 84, 111, 114 | sylanbrc 695 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) |
116 | | suprzub 11655 |
. . . . . 6
⊢ (({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁} ⊆ ℤ ∧
∃𝑥 ∈ ℤ
∀𝑧 ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}𝑧 ≤ 𝑥 ∧ ((𝑄‘𝑁) · 𝐾) ∈ {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}) → ((𝑄‘𝑁) · 𝐾) ≤ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
117 | 82, 83, 115, 116 | syl3anc 1318 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ≤ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
118 | 8 | ad2antrr 758 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → (𝑄‘𝑁) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑁}, ℝ, < )) |
119 | 117, 118 | breqtrrd 4611 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) ∧ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) → ((𝑄‘𝑁) · 𝐾) ≤ (𝑄‘𝑁)) |
120 | 81, 119 | mtand 689 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈
(ℤ≥‘2)) → ¬ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))) |
121 | 120 | ex 449 |
. 2
⊢ (𝑁 ∈ ℕ → (𝐾 ∈
(ℤ≥‘2) → ¬ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2)))) |
122 | 54, 60, 121 | 3jca 1235 |
1
⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁 ∧ (𝐾 ∈ (ℤ≥‘2)
→ ¬ (𝐾↑2)
∥ (𝑁 / ((𝑄‘𝑁)↑2))))) |