Step | Hyp | Ref
| Expression |
1 | | nnex 11715 |
. . . 4
⊢ ℕ
∈ V |
2 | | inss1 4117 |
. . . . 5
⊢ (ℙ
∩ 𝑇) ⊆
ℙ |
3 | | prmssnn 16110 |
. . . . 5
⊢ ℙ
⊆ ℕ |
4 | 2, 3 | sstri 3884 |
. . . 4
⊢ (ℙ
∩ 𝑇) ⊆
ℕ |
5 | | ssdomg 8594 |
. . . 4
⊢ (ℕ
∈ V → ((ℙ ∩ 𝑇) ⊆ ℕ → (ℙ ∩
𝑇) ≼
ℕ)) |
6 | 1, 4, 5 | mp2 9 |
. . 3
⊢ (ℙ
∩ 𝑇) ≼
ℕ |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → (ℙ ∩ 𝑇) ≼
ℕ) |
8 | | logno1 25371 |
. . . 4
⊢ ¬
(𝑥 ∈
ℝ+ ↦ (log‘𝑥)) ∈ 𝑂(1) |
9 | | rpvmasum.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
10 | 9 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 𝑁 ∈
ℕ) |
11 | 10 | phicld 16202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℕ) |
12 | 11 | nnred 11724 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℝ) |
13 | 12 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (ϕ‘𝑁)
∈ ℝ) |
14 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (ℙ
∩ 𝑇) ∈
Fin) |
15 | | inss2 4118 |
. . . . . . . . . 10
⊢
((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇) |
16 | | ssfi 8765 |
. . . . . . . . . 10
⊢
(((ℙ ∩ 𝑇)
∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇)) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin) |
17 | 14, 15, 16 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
∈ Fin) |
18 | | elinel2 4084 |
. . . . . . . . . 10
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
→ 𝑛 ∈ (ℙ
∩ 𝑇)) |
19 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ (ℙ ∩ 𝑇)) |
20 | 4, 19 | sseldi 3873 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℕ) |
21 | 20 | nnrpd 12505 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 𝑛 ∈ ℝ+) |
22 | | relogcl 25311 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℝ+
→ (log‘𝑛) ∈
ℝ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘𝑛) ∈
ℝ) |
24 | 23, 20 | nndivred 11763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → ((log‘𝑛) / 𝑛) ∈ ℝ) |
25 | 18, 24 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ ((log‘𝑛) /
𝑛) ∈
ℝ) |
26 | 17, 25 | fsumrecl 15177 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
27 | 26 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ∈ ℝ) |
28 | | rpssre 12472 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
29 | 12 | recnd 10740 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
(ϕ‘𝑁) ∈
ℂ) |
30 | | o1const 15060 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℝ ∧ (ϕ‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
31 | 28, 29, 30 | sylancr 590 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (ϕ‘𝑁))
∈ 𝑂(1)) |
32 | 28 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
ℝ+ ⊆ ℝ) |
33 | | 1red 10713 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 1 ∈
ℝ) |
34 | 14, 24 | fsumrecl 15177 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈ (ℙ
∩ 𝑇)((log‘𝑛) / 𝑛) ∈ ℝ) |
35 | | log1 25321 |
. . . . . . . . . . . . 13
⊢
(log‘1) = 0 |
36 | 20 | nnge1d 11757 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 1 ≤ 𝑛) |
37 | | 1rp 12469 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ |
38 | | logleb 25338 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ+ ∧ 𝑛 ∈ ℝ+) → (1 ≤
𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
39 | 37, 21, 38 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (1 ≤ 𝑛 ↔ (log‘1) ≤
(log‘𝑛))) |
40 | 36, 39 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → (log‘1) ≤
(log‘𝑛)) |
41 | 35, 40 | eqbrtrrid 5063 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
(log‘𝑛)) |
42 | 23, 21, 41 | divge0d 12547 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈ (ℙ ∩ 𝑇)) → 0 ≤
((log‘𝑛) / 𝑛)) |
43 | 15 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))
⊆ (ℙ ∩ 𝑇)) |
44 | 14, 24, 42, 43 | fsumless 15237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
45 | 44 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ (𝑥 ∈ ℝ+
∧ 1 ≤ 𝑥)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛) ≤ Σ𝑛 ∈ (ℙ ∩ 𝑇)((log‘𝑛) / 𝑛)) |
46 | 32, 27, 33, 34, 45 | ello1d 14963 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1)) |
47 | | 0red 10715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ∈
ℝ) |
48 | 18, 42 | sylan2 596 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇)))
→ 0 ≤ ((log‘𝑛) / 𝑛)) |
49 | 17, 25, 48 | fsumge0 15236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → 0 ≤
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
50 | 49 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ 0 ≤ Σ𝑛
∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) |
51 | 27, 47, 50 | o1lo12 14978 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ≤𝑂(1))) |
52 | 46, 51 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ 𝑂(1)) |
53 | 13, 27, 31, 52 | o1mul2 15065 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
54 | 12, 26 | remulcld 10742 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℝ) |
55 | 54 | recnd 10740 |
. . . . . . . 8
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
56 | 55 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) ∈ ℂ) |
57 | | relogcl 25311 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
58 | 57 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) ∧ 𝑥 ∈ ℝ+)
→ (log‘𝑥) ∈
ℝ) |
59 | 58 | recnd 10740 |
. . . . . . 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 26255 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
66 | 65 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1)) |
67 | 56, 59, 66 | o1dif 15070 |
. . . . . 6
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → ((𝑥 ∈ ℝ+
↦ ((ϕ‘𝑁)
· Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ (ℙ ∩ 𝑇))((log‘𝑛) / 𝑛))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
68 | 53, 67 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ (ℙ ∩ 𝑇) ∈ Fin) → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1)) |
69 | 68 | ex 416 |
. . . 4
⊢ (𝜑 → ((ℙ ∩ 𝑇) ∈ Fin → (𝑥 ∈ ℝ+
↦ (log‘𝑥))
∈ 𝑂(1))) |
70 | 8, 69 | mtoi 202 |
. . 3
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ∈ Fin) |
71 | | nnenom 13432 |
. . . . 5
⊢ ℕ
≈ ω |
72 | | sdomentr 8694 |
. . . . 5
⊢
(((ℙ ∩ 𝑇)
≺ ℕ ∧ ℕ ≈ ω) → (ℙ ∩ 𝑇) ≺
ω) |
73 | 71, 72 | mpan2 691 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
≺ ω) |
74 | | isfinite2 8843 |
. . . 4
⊢ ((ℙ
∩ 𝑇) ≺ ω
→ (ℙ ∩ 𝑇)
∈ Fin) |
75 | 73, 74 | syl 17 |
. . 3
⊢ ((ℙ
∩ 𝑇) ≺ ℕ
→ (ℙ ∩ 𝑇)
∈ Fin) |
76 | 70, 75 | nsyl 142 |
. 2
⊢ (𝜑 → ¬ (ℙ ∩ 𝑇) ≺
ℕ) |
77 | | bren2 8579 |
. 2
⊢ ((ℙ
∩ 𝑇) ≈ ℕ
↔ ((ℙ ∩ 𝑇)
≼ ℕ ∧ ¬ (ℙ ∩ 𝑇) ≺ ℕ)) |
78 | 7, 76, 77 | sylanbrc 586 |
1
⊢ (𝜑 → (ℙ ∩ 𝑇) ≈
ℕ) |