Step | Hyp | Ref
| Expression |
1 | | reex 10844 |
. . . . . 6
⊢ ℝ
∈ V |
2 | | rpssre 12617 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 5229 |
. . . . 5
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+ ∈
V) |
5 | | fzfid 13570 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘𝑥)) ∈ Fin) |
6 | | elfznn 13165 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
7 | 6 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
8 | | vmacl 26024 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
10 | 9, 7 | nndivred 11908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
11 | 10 | recnd 10885 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
12 | 5, 11 | fsumcl 15321 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
14 | | relogcl 25488 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
15 | 14 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
16 | 15 | recnd 10885 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
17 | 13, 16 | subcld 11213 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
18 | | 1re 10857 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
19 | | rpvmasum.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (DChr‘𝑁) |
20 | | rpvmasum.z |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
21 | | rpvmasum.1 |
. . . . . . . . . . . 12
⊢ 1 =
(0g‘𝐺) |
22 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
23 | | rpvmasum.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
24 | 19, 20, 21, 22, 23 | dchr1re 26168 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 :(Base‘𝑍)⟶ℝ) |
25 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ) |
26 | 23 | nnnn0d 12174 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
27 | | rpvmasum.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (ℤRHom‘𝑍) |
28 | 20, 22, 27 | znzrhfo 20536 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
29 | | fof 6651 |
. . . . . . . . . . . 12
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
30 | 26, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
31 | | elfzelz 13136 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
32 | | ffvelrn 6920 |
. . . . . . . . . . 11
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
33 | 30, 31, 32 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
34 | 25, 33 | ffvelrnd 6923 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
35 | | resubcl 11166 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
36 | 18, 34, 35 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
37 | 36, 10 | remulcld 10887 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
38 | 37 | recnd 10885 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
39 | 5, 38 | fsumcl 15321 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
40 | 39 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
41 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
42 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
43 | 4, 17, 40, 41, 42 | offval2 7506 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))) |
44 | 13, 16, 40 | sub32d 11245 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥))) |
45 | 5, 11, 38 | fsumsub 15376 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
46 | | 1cnd 10852 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
47 | 36 | recnd 10885 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
48 | 46, 47, 11 | subdird 11313 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
49 | | ax-1cn 10811 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
50 | 34 | recnd 10885 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) |
51 | | nncan 11131 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) → (1 − (1
− ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
52 | 49, 50, 51 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 −
( 1
‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
53 | 52 | oveq1d 7246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
54 | 11 | mulid2d 10875 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ·
((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛)) |
55 | 54 | oveq1d 7246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 ·
((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
56 | 48, 53, 55 | 3eqtr3rd 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) − ((1 − (
1
‘(𝐿‘𝑛))) ·
((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
57 | 56 | sumeq2dv 15291 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
58 | 45, 57 | eqtr3d 2780 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
59 | 58 | oveq1d 7246 |
. . . . . 6
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
60 | 59 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
61 | 44, 60 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
62 | 61 | mpteq2dva 5164 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
63 | 43, 62 | eqtrd 2778 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
64 | | vmadivsum 26387 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
65 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
66 | | 1red 10858 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
67 | | prmdvdsfi 26013 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
68 | 23, 67 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
69 | | elrabi 3608 |
. . . . . 6
⊢ (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
70 | | prmnn 16255 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
71 | 70 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ) |
72 | 71 | nnrpd 12650 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+) |
73 | 72 | relogcld 25535 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈
ℝ) |
74 | | prmuz2 16277 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
75 | 74 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
76 | | uz2m1nn 12543 |
. . . . . . . 8
⊢ (𝑝 ∈
(ℤ≥‘2) → (𝑝 − 1) ∈ ℕ) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ) |
78 | 73, 77 | nndivred 11908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
79 | 69, 78 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
80 | 68, 79 | fsumrecl 15322 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
81 | | fzfid 13570 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘𝑥))
∈ Fin) |
82 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) = 0) |
83 | | 0re 10859 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
84 | 82, 83 | eqeltrdi 2847 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
85 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
86 | 23 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → 𝑁 ∈
ℕ) |
87 | | rpvmasum.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (Base‘𝐺) |
88 | 19 | dchrabl 26159 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
89 | | ablgrp 19199 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
90 | 87, 21 | grpidcl 18419 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
91 | 23, 88, 89, 90 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈ 𝐷) |
92 | 91 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1
∈ 𝐷) |
93 | 33 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑛) ∈ (Base‘𝑍)) |
94 | 19, 20, 87, 22, 85, 92, 93 | dchrn0 26155 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (( 1 ‘(𝐿‘𝑛)) ≠ 0 ↔ (𝐿‘𝑛) ∈ (Unit‘𝑍))) |
95 | 94 | biimpa 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → (𝐿‘𝑛) ∈ (Unit‘𝑍)) |
96 | 19, 20, 21, 85, 86, 95 | dchr1 26162 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) = 1) |
97 | 96, 18 | eqeltrdi 2847 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
98 | 84, 97 | pm2.61dane 3030 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
99 | 18, 98, 35 | sylancr 590 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
100 | 10 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
101 | 99, 100 | remulcld 10887 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
102 | 81, 101 | fsumrecl 15322 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
103 | | 0le1 11379 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
104 | 82, 103 | eqbrtrdi 5106 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
105 | 18 | leidi 11390 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
106 | 96, 105 | eqbrtrdi 5106 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
107 | 104, 106 | pm2.61dane 3030 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
108 | | subge0 11369 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (0 ≤ (1 −
( 1
‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
109 | 18, 98, 108 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
110 | 107, 109 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (1 − ( 1 ‘(𝐿‘𝑛)))) |
111 | 9 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
112 | 6 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
113 | | vmage0 26027 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
115 | 112 | nnred 11869 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
116 | 112 | nngt0d 11903 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 < 𝑛) |
117 | | divge0 11725 |
. . . . . . . . 9
⊢
((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤
(Λ‘𝑛)) ∧
(𝑛 ∈ ℝ ∧ 0
< 𝑛)) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
118 | 111, 114,
115, 116, 117 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) / 𝑛)) |
119 | 99, 100, 110, 118 | mulge0d 11433 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
120 | 81, 101, 119 | fsumge0 15383 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
121 | 102, 120 | absidd 15010 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
122 | 68 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
123 | | inss2 4158 |
. . . . . . . . 9
⊢
((0[,]𝑥) ∩
ℙ) ⊆ ℙ |
124 | | rabss2 4005 |
. . . . . . . . 9
⊢
(((0[,]𝑥) ∩
ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
125 | 123, 124 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
126 | 122, 125 | ssfid 8922 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
127 | | ssrab2 4007 |
. . . . . . . . . 10
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ) |
128 | 127, 123 | sstri 3924 |
. . . . . . . . 9
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ℙ |
129 | 128 | sseli 3910 |
. . . . . . . 8
⊢ (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
130 | 78 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ) |
131 | 129, 130 | sylan2 596 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
132 | 126, 131 | fsumrecl 15322 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
133 | 80 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
134 | | 2fveq3 6740 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → ( 1 ‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
135 | 134 | oveq2d 7247 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → (1 − ( 1 ‘(𝐿‘𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘))))) |
136 | | fveq2 6735 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
137 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘)) |
138 | 136, 137 | oveq12d 7249 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
139 | 135, 138 | oveq12d 7249 |
. . . . . . . . 9
⊢ (𝑛 = (𝑝↑𝑘) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
140 | | rpre 12618 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
141 | 140 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
142 | 38 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
143 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) |
144 | 143 | oveq1d 7246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛)) |
145 | 6 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℕ) |
146 | 145 | nncnd 11870 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℂ) |
147 | 145 | nnne0d 11904 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ≠
0) |
148 | 146, 147 | div0d 11631 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (0 / 𝑛) =
0) |
149 | 144, 148 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = 0) |
150 | 149 | oveq2d 7247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘𝑛))) · 0)) |
151 | 47 | ad2ant2r 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
152 | 151 | mul01d 11055 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · 0) = 0) |
153 | 150, 152 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0) |
154 | 139, 141,
142, 153 | fsumvma2 26119 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
155 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)) |
156 | | fzfid 13570 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) |
157 | 24 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 :(Base‘𝑍)⟶ℝ) |
158 | 30 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝐿:ℤ⟶(Base‘𝑍)) |
159 | 70 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℕ) |
160 | | elfznn 13165 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
161 | 160 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ) |
162 | 161 | nnnn0d 12174 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0) |
163 | 159, 162 | nnexpcld 13836 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ) |
164 | 163 | nnzd 12305 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℤ) |
165 | 158, 164 | ffvelrnd 6923 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Base‘𝑍)) |
166 | 157, 165 | ffvelrnd 6923 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) |
167 | | resubcl 11166 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
168 | 18, 166, 167 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
169 | | vmacl 26024 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝↑𝑘) ∈ ℕ →
(Λ‘(𝑝↑𝑘)) ∈ ℝ) |
170 | 163, 169 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℝ) |
171 | 170, 163 | nndivred 11908 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℝ) |
172 | 168, 171 | remulcld 10887 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
173 | 172 | anassrs 471 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
174 | 173 | recnd 10885 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
175 | 156, 174 | fsumcl 15321 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
176 | 129, 175 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
177 | | breq1 5070 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁)) |
178 | 177 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → (¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁)) |
179 | | notrab 4240 |
. . . . . . . . . . 11
⊢
(((0[,]𝑥) ∩
ℙ) ∖ {𝑞 ∈
((0[,]𝑥) ∩ ℙ)
∣ 𝑞 ∥ 𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞 ∥ 𝑁} |
180 | 178, 179 | elrab2 3617 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) |
181 | 123 | sseli 3910 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ) |
182 | 23 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ) |
183 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝 ∥ 𝑁) |
184 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ) |
185 | 182 | nnzd 12305 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ) |
186 | | coprm 16292 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬
𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
187 | 184, 185,
186 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
188 | 183, 187 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1) |
189 | | prmz 16256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
190 | 184, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ) |
191 | 160 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ) |
192 | 191 | nnnn0d 12174 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ0) |
193 | | rpexp1i 16304 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1)) |
194 | 190, 185,
192, 193 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1)) |
195 | 188, 194 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝↑𝑘) gcd 𝑁) = 1) |
196 | 182 | nnnn0d 12174 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈
ℕ0) |
197 | 164 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
198 | 197 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
199 | 20, 85, 27 | znunit 20552 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑝↑𝑘) ∈ ℤ) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
200 | 196, 198,
199 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
201 | 195, 200 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
202 | 19, 20, 21, 85, 182, 201 | dchr1 26162 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
203 | 202 | oveq2d 7247 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = (1 − 1)) |
204 | | 1m1e0 11926 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
205 | 203, 204 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = 0) |
206 | 205 | oveq1d 7246 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
207 | 171 | recnd 10885 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
208 | 207 | anassrs 471 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
209 | 208 | adantlrr 721 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) →
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
210 | 209 | mul02d 11054 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
211 | 206, 210 | eqtrd 2778 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
212 | 211 | sumeq2dv 15291 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0) |
213 | | fzfid 13570 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) |
214 | 213 | olcd 874 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ≥‘1)
∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)) |
215 | | sumz 15310 |
. . . . . . . . . . . . 13
⊢
(((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ≥‘1)
∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) → Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0) |
217 | 212, 216 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
218 | 181, 217 | sylanr1 682 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
219 | 180, 218 | sylan2b 597 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
220 | | ppifi 26012 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
((0[,]𝑥) ∩ ℙ)
∈ Fin) |
221 | 141, 220 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈
Fin) |
222 | 155, 176,
219, 221 | fsumss 15313 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
223 | 154, 222 | eqtr4d 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
224 | 156, 173 | fsumrecl 15322 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
225 | 129, 224 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
226 | 73 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ) |
227 | 70 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
228 | 227 | nnrecred 11905 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ) |
229 | 227 | nnrpd 12650 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ+) |
230 | 229 | rpreccld 12662 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ+) |
231 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈
ℝ+) |
232 | 231 | relogcld 25535 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑥) ∈
ℝ) |
233 | 227 | nnred 11869 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ) |
234 | 74 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
235 | | eluz2gt1 12540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 <
𝑝) |
237 | 233, 236 | rplogcld 25541 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ+) |
238 | 232, 237 | rerpdivcld 12683 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑥) /
(log‘𝑝)) ∈
ℝ) |
239 | 238 | flcld 13397 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ) |
240 | 239 | peano2zd 12309 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ) |
241 | 230, 240 | rpexpcld 13838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ+) |
242 | 241 | rpred 12652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ) |
243 | 228, 242 | resubcld 11284 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈
ℝ) |
244 | 234, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℕ) |
245 | 244 | nnrpd 12650 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℝ+) |
246 | 245, 229 | rpdivcld 12669 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈
ℝ+) |
247 | 243, 246 | rerpdivcld 12683 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ) |
248 | 226, 247 | remulcld 10887 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ) |
249 | 170 | recnd 10885 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℂ) |
250 | 163 | nncnd 11870 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℂ) |
251 | 163 | nnne0d 11904 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ≠ 0) |
252 | 249, 250,
251 | divrecd 11635 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘)))) |
253 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ) |
254 | | vmappw 26022 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
255 | 253, 161,
254 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
256 | 159 | nncnd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ) |
257 | 159 | nnne0d 11904 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0) |
258 | | elfzelz 13136 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ) |
259 | 258 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ) |
260 | 256, 257,
259 | exprecd 13748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘))) |
261 | 260 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝↑𝑘)) = ((1 / 𝑝)↑𝑘)) |
262 | 255, 261 | oveq12d 7249 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
263 | 252, 262 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
264 | 263, 171 | eqeltrrd 2840 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
265 | 264 | anassrs 471 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
266 | | 1red 10858 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈
ℝ) |
267 | | vmage0 26027 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝↑𝑘) ∈ ℕ → 0 ≤
(Λ‘(𝑝↑𝑘))) |
268 | 163, 267 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝↑𝑘))) |
269 | 163 | nnred 11869 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℝ) |
270 | 163 | nngt0d 11903 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝↑𝑘)) |
271 | | divge0 11725 |
. . . . . . . . . . . . . . . 16
⊢
((((Λ‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ≤
(Λ‘(𝑝↑𝑘))) ∧ ((𝑝↑𝑘) ∈ ℝ ∧ 0 < (𝑝↑𝑘))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
272 | 170, 268,
269, 270, 271 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
273 | 83 | leidi 11390 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
0 |
274 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) |
275 | 273, 274 | breqtrrid 5105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
276 | 23 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 𝑁 ∈ ℕ) |
277 | 91 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ 𝐷) |
278 | 19, 20, 87, 22, 85, 277, 165 | dchrn0 26155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0 ↔ (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍))) |
279 | 278 | biimpa 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
280 | 19, 20, 21, 85, 276, 279 | dchr1 26162 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
281 | 103, 280 | breqtrrid 5105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
282 | 275, 281 | pm2.61dane 3030 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
283 | | subge02 11372 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
284 | 18, 166, 283 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
285 | 282, 284 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1) |
286 | 168, 266,
171, 272, 285 | lemul1ad 11795 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
287 | 207 | mulid2d 10875 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
288 | 287, 263 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
289 | 286, 288 | breqtrd 5093 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
290 | 289 | anassrs 471 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
291 | 156, 173,
265, 290 | fsumle 15387 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
292 | 226 | recnd 10885 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℂ) |
293 | 159 | nnrecred 11905 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ) |
294 | 293, 162 | reexpcld 13757 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ) |
295 | 294 | recnd 10885 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
296 | 295 | anassrs 471 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
297 | 156, 292,
296 | fsummulc2 15372 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
298 | | fzval3 13335 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
299 | 239, 298 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
300 | 299 | sumeq1d 15289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘)) |
301 | 228 | recnd 10885 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℂ) |
302 | 227 | nngt0d 11903 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 <
𝑝) |
303 | | recgt1 11752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℝ ∧ 0 <
𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
304 | 233, 302,
303 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 <
𝑝 ↔ (1 / 𝑝) < 1)) |
305 | 236, 304 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) < 1) |
306 | 228, 305 | ltned 10992 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ≠ 1) |
307 | | 1nn0 12130 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
308 | 307 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℕ0) |
309 | | log1 25498 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(log‘1) = 0 |
310 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
311 | | 1rp 12614 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ |
312 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ+) |
313 | | logleb 25515 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
314 | 311, 312,
313 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
315 | 310, 314 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘1)
≤ (log‘𝑥)) |
316 | 309, 315 | eqbrtrrid 5103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(log‘𝑥)) |
317 | 316 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
(log‘𝑥)) |
318 | 232, 237,
317 | divge0d 12692 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑥) /
(log‘𝑝))) |
319 | | flge0nn0 13419 |
. . . . . . . . . . . . . . . . . 18
⊢
((((log‘𝑥) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
320 | 238, 318,
319 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
321 | | nn0p1nn 12153 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0 →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
322 | 320, 321 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
323 | | nnuz 12501 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
324 | 322, 323 | eleqtrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈
(ℤ≥‘1)) |
325 | 301, 306,
308, 324 | geoserg 15454 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
326 | 301 | exp1d 13735 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑1) = (1 / 𝑝)) |
327 | 326 | oveq1d 7246 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))) |
328 | 227 | nncnd 11870 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℂ) |
329 | | 1cnd 10852 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℂ) |
330 | 229 | rpcnne0d 12661 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) |
331 | | divsubdir 11550 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝑝 ∈
ℂ ∧ 𝑝 ≠ 0))
→ ((𝑝 − 1) /
𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
332 | 328, 329,
330, 331 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
333 | | divid 11543 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1) |
334 | 330, 333 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1) |
335 | 334 | oveq1d 7246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝))) |
336 | 332, 335 | eqtr2d 2779 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1
− (1 / 𝑝)) = ((𝑝 − 1) / 𝑝)) |
337 | 327, 336 | oveq12d 7249 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
338 | 300, 325,
337 | 3eqtrd 2782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
339 | 338 | oveq2d 7247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
340 | 297, 339 | eqtr3d 2780 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
341 | 291, 340 | breqtrd 5093 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
342 | 241 | rpge0d 12656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
343 | 228, 242 | subge02d 11448 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝))) |
344 | 342, 343 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝)) |
345 | 245 | rpcnne0d 12661 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠
0)) |
346 | | dmdcan 11566 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠ 0) ∧
(𝑝 ∈ ℂ ∧
𝑝 ≠ 0) ∧ 1 ∈
ℂ) → (((𝑝
− 1) / 𝑝) · (1
/ (𝑝 − 1))) = (1 /
𝑝)) |
347 | 345, 330,
329, 346 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝)) |
348 | 344, 347 | breqtrrd 5095 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1)))) |
349 | 244 | nnrecred 11905 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
(𝑝 − 1)) ∈
ℝ) |
350 | 243, 349,
246 | ledivmuld 12705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))) |
351 | 348, 350 | mpbird 260 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1))) |
352 | 247, 349,
237 | lemul2d 12696 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1))))) |
353 | 351, 352 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1)))) |
354 | 244 | nncnd 11870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℂ) |
355 | 244 | nnne0d 11904 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠
0) |
356 | 292, 354,
355 | divrecd 11635 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1)))) |
357 | 353, 356 | breqtrrd 5095 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
358 | 224, 248,
130, 341, 357 | letrd 11013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
359 | 129, 358 | sylan2 596 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
360 | 126, 225,
131, 359 | fsumle 15387 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
361 | 223, 360 | eqbrtrd 5089 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
362 | 79 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
363 | 237, 245 | rpdivcld 12669 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ+) |
364 | 363 | rpge0d 12656 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑝) / (𝑝 − 1))) |
365 | 69, 364 | sylan2 596 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1))) |
366 | 122, 362,
365, 125 | fsumless 15384 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
367 | 102, 132,
133, 361, 366 | letrd 11013 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
368 | 121, 367 | eqbrtrd 5089 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
369 | 65, 40, 66, 80, 368 | elo1d 15121 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
370 | | o1sub 15201 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
371 | 64, 369, 370 | sylancr 590 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
372 | 63, 371 | eqeltrrd 2840 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |