| Step | Hyp | Ref
| Expression |
| 1 | | reex 11246 |
. . . . . 6
⊢ ℝ
∈ V |
| 2 | | rpssre 13042 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
| 3 | 1, 2 | ssexi 5322 |
. . . . 5
⊢
ℝ+ ∈ V |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+ ∈
V) |
| 5 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘𝑥)) ∈ Fin) |
| 6 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 7 | 6 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
| 8 | | vmacl 27161 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
| 10 | 9, 7 | nndivred 12320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
| 11 | 10 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
| 12 | 5, 11 | fsumcl 15769 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 14 | | relogcl 26617 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 15 | 14 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
| 16 | 15 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
| 17 | 13, 16 | subcld 11620 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
| 18 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 19 | | rpvmasum.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (DChr‘𝑁) |
| 20 | | rpvmasum.z |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 21 | | rpvmasum.1 |
. . . . . . . . . . . 12
⊢ 1 =
(0g‘𝐺) |
| 22 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 23 | | rpvmasum.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 24 | 19, 20, 21, 22, 23 | dchr1re 27307 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 :(Base‘𝑍)⟶ℝ) |
| 25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ) |
| 26 | 23 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 27 | | rpvmasum.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 28 | 20, 22, 27 | znzrhfo 21566 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
| 29 | | fof 6820 |
. . . . . . . . . . . 12
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
| 30 | 26, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
| 31 | | elfzelz 13564 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
| 32 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
| 34 | 25, 33 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
| 35 | | resubcl 11573 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
| 36 | 18, 34, 35 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
| 37 | 36, 10 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
| 38 | 37 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 39 | 5, 38 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 40 | 39 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 41 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
| 42 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
| 43 | 4, 17, 40, 41, 42 | offval2 7717 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))) |
| 44 | 13, 16, 40 | sub32d 11652 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥))) |
| 45 | 5, 11, 38 | fsumsub 15824 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
| 46 | | 1cnd 11256 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
| 47 | 36 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
| 48 | 46, 47, 11 | subdird 11720 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
| 49 | | ax-1cn 11213 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
| 50 | 34 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) |
| 51 | | nncan 11538 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) → (1 − (1
− ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
| 52 | 49, 50, 51 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 −
( 1
‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
| 53 | 52 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 54 | 11 | mullidd 11279 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ·
((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛)) |
| 55 | 54 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 ·
((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
| 56 | 48, 53, 55 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) − ((1 − (
1
‘(𝐿‘𝑛))) ·
((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 57 | 56 | sumeq2dv 15738 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 58 | 45, 57 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 59 | 58 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
| 60 | 59 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
| 61 | 44, 60 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
| 62 | 61 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
| 63 | 43, 62 | eqtrd 2777 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
| 64 | | vmadivsum 27526 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
| 65 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 66 | | 1red 11262 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
| 67 | | prmdvdsfi 27150 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
| 68 | 23, 67 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
| 69 | | elrabi 3687 |
. . . . . 6
⊢ (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
| 70 | | prmnn 16711 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 71 | 70 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ) |
| 72 | 71 | nnrpd 13075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+) |
| 73 | 72 | relogcld 26665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈
ℝ) |
| 74 | | prmuz2 16733 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
| 75 | 74 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
| 76 | | uz2m1nn 12965 |
. . . . . . . 8
⊢ (𝑝 ∈
(ℤ≥‘2) → (𝑝 − 1) ∈ ℕ) |
| 77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ) |
| 78 | 73, 77 | nndivred 12320 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 79 | 69, 78 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 80 | 68, 79 | fsumrecl 15770 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 81 | | fzfid 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘𝑥))
∈ Fin) |
| 82 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) = 0) |
| 83 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 84 | 82, 83 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
| 85 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
| 86 | 23 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → 𝑁 ∈
ℕ) |
| 87 | | rpvmasum.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (Base‘𝐺) |
| 88 | 19 | dchrabl 27298 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
| 89 | | ablgrp 19803 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 90 | 87, 21 | grpidcl 18983 |
. . . . . . . . . . . . . . . 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 27294 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (( 1 ‘(𝐿‘𝑛)) ≠ 0 ↔ (𝐿‘𝑛) ∈ (Unit‘𝑍))) |
| 95 | 94 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → (𝐿‘𝑛) ∈ (Unit‘𝑍)) |
| 96 | 19, 20, 21, 85, 86, 95 | dchr1 27301 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) = 1) |
| 97 | 96, 18 | eqeltrdi 2849 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
| 98 | 84, 97 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
| 99 | 18, 98, 35 | sylancr 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
| 100 | 10 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
| 101 | 99, 100 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
| 102 | 81, 101 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
| 103 | | 0le1 11786 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
| 104 | 82, 103 | eqbrtrdi 5182 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
| 105 | 18 | leidi 11797 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
| 106 | 96, 105 | eqbrtrdi 5182 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
| 107 | 104, 106 | pm2.61dane 3029 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
| 108 | | subge0 11776 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (0 ≤ (1 −
( 1
‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
| 109 | 18, 98, 108 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
| 110 | 107, 109 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (1 − ( 1 ‘(𝐿‘𝑛)))) |
| 111 | 9 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 112 | 6 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 113 | | vmage0 27164 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
| 115 | 112 | nnred 12281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
| 116 | 112 | nngt0d 12315 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 < 𝑛) |
| 117 | | divge0 12137 |
. . . . . . . . 9
⊢
((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤
(Λ‘𝑛)) ∧
(𝑛 ∈ ℝ ∧ 0
< 𝑛)) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
| 118 | 111, 114,
115, 116, 117 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) / 𝑛)) |
| 119 | 99, 100, 110, 118 | mulge0d 11840 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
| 120 | 81, 101, 119 | fsumge0 15831 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
| 121 | 102, 120 | absidd 15461 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
| 122 | 68 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
| 123 | | inss2 4238 |
. . . . . . . . 9
⊢
((0[,]𝑥) ∩
ℙ) ⊆ ℙ |
| 124 | | rabss2 4078 |
. . . . . . . . 9
⊢
(((0[,]𝑥) ∩
ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
| 125 | 123, 124 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
| 126 | 122, 125 | ssfid 9301 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
| 127 | | ssrab2 4080 |
. . . . . . . . . 10
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ) |
| 128 | 127, 123 | sstri 3993 |
. . . . . . . . 9
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ℙ |
| 129 | 128 | sseli 3979 |
. . . . . . . 8
⊢ (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
| 130 | 78 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ) |
| 131 | 129, 130 | sylan2 593 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 132 | 126, 131 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 133 | 80 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 134 | | 2fveq3 6911 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → ( 1 ‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
| 135 | 134 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → (1 − ( 1 ‘(𝐿‘𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘))))) |
| 136 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
| 137 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘)) |
| 138 | 136, 137 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
| 139 | 135, 138 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑛 = (𝑝↑𝑘) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 140 | | rpre 13043 |
. . . . . . . . . 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 7446 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛)) |
| 145 | 6 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℕ) |
| 146 | 145 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℂ) |
| 147 | 145 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ≠
0) |
| 148 | 146, 147 | div0d 12042 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (0 / 𝑛) =
0) |
| 149 | 144, 148 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = 0) |
| 150 | 149 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘𝑛))) · 0)) |
| 151 | 47 | ad2ant2r 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
| 152 | 151 | mul01d 11460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · 0) = 0) |
| 153 | 150, 152 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0) |
| 154 | 139, 141,
142, 153 | fsumvma2 27258 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 155 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)) |
| 156 | | fzfid 14014 |
. . . . . . . . . . 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 13593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 161 | 160 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ) |
| 162 | 161 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0) |
| 163 | 159, 162 | nnexpcld 14284 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ) |
| 164 | 163 | nnzd 12640 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℤ) |
| 165 | 158, 164 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Base‘𝑍)) |
| 166 | 157, 165 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) |
| 167 | | resubcl 11573 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
| 168 | 18, 166, 167 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
| 169 | | vmacl 27161 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝↑𝑘) ∈ ℕ →
(Λ‘(𝑝↑𝑘)) ∈ ℝ) |
| 170 | 163, 169 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℝ) |
| 171 | 170, 163 | nndivred 12320 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℝ) |
| 172 | 168, 171 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
| 173 | 172 | anassrs 467 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
| 174 | 173 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
| 175 | 156, 174 | fsumcl 15769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
| 176 | 129, 175 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
| 177 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁)) |
| 178 | 177 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → (¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁)) |
| 179 | | notrab 4322 |
. . . . . . . . . . 11
⊢
(((0[,]𝑥) ∩
ℙ) ∖ {𝑞 ∈
((0[,]𝑥) ∩ ℙ)
∣ 𝑞 ∥ 𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞 ∥ 𝑁} |
| 180 | 178, 179 | elrab2 3695 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) |
| 181 | 123 | sseli 3979 |
. . . . . . . . . . 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 12640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ) |
| 186 | | coprm 16748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬
𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
| 187 | 184, 185,
186 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
| 188 | 183, 187 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1) |
| 189 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 190 | 184, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ) |
| 191 | 160 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ) |
| 192 | 191 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ0) |
| 193 | | rpexp1i 16760 |
. . . . . . . . . . . . . . . . . . . . 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 12587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈
ℕ0) |
| 197 | 164 | anassrs 467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
| 198 | 197 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
| 199 | 20, 85, 27 | znunit 21582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑝↑𝑘) ∈ ℤ) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
| 200 | 196, 198,
199 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
| 201 | 195, 200 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
| 202 | 19, 20, 21, 85, 182, 201 | dchr1 27301 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
| 203 | 202 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = (1 − 1)) |
| 204 | | 1m1e0 12338 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
| 205 | 203, 204 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = 0) |
| 206 | 205 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 207 | 171 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
| 208 | 207 | anassrs 467 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
| 209 | 208 | adantlrr 721 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) →
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
| 210 | 209 | mul02d 11459 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
| 211 | 206, 210 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
| 212 | 211 | sumeq2dv 15738 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0) |
| 213 | | fzfid 14014 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) |
| 214 | 213 | olcd 875 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ≥‘1)
∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)) |
| 215 | | sumz 15758 |
. . . . . . . . . . . . 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 2777 |
. . . . . . . . . . 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 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
| 220 | | ppifi 27149 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
((0[,]𝑥) ∩ ℙ)
∈ Fin) |
| 221 | 141, 220 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈
Fin) |
| 222 | 155, 176,
219, 221 | fsumss 15761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 223 | 154, 222 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 224 | 156, 173 | fsumrecl 15770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
| 225 | 129, 224 | sylan2 593 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
| 226 | 73 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ) |
| 227 | 70 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
| 228 | 227 | nnrecred 12317 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ) |
| 229 | 227 | nnrpd 13075 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ+) |
| 230 | 229 | rpreccld 13087 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ+) |
| 231 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈
ℝ+) |
| 232 | 231 | relogcld 26665 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑥) ∈
ℝ) |
| 233 | 227 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ) |
| 234 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
| 235 | | eluz2gt1 12962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
| 236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 <
𝑝) |
| 237 | 233, 236 | rplogcld 26671 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ+) |
| 238 | 232, 237 | rerpdivcld 13108 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑥) /
(log‘𝑝)) ∈
ℝ) |
| 239 | 238 | flcld 13838 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ) |
| 240 | 239 | peano2zd 12725 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ) |
| 241 | 230, 240 | rpexpcld 14286 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ+) |
| 242 | 241 | rpred 13077 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ) |
| 243 | 228, 242 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈
ℝ) |
| 244 | 234, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℕ) |
| 245 | 244 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℝ+) |
| 246 | 245, 229 | rpdivcld 13094 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈
ℝ+) |
| 247 | 243, 246 | rerpdivcld 13108 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ) |
| 248 | 226, 247 | remulcld 11291 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ) |
| 249 | 170 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℂ) |
| 250 | 163 | nncnd 12282 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℂ) |
| 251 | 163 | nnne0d 12316 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ≠ 0) |
| 252 | 249, 250,
251 | divrecd 12046 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘)))) |
| 253 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ) |
| 254 | | vmappw 27159 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 255 | 253, 161,
254 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 256 | 159 | nncnd 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ) |
| 257 | 159 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0) |
| 258 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ) |
| 259 | 258 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ) |
| 260 | 256, 257,
259 | exprecd 14194 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘))) |
| 261 | 260 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝↑𝑘)) = ((1 / 𝑝)↑𝑘)) |
| 262 | 255, 261 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 263 | 252, 262 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 264 | 263, 171 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
| 265 | 264 | anassrs 467 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
| 266 | | 1red 11262 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈
ℝ) |
| 267 | | vmage0 27164 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝↑𝑘) ∈ ℕ → 0 ≤
(Λ‘(𝑝↑𝑘))) |
| 268 | 163, 267 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝↑𝑘))) |
| 269 | 163 | nnred 12281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℝ) |
| 270 | 163 | nngt0d 12315 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝↑𝑘)) |
| 271 | | divge0 12137 |
. . . . . . . . . . . . . . . 16
⊢
((((Λ‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ≤
(Λ‘(𝑝↑𝑘))) ∧ ((𝑝↑𝑘) ∈ ℝ ∧ 0 < (𝑝↑𝑘))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
| 272 | 170, 268,
269, 270, 271 | syl22anc 839 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
| 273 | 83 | leidi 11797 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
0 |
| 274 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) |
| 275 | 273, 274 | breqtrrid 5181 |
. . . . . . . . . . . . . . . . 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 27294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0 ↔ (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍))) |
| 279 | 278 | biimpa 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
| 280 | 19, 20, 21, 85, 276, 279 | dchr1 27301 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
| 281 | 103, 280 | breqtrrid 5181 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
| 282 | 275, 281 | pm2.61dane 3029 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
| 283 | | subge02 11779 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
| 284 | 18, 166, 283 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
| 285 | 282, 284 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1) |
| 286 | 168, 266,
171, 272, 285 | lemul1ad 12207 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
| 287 | 207 | mullidd 11279 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
| 288 | 287, 263 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 289 | 286, 288 | breqtrd 5169 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 290 | 289 | anassrs 467 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 291 | 156, 173,
265, 290 | fsumle 15835 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 292 | 226 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℂ) |
| 293 | 159 | nnrecred 12317 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ) |
| 294 | 293, 162 | reexpcld 14203 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ) |
| 295 | 294 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
| 296 | 295 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
| 297 | 156, 292,
296 | fsummulc2 15820 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 298 | | fzval3 13773 |
. . . . . . . . . . . . . . . 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 15736 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘)) |
| 301 | 228 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℂ) |
| 302 | 227 | nngt0d 12315 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 <
𝑝) |
| 303 | | recgt1 12164 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℝ ∧ 0 <
𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
| 304 | 233, 302,
303 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 <
𝑝 ↔ (1 / 𝑝) < 1)) |
| 305 | 236, 304 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) < 1) |
| 306 | 228, 305 | ltned 11397 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ≠ 1) |
| 307 | | 1nn0 12542 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
| 308 | 307 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℕ0) |
| 309 | | log1 26627 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(log‘1) = 0 |
| 310 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
| 311 | | 1rp 13038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ |
| 312 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ+) |
| 313 | | logleb 26645 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
| 314 | 311, 312,
313 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
| 315 | 310, 314 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘1)
≤ (log‘𝑥)) |
| 316 | 309, 315 | eqbrtrrid 5179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(log‘𝑥)) |
| 317 | 316 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
(log‘𝑥)) |
| 318 | 232, 237,
317 | divge0d 13117 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑥) /
(log‘𝑝))) |
| 319 | | flge0nn0 13860 |
. . . . . . . . . . . . . . . . . 18
⊢
((((log‘𝑥) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
| 320 | 238, 318,
319 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
| 321 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0 →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
| 322 | 320, 321 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
| 323 | | nnuz 12921 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
| 324 | 322, 323 | eleqtrdi 2851 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈
(ℤ≥‘1)) |
| 325 | 301, 306,
308, 324 | geoserg 15902 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
| 326 | 301 | exp1d 14181 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑1) = (1 / 𝑝)) |
| 327 | 326 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))) |
| 328 | 227 | nncnd 12282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℂ) |
| 329 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℂ) |
| 330 | 229 | rpcnne0d 13086 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) |
| 331 | | divsubdir 11961 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝑝 ∈
ℂ ∧ 𝑝 ≠ 0))
→ ((𝑝 − 1) /
𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
| 332 | 328, 329,
330, 331 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
| 333 | | divid 11953 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1) |
| 334 | 330, 333 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1) |
| 335 | 334 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝))) |
| 336 | 332, 335 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1
− (1 / 𝑝)) = ((𝑝 − 1) / 𝑝)) |
| 337 | 327, 336 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
| 338 | 300, 325,
337 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
| 339 | 338 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
| 340 | 297, 339 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
| 341 | 291, 340 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
| 342 | 241 | rpge0d 13081 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
| 343 | 228, 242 | subge02d 11855 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝))) |
| 344 | 342, 343 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝)) |
| 345 | 245 | rpcnne0d 13086 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠
0)) |
| 346 | | dmdcan 11977 |
. . . . . . . . . . . . . . 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 5171 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1)))) |
| 349 | 244 | nnrecred 12317 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
(𝑝 − 1)) ∈
ℝ) |
| 350 | 243, 349,
246 | ledivmuld 13130 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))) |
| 351 | 348, 350 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1))) |
| 352 | 247, 349,
237 | lemul2d 13121 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1))))) |
| 353 | 351, 352 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1)))) |
| 354 | 244 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℂ) |
| 355 | 244 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠
0) |
| 356 | 292, 354,
355 | divrecd 12046 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1)))) |
| 357 | 353, 356 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
| 358 | 224, 248,
130, 341, 357 | letrd 11418 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
| 359 | 129, 358 | sylan2 593 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
| 360 | 126, 225,
131, 359 | fsumle 15835 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
| 361 | 223, 360 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
| 362 | 79 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
| 363 | 237, 245 | rpdivcld 13094 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ+) |
| 364 | 363 | rpge0d 13081 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑝) / (𝑝 − 1))) |
| 365 | 69, 364 | sylan2 593 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1))) |
| 366 | 122, 362,
365, 125 | fsumless 15832 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
| 367 | 102, 132,
133, 361, 366 | letrd 11418 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
| 368 | 121, 367 | eqbrtrd 5165 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
| 369 | 65, 40, 66, 80, 368 | elo1d 15572 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
| 370 | | o1sub 15652 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
| 371 | 64, 369, 370 | sylancr 587 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
| 372 | 63, 371 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |