| Step | Hyp | Ref
| Expression |
| 1 | | nnex 12272 |
. . . 4
⊢ ℕ
∈ V |
| 2 | | inss1 4237 |
. . . . 5
⊢ (ℙ
∩ 𝑇) ⊆
ℙ |
| 3 | | prmssnn 16713 |
. . . . 5
⊢ ℙ
⊆ ℕ |
| 4 | 2, 3 | sstri 3993 |
. . . 4
⊢ (ℙ
∩ 𝑇) ⊆
ℕ |
| 5 | | ssdomg 9040 |
. . . 4
⊢ (ℕ
∈ V → ((ℙ ∩ 𝑇) ⊆ ℕ → (ℙ ∩
𝑇) ≼
ℕ)) |
| 6 | 1, 4, 5 | mp2 9 |
. . 3
⊢ (ℙ
∩ 𝑇) ≼
ℕ |
| 7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (ℙ ∩ 𝑇) ≼
ℕ) |
| 8 | | logno1 26678 |
. . . 4
⊢ ¬
(𝑥 ∈
ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) |
| 9 | | rpvmasum.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 𝑁 ∈
ℕ) |
| 11 | 10 | phicld 16809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℕ) |
| 12 | 11 | nnred 12281 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℝ) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (ϕ‘𝑁)
∈ ℝ) |
| 14 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (ℙ
∩ 𝑇) ∈
Fin) |
| 15 | | inss2 4238 |
. . . . . . . . . 10
⊢
((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇) |
| 16 | | ssfi 9213 |
. . . . . . . . . 10
⊢
(((ℙ ∩ 𝑇)
∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇)) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin) |
| 17 | 14, 15, 16 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
∈ Fin) |
| 18 | | elinel2 4202 |
. . . . . . . . . 10
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
→ 𝑛 ∈ (ℙ
∩ 𝑇)) |
| 19 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ (ℙ ∩ 𝑇)) |
| 20 | 4, 19 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℕ) |
| 21 | 20 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℝ+) |
| 22 | | relogcl 26617 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘𝑛) ∈
ℝ) |
| 24 | 23, 20 | nndivred 12320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → ((log‘𝑛) / 𝑛) ∈ ℝ) |
| 25 | 18, 24 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ ((log‘𝑛) /
𝑛) ∈
ℝ) |
| 26 | 17, 25 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
| 28 | | rpssre 13042 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
| 29 | 12 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℂ) |
| 30 | | o1const 15656 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℝ ∧ (ϕ‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
| 31 | 28, 29, 30 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
| 32 | 28 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
ℝ+ ⊆ ℝ) |
| 33 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 1 ∈
ℝ) |
| 34 | 14, 24 | fsumrecl 15770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈ (ℙ
∩ 𝑇)((log‘𝑛) / 𝑛) ∈ ℝ) |
| 35 | | log1 26627 |
. . . . . . . . . . . . 13
⊢
(log‘1) = 0 |
| 36 | 20 | nnge1d 12314 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 1 ≤ 𝑛) |
| 37 | | 1rp 13038 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ |
| 38 | | logleb 26645 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (1 ≤
𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
| 39 | 37, 21, 38 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (1 ≤ 𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
| 40 | 36, 39 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘1) ≤
(log‘𝑛)) |
| 41 | 35, 40 | eqbrtrrid 5179 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
(log‘𝑛)) |
| 42 | 23, 21, 41 | divge0d 13117 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
((log‘𝑛) / 𝑛)) |
| 43 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
⊆ (ℙ ∩ 𝑇)) |
| 44 | 14, 24, 42, 43 | fsumless 15832 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
| 45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ (𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
| 46 | 32, 27, 33, 34, 45 | ello1d 15559 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1)) |
| 47 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ∈
ℝ) |
| 48 | 18, 42 | sylan2 593 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ 0 ≤ ((log‘𝑛) / 𝑛)) |
| 49 | 17, 25, 48 | fsumge0 15831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ≤
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
| 50 | 49 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ 0 ≤ Σ𝑛
∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
| 51 | 27, 47, 50 | o1lo12 15574 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1))) |
| 52 | 46, 51 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
| 53 | 13, 27, 31, 52 | o1mul2 15661 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
| 54 | 12, 26 | remulcld 11291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℝ) |
| 55 | 54 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
| 56 | 55 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
| 57 | | relogcl 26617 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 58 | 57 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
| 59 | 58 | recnd 11289 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℂ) |
| 60 | | rpvmasum.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 61 | | rpvmasum.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 62 | | rpvmasum.u |
. . . . . . . . 9
⊢ 𝑈 = (Unit‘𝑍) |
| 63 | | rpvmasum.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 64 | | rpvmasum.t |
. . . . . . . . 9
⊢ 𝑇 = (◡𝐿 “ {𝐴}) |
| 65 | 60, 61, 9, 62, 63, 64 | rplogsum 27571 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
| 66 | 65 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
| 67 | 56, 59, 66 | o1dif 15666 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
| 68 | 53, 67 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1)) |
| 69 | 68 | ex 412 |
. . . 4
⊢ (𝜑 → ((ℙ ∩ 𝑇) ∈ Fin → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
| 70 | 8, 69 | mtoi 199 |
. . 3
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ∈ Fin) |
| 71 | | nnenom 14021 |
. . . . 5
⊢ ℕ
≈ ω |
| 72 | | sdomentr 9151 |
. . . . 5
⊢
(((ℙ ∩ 𝑇)
≺ ℕ ∧ ℕ ≈ ω) → (ℙ ∩ 𝑇) ≺
ω) |
| 73 | 71, 72 | mpan2 691 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
≺ ω) |
| 74 | | isfinite2 9334 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ω
→ (ℙ ∩ 𝑇)
∈ Fin) |
| 75 | 73, 74 | syl 17 |
. . 3
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
∈ Fin) |
| 76 | 70, 75 | nsyl 140 |
. 2
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ≺
ℕ) |
| 77 | | bren2 9023 |
. 2
⊢ ((ℙ
∩ 𝑇) ≈ ℕ
↔ ((ℙ ∩ 𝑇)
≼ ℕ ∧ ¬ (ℙ ∩ 𝑇) ≺ ℕ)) |
| 78 | 7, 76, 77 | sylanbrc 583 |
1
⊢ (𝜑 → (ℙ ∩ 𝑇) ≈
ℕ) |