Step | Hyp | Ref
| Expression |
1 | | nnex 11026 |
. . . 4
⊢ ℕ
∈ V |
2 | | inss1 3833 |
. . . . 5
⊢ (ℙ
∩ 𝑇) ⊆
ℙ |
3 | | prmnn 15388 |
. . . . . 6
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
4 | 3 | ssriv 3607 |
. . . . 5
⊢ ℙ
⊆ ℕ |
5 | 2, 4 | sstri 3612 |
. . . 4
⊢ (ℙ
∩ 𝑇) ⊆
ℕ |
6 | | ssdomg 8001 |
. . . 4
⊢ (ℕ
∈ V → ((ℙ ∩ 𝑇) ⊆ ℕ → (ℙ ∩
𝑇) ≼
ℕ)) |
7 | 1, 5, 6 | mp2 9 |
. . 3
⊢ (ℙ
∩ 𝑇) ≼
ℕ |
8 | 7 | a1i 11 |
. 2
⊢ (𝜑 → (ℙ ∩ 𝑇) ≼
ℕ) |
9 | | logno1 24382 |
. . . 4
⊢ ¬
(𝑥 ∈
ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) |
10 | | rpvmasum.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
11 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 𝑁 ∈
ℕ) |
12 | 11 | phicld 15477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℕ) |
13 | 12 | nnred 11035 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℝ) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (ϕ‘𝑁)
∈ ℝ) |
15 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (ℙ
∩ 𝑇) ∈
Fin) |
16 | | inss2 3834 |
. . . . . . . . . 10
⊢
((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇) |
17 | | ssfi 8180 |
. . . . . . . . . 10
⊢
(((ℙ ∩ 𝑇)
∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇)) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin) |
18 | 15, 16, 17 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
∈ Fin) |
19 | 16 | sseli 3599 |
. . . . . . . . . 10
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
→ 𝑛 ∈ (ℙ
∩ 𝑇)) |
20 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ (ℙ ∩ 𝑇)) |
21 | 5, 20 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℕ) |
22 | 21 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℝ+) |
23 | | relogcl 24322 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘𝑛) ∈
ℝ) |
25 | 24, 21 | nndivred 11069 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → ((log‘𝑛) / 𝑛) ∈ ℝ) |
26 | 19, 25 | sylan2 491 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ ((log‘𝑛) /
𝑛) ∈
ℝ) |
27 | 18, 26 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
29 | | rpssre 11843 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
30 | 13 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℂ) |
31 | | o1const 14350 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℝ ∧ (ϕ‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
32 | 29, 30, 31 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
33 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
ℝ+ ⊆ ℝ) |
34 | | 1red 10055 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 1 ∈
ℝ) |
35 | 15, 25 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈ (ℙ
∩ 𝑇)((log‘𝑛) / 𝑛) ∈ ℝ) |
36 | | log1 24332 |
. . . . . . . . . . . . 13
⊢
(log‘1) = 0 |
37 | 21 | nnge1d 11063 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 1 ≤ 𝑛) |
38 | | 1rp 11836 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ |
39 | | logleb 24349 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (1 ≤
𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
40 | 38, 22, 39 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (1 ≤ 𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
41 | 37, 40 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘1) ≤
(log‘𝑛)) |
42 | 36, 41 | syl5eqbrr 4689 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
(log‘𝑛)) |
43 | 24, 22, 42 | divge0d 11912 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
((log‘𝑛) / 𝑛)) |
44 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
⊆ (ℙ ∩ 𝑇)) |
45 | 15, 25, 43, 44 | fsumless 14528 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
46 | 45 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ (𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
47 | 33, 28, 34, 35, 46 | ello1d 14254 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1)) |
48 | | 0red 10041 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ∈
ℝ) |
49 | 19, 43 | sylan2 491 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ 0 ≤ ((log‘𝑛) / 𝑛)) |
50 | 18, 26, 49 | fsumge0 14527 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ≤
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
51 | 50 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ 0 ≤ Σ𝑛
∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
52 | 28, 48, 51 | o1lo12 14269 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1))) |
53 | 47, 52 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
54 | 14, 28, 32, 53 | o1mul2 14355 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
55 | 13, 27 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℝ) |
56 | 55 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
57 | 56 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
58 | | relogcl 24322 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
59 | 58 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
60 | 59 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℂ) |
61 | | rpvmasum.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
62 | | rpvmasum.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑍) |
63 | | rpvmasum.u |
. . . . . . . . 9
⊢ 𝑈 = (Unit‘𝑍) |
64 | | rpvmasum.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
65 | | rpvmasum.t |
. . . . . . . . 9
⊢ 𝑇 = (◡𝐿 “ {𝐴}) |
66 | 61, 62, 10, 63, 64, 65 | rplogsum 25216 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
67 | 66 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
68 | 57, 60, 67 | o1dif 14360 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
69 | 54, 68 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1)) |
70 | 69 | ex 450 |
. . . 4
⊢ (𝜑 → ((ℙ ∩ 𝑇) ∈ Fin → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
71 | 9, 70 | mtoi 190 |
. . 3
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ∈ Fin) |
72 | | nnenom 12779 |
. . . . 5
⊢ ℕ
≈ ω |
73 | | sdomentr 8094 |
. . . . 5
⊢
(((ℙ ∩ 𝑇)
≺ ℕ ∧ ℕ ≈ ω) → (ℙ ∩ 𝑇) ≺
ω) |
74 | 72, 73 | mpan2 707 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
≺ ω) |
75 | | isfinite2 8218 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ω
→ (ℙ ∩ 𝑇)
∈ Fin) |
76 | 74, 75 | syl 17 |
. . 3
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
∈ Fin) |
77 | 71, 76 | nsyl 135 |
. 2
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ≺
ℕ) |
78 | | bren2 7986 |
. 2
⊢ ((ℙ
∩ 𝑇) ≈ ℕ
↔ ((ℙ ∩ 𝑇)
≼ ℕ ∧ ¬ (ℙ ∩ 𝑇) ≺ ℕ)) |
79 | 8, 77, 78 | sylanbrc 698 |
1
⊢ (𝜑 → (ℙ ∩ 𝑇) ≈
ℕ) |