MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpvmasumlem Structured version   Visualization version   GIF version

Theorem rpvmasumlem 26392
Description: Lemma for rpvmasum 26431. Calculate the "trivial case" estimate Σ𝑛𝑥( 1 (𝑛)Λ(𝑛) / 𝑛) = log𝑥 + 𝑂(1), where 1 (𝑥) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum.g 𝐺 = (DChr‘𝑁)
rpvmasum.d 𝐷 = (Base‘𝐺)
rpvmasum.1 1 = (0g𝐺)
Assertion
Ref Expression
rpvmasumlem (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
Distinct variable groups:   𝑥,𝑛, 1   𝑛,𝑁,𝑥   𝜑,𝑛,𝑥   𝑛,𝑍,𝑥   𝐷,𝑛,𝑥   𝑛,𝐿,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑛)

Proof of Theorem rpvmasumlem
Dummy variables 𝑘 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 10844 . . . . . 6 ℝ ∈ V
2 rpssre 12617 . . . . . 6 + ⊆ ℝ
31, 2ssexi 5229 . . . . 5 + ∈ V
43a1i 11 . . . 4 (𝜑 → ℝ+ ∈ V)
5 fzfid 13570 . . . . . . 7 (𝜑 → (1...(⌊‘𝑥)) ∈ Fin)
6 elfznn 13165 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
76adantl 485 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8 vmacl 26024 . . . . . . . . . 10 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
97, 8syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
109, 7nndivred 11908 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
1110recnd 10885 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
125, 11fsumcl 15321 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
1312adantr 484 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
14 relogcl 25488 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
1514adantl 485 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
1615recnd 10885 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
1713, 16subcld 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 (𝜑𝑁 ∈ ℕ)
2419, 20, 21, 22, 23dchr1re 26168 . . . . . . . . . . 11 (𝜑1 :(Base‘𝑍)⟶ℝ)
2524adantr 484 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ)
2623nnnn0d 12174 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
27 rpvmasum.l . . . . . . . . . . . . 13 𝐿 = (ℤRHom‘𝑍)
2820, 22, 27znzrhfo 20536 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
29 fof 6651 . . . . . . . . . . . 12 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
3026, 28, 293syl 18 . . . . . . . . . . 11 (𝜑𝐿:ℤ⟶(Base‘𝑍))
31 elfzelz 13136 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
32 ffvelrn 6920 . . . . . . . . . . 11 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿𝑛) ∈ (Base‘𝑍))
3330, 31, 32syl2an 599 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
3425, 33ffvelrnd 6923 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
35 resubcl 11166 . . . . . . . . 9 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
3618, 34, 35sylancr 590 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
3736, 10remulcld 10887 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
3837recnd 10885 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
395, 38fsumcl 15321 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
4039adantr 484 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
41 eqidd 2739 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
42 eqidd 2739 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
434, 17, 40, 41, 42offval2 7506 . . 3 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))))
4413, 16, 40sub32d 11245 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)))
455, 11, 38fsumsub 15376 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
46 1cnd 10852 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
4736recnd 10885 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℂ)
4846, 47, 11subdird 11313 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
49 ax-1cn 10811 . . . . . . . . . . . 12 1 ∈ ℂ
5034recnd 10885 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℂ)
51 nncan 11131 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℂ) → (1 − (1 − ( 1 ‘(𝐿𝑛)))) = ( 1 ‘(𝐿𝑛)))
5249, 50, 51sylancr 590 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 − ( 1 ‘(𝐿𝑛)))) = ( 1 ‘(𝐿𝑛)))
5352oveq1d 7246 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5411mulid2d 10875 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 · ((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
5554oveq1d 7246 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
5648, 53, 553eqtr3rd 2787 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5756sumeq2dv 15291 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5845, 57eqtr3d 2780 . . . . . . 7 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5958oveq1d 7246 . . . . . 6 (𝜑 → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6059adantr 484 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6144, 60eqtrd 2778 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6261mpteq2dva 5164 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
6343, 62eqtrd 2778 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
64 vmadivsum 26387 . . 3 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
652a1i 11 . . . 4 (𝜑 → ℝ+ ⊆ ℝ)
66 1red 10858 . . . 4 (𝜑 → 1 ∈ ℝ)
67 prmdvdsfi 26013 . . . . . 6 (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
6823, 67syl 17 . . . . 5 (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
69 elrabi 3608 . . . . . 6 (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} → 𝑝 ∈ ℙ)
70 prmnn 16255 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
7170adantl 485 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
7271nnrpd 12650 . . . . . . . 8 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+)
7372relogcld 25535 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
74 prmuz2 16277 . . . . . . . . 9 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
7574adantl 485 . . . . . . . 8 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ‘2))
76 uz2m1nn 12543 . . . . . . . 8 (𝑝 ∈ (ℤ‘2) → (𝑝 − 1) ∈ ℕ)
7775, 76syl 17 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
7873, 77nndivred 11908 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
7969, 78sylan2 596 . . . . 5 ((𝜑𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
8068, 79fsumrecl 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 ∈ ℝ
8482, 83eqeltrdi 2847 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) = 0) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
85 eqid 2738 . . . . . . . . . . . 12 (Unit‘𝑍) = (Unit‘𝑍)
8623ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → 𝑁 ∈ ℕ)
87 rpvmasum.d . . . . . . . . . . . . . 14 𝐷 = (Base‘𝐺)
8819dchrabl 26159 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
89 ablgrp 19199 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
9087, 21grpidcl 18419 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → 1𝐷)
9123, 88, 89, 904syl 19 . . . . . . . . . . . . . . 15 (𝜑1𝐷)
9291ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1𝐷)
9333adantlr 715 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
9419, 20, 87, 22, 85, 92, 93dchrn0 26155 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (( 1 ‘(𝐿𝑛)) ≠ 0 ↔ (𝐿𝑛) ∈ (Unit‘𝑍)))
9594biimpa 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → (𝐿𝑛) ∈ (Unit‘𝑍))
9619, 20, 21, 85, 86, 95dchr1 26162 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) = 1)
9796, 18eqeltrdi 2847 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
9884, 97pm2.61dane 3030 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
9918, 98, 35sylancr 590 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
10010adantlr 715 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
10199, 100remulcld 10887 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
10281, 101fsumrecl 15322 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
103 0le1 11379 . . . . . . . . . . 11 0 ≤ 1
10482, 103eqbrtrdi 5106 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) = 0) → ( 1 ‘(𝐿𝑛)) ≤ 1)
10518leidi 11390 . . . . . . . . . . 11 1 ≤ 1
10696, 105eqbrtrdi 5106 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) ≤ 1)
107104, 106pm2.61dane 3030 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ≤ 1)
108 subge0 11369 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℝ) → (0 ≤ (1 − ( 1 ‘(𝐿𝑛))) ↔ ( 1 ‘(𝐿𝑛)) ≤ 1))
10918, 98, 108sylancr 590 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (1 − ( 1 ‘(𝐿𝑛))) ↔ ( 1 ‘(𝐿𝑛)) ≤ 1))
110107, 109mpbird 260 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (1 − ( 1 ‘(𝐿𝑛))))
1119adantlr 715 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
1126adantl 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
113 vmage0 26027 . . . . . . . . . 10 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
114112, 113syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
115112nnred 11869 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
116112nngt0d 11903 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 < 𝑛)
117 divge0 11725 . . . . . . . . 9 ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
118111, 114, 115, 116, 117syl22anc 839 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
11999, 100, 110, 118mulge0d 11433 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
12081, 101, 119fsumge0 15383 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
121102, 120absidd 15010 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
12268adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
123 inss2 4158 . . . . . . . . 9 ((0[,]𝑥) ∩ ℙ) ⊆ ℙ
124 rabss2 4005 . . . . . . . . 9 (((0[,]𝑥) ∩ ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞𝑁})
125123, 124mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞𝑁})
126122, 125ssfid 8922 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ∈ Fin)
127 ssrab2 4007 . . . . . . . . . 10 {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)
128127, 123sstri 3924 . . . . . . . . 9 {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ℙ
129128sseli 3910 . . . . . . . 8 (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} → 𝑝 ∈ ℙ)
13078adantlr 715 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
131129, 130sylan2 596 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
132126, 131fsumrecl 15322 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
13380adantr 484 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
134 2fveq3 6740 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → ( 1 ‘(𝐿𝑛)) = ( 1 ‘(𝐿‘(𝑝𝑘))))
135134oveq2d 7247 . . . . . . . . . 10 (𝑛 = (𝑝𝑘) → (1 − ( 1 ‘(𝐿𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))))
136 fveq2 6735 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
137 id 22 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → 𝑛 = (𝑝𝑘))
138136, 137oveq12d 7249 . . . . . . . . . 10 (𝑛 = (𝑝𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
139135, 138oveq12d 7249 . . . . . . . . 9 (𝑛 = (𝑝𝑘) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
140 rpre 12618 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
141140ad2antrl 728 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
14238adantlr 715 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
143 simprr 773 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
144143oveq1d 7246 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛))
1456ad2antrl 728 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
146145nncnd 11870 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℂ)
147145nnne0d 11904 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ≠ 0)
148146, 147div0d 11631 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
149144, 148eqtrd 2778 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = 0)
150149oveq2d 7247 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿𝑛))) · 0))
15147ad2ant2r 747 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℂ)
152151mul01d 11055 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · 0) = 0)
153150, 152eqtrd 2778 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0)
154139, 141, 142, 153fsumvma2 26119 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
155127a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ((0[,]𝑥) ∩ ℙ))
156 fzfid 13570 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
15724ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 :(Base‘𝑍)⟶ℝ)
15830ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝐿:ℤ⟶(Base‘𝑍))
15970ad2antrl 728 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
160 elfznn 13165 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
161160ad2antll 729 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
162161nnnn0d 12174 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0)
163159, 162nnexpcld 13836 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℕ)
164163nnzd 12305 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℤ)
165158, 164ffvelrnd 6923 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝𝑘)) ∈ (Base‘𝑍))
166157, 165ffvelrnd 6923 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ)
167 resubcl 11166 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ∈ ℝ)
16818, 166, 167sylancr 590 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ∈ ℝ)
169 vmacl 26024 . . . . . . . . . . . . . . . 16 ((𝑝𝑘) ∈ ℕ → (Λ‘(𝑝𝑘)) ∈ ℝ)
170163, 169syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℝ)
171170, 163nndivred 11908 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℝ)
172168, 171remulcld 10887 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
173172anassrs 471 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
174173recnd 10885 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
175156, 174fsumcl 15321 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
176129, 175sylan2 596 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
177 breq1 5070 . . . . . . . . . . . 12 (𝑞 = 𝑝 → (𝑞𝑁𝑝𝑁))
178177notbid 321 . . . . . . . . . . 11 (𝑞 = 𝑝 → (¬ 𝑞𝑁 ↔ ¬ 𝑝𝑁))
179 notrab 4240 . . . . . . . . . . 11 (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞𝑁}
180178, 179elrab2 3617 . . . . . . . . . 10 (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝𝑁))
181123sseli 3910 . . . . . . . . . . 11 (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ)
18223ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ)
183 simplrr 778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝𝑁)
184 simplrl 777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ)
185182nnzd 12305 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ)
186 coprm 16292 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑝𝑁 ↔ (𝑝 gcd 𝑁) = 1))
187184, 185, 186syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝𝑁 ↔ (𝑝 gcd 𝑁) = 1))
188183, 187mpbid 235 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1)
189 prmz 16256 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
190184, 189syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ)
191160adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ)
192191nnnn0d 12174 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ0)
193 rpexp1i 16304 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → ((𝑝 gcd 𝑁) = 1 → ((𝑝𝑘) gcd 𝑁) = 1))
194190, 185, 192, 193syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝 gcd 𝑁) = 1 → ((𝑝𝑘) gcd 𝑁) = 1))
195188, 194mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝𝑘) gcd 𝑁) = 1)
196182nnnn0d 12174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ0)
197164anassrs 471 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝𝑘) ∈ ℤ)
198197adantlrr 721 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝𝑘) ∈ ℤ)
19920, 85, 27znunit 20552 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ0 ∧ (𝑝𝑘) ∈ ℤ) → ((𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝𝑘) gcd 𝑁) = 1))
200196, 198, 199syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝𝑘) gcd 𝑁) = 1))
201195, 200mpbird 260 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍))
20219, 20, 21, 85, 182, 201dchr1 26162 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 1)
203202oveq2d 7247 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) = (1 − 1))
204 1m1e0 11926 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
205203, 204eqtrdi 2795 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) = 0)
206205oveq1d 7246 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = (0 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
207171recnd 10885 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
208207anassrs 471 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
209208adantlrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
210209mul02d 11054 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
211206, 210eqtrd 2778 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
212211sumeq2dv 15291 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0)
213 fzfid 13570 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
214213olcd 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)
216214, 215syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0)
217212, 216eqtrd 2778 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
218181, 217sylanr1 682 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
219180, 218sylan2b 597 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
220 ppifi 26012 . . . . . . . . . 10 (𝑥 ∈ ℝ → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
221141, 220syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
222155, 176, 219, 221fsumss 15313 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
223154, 222eqtr4d 2781 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
224156, 173fsumrecl 15322 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
225129, 224sylan2 596 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
22673adantlr 715 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
22770adantl 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
228227nnrecred 11905 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ)
229227nnrpd 12650 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+)
230229rpreccld 12662 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ+)
231 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈ ℝ+)
232231relogcld 25535 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑥) ∈ ℝ)
233227nnred 11869 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
23474adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ‘2))
235 eluz2gt1 12540 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
236234, 235syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
237233, 236rplogcld 25541 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ+)
238232, 237rerpdivcld 12683 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑥) / (log‘𝑝)) ∈ ℝ)
239238flcld 13397 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ)
240239peano2zd 12309 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ)
241230, 240rpexpcld 13838 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ+)
242241rpred 12652 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ)
243228, 242resubcld 11284 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈ ℝ)
244234, 76syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
245244nnrpd 12650 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℝ+)
246245, 229rpdivcld 12669 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈ ℝ+)
247243, 246rerpdivcld 12683 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ)
248226, 247remulcld 10887 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ)
249170recnd 10885 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℂ)
250163nncnd 11870 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℂ)
251163nnne0d 11904 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ≠ 0)
252249, 250, 251divrecd 11635 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) = ((Λ‘(𝑝𝑘)) · (1 / (𝑝𝑘))))
253 simprl 771 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
254 vmappw 26022 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
255253, 161, 254syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
256159nncnd 11870 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ)
257159nnne0d 11904 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0)
258 elfzelz 13136 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ)
259258ad2antll 729 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ)
260256, 257, 259exprecd 13748 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝𝑘)))
261260eqcomd 2744 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝𝑘)) = ((1 / 𝑝)↑𝑘))
262255, 261oveq12d 7249 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) · (1 / (𝑝𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
263252, 262eqtrd 2778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
264263, 171eqeltrrd 2840 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
265264anassrs 471 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
266 1red 10858 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ ℝ)
267 vmage0 26027 . . . . . . . . . . . . . . . . 17 ((𝑝𝑘) ∈ ℕ → 0 ≤ (Λ‘(𝑝𝑘)))
268163, 267syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝𝑘)))
269163nnred 11869 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℝ)
270163nngt0d 11903 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝𝑘))
271 divge0 11725 . . . . . . . . . . . . . . . 16 ((((Λ‘(𝑝𝑘)) ∈ ℝ ∧ 0 ≤ (Λ‘(𝑝𝑘))) ∧ ((𝑝𝑘) ∈ ℝ ∧ 0 < (𝑝𝑘))) → 0 ≤ ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
272170, 268, 269, 270, 271syl22anc 839 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
27383leidi 11390 . . . . . . . . . . . . . . . . . 18 0 ≤ 0
274 simpr 488 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 0)
275273, 274breqtrrid 5105 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) = 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
27623ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → 𝑁 ∈ ℕ)
27791ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1𝐷)
27819, 20, 87, 22, 85, 277, 165dchrn0 26155 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0 ↔ (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍)))
279278biimpa 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍))
28019, 20, 21, 85, 276, 279dchr1 26162 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 1)
281103, 280breqtrrid 5105 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
282275, 281pm2.61dane 3030 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
283 subge02 11372 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1))
28418, 166, 283sylancr 590 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1))
285282, 284mpbid 235 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1)
286168, 266, 171, 272, 285lemul1ad 11795 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
287207mulid2d 10875 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
288287, 263eqtrd 2778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
289286, 288breqtrd 5093 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
290289anassrs 471 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
291156, 173, 265, 290fsumle 15387 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
292226recnd 10885 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℂ)
293159nnrecred 11905 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ)
294293, 162reexpcld 13757 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ)
295294recnd 10885 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
296295anassrs 471 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
297156, 292, 296fsummulc2 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)))
299239, 298syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
300299sumeq1d 15289 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
301228recnd 10885 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℂ)
302227nngt0d 11903 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 < 𝑝)
303 recgt1 11752 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
304233, 302, 303syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
305236, 304mpbid 235 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) < 1)
306228, 305ltned 10992 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ≠ 1)
307 1nn0 12130 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
308307a1i 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‘𝑥)))
314311, 312, 313sylancr 590 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
315310, 314mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
316309, 315eqbrtrrid 5103 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
317316adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ (log‘𝑥))
318232, 237, 317divge0d 12692 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑥) / (log‘𝑝)))
319 flge0nn0 13419 . . . . . . . . . . . . . . . . . 18 ((((log‘𝑥) / (log‘𝑝)) ∈ ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0)
320238, 318, 319syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0)
321 nn0p1nn 12153 . . . . . . . . . . . . . . . . 17 ((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0 → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
322320, 321syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
323 nnuz 12501 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
324322, 323eleqtrdi 2849 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ (ℤ‘1))
325301, 306, 308, 324geoserg 15454 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
326301exp1d 13735 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑1) = (1 / 𝑝))
327326oveq1d 7246 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))))
328227nncnd 11870 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℂ)
329 1cnd 10852 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℂ)
330229rpcnne0d 12661 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
331 divsubdir 11550 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
332328, 329, 330, 331syl3anc 1373 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
333 divid 11543 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
334330, 333syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1)
335334oveq1d 7246 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
336332, 335eqtr2d 2779 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 − (1 / 𝑝)) = ((𝑝 − 1) / 𝑝))
337327, 336oveq12d 7249 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
338300, 325, 3373eqtrd 2782 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
339338oveq2d 7247 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
340297, 339eqtr3d 2780 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
341291, 340breqtrd 5093 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
342241rpge0d 12656 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
343228, 242subge02d 11448 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝)))
344342, 343mpbid 235 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝))
345245rpcnne0d 12661 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
346 dmdcan 11566 . . . . . . . . . . . . . . 15 ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ 1 ∈ ℂ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
347345, 330, 329, 346syl3anc 1373 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
348344, 347breqtrrd 5095 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))
349244nnrecred 11905 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / (𝑝 − 1)) ∈ ℝ)
350243, 349, 246ledivmuld 12705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1)))))
351348, 350mpbird 260 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)))
352247, 349, 237lemul2d 12696 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1)))))
353351, 352mpbid 235 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1))))
354244nncnd 11870 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℂ)
355244nnne0d 11904 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠ 0)
356292, 354, 355divrecd 11635 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1))))
357353, 356breqtrrd 5095 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1)))
358224, 248, 130, 341, 357letrd 11013 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
359129, 358sylan2 596 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
360126, 225, 131, 359fsumle 15387 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
361223, 360eqbrtrd 5089 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
36279adantlr 715 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
363237, 245rpdivcld 12669 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ+)
364363rpge0d 12656 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
36569, 364sylan2 596 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
366122, 362, 365, 125fsumless 15384 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
367102, 132, 133, 361, 366letrd 11013 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
368121, 367eqbrtrd 5089 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
36965, 40, 66, 80, 368elo1d 15121 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
370 o1sub 15201 . . 3 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
37164, 369, 370sylancr 590 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
37263, 371eqeltrrd 2840 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 847   = wceq 1543  wcel 2111  wne 2941  {crab 3066  Vcvv 3420  cdif 3877  cin 3879  wss 3880   class class class wbr 5067  cmpt 5149  wf 6393  ontowfo 6395  cfv 6397  (class class class)co 7231  f cof 7485  Fincfn 8646  cc 10751  cr 10752  0cc0 10753  1c1 10754   + caddc 10756   · cmul 10758   < clt 10891  cle 10892  cmin 11086   / cdiv 11513  cn 11854  2c2 11909  0cn0 12114  cz 12200  cuz 12462  +crp 12610  [,]cicc 12962  ...cfz 13119  ..^cfzo 13262  cfl 13389  cexp 13659  abscabs 14821  𝑂(1)co1 15071  Σcsu 15273  cdvds 15839   gcd cgcd 16077  cprime 16252  Basecbs 16784  0gc0g 16968  Grpcgrp 18389  Abelcabl 19195  Unitcui 19681  ℤRHomczrh 20490  ℤ/nczn 20493  logclog 25467  Λcvma 25998  DChrcdchr 26137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-inf2 9280  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-pre-sup 10831  ax-addf 10832  ax-mulf 10833
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-iun 4920  df-iin 4921  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-of 7487  df-om 7663  df-1st 7779  df-2nd 7780  df-supp 7924  df-tpos 7988  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-2o 8223  df-oadd 8226  df-er 8411  df-ec 8413  df-qs 8417  df-map 8530  df-pm 8531  df-ixp 8599  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-fsupp 9010  df-fi 9051  df-sup 9082  df-inf 9083  df-oi 9150  df-dju 9541  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-n0 12115  df-xnn0 12187  df-z 12201  df-dec 12318  df-uz 12463  df-q 12569  df-rp 12611  df-xneg 12728  df-xadd 12729  df-xmul 12730  df-ioo 12963  df-ioc 12964  df-ico 12965  df-icc 12966  df-fz 13120  df-fzo 13263  df-fl 13391  df-mod 13467  df-seq 13599  df-exp 13660  df-fac 13864  df-bc 13893  df-hash 13921  df-shft 14654  df-cj 14686  df-re 14687  df-im 14688  df-sqrt 14822  df-abs 14823  df-limsup 15056  df-clim 15073  df-rlim 15074  df-o1 15075  df-lo1 15076  df-sum 15274  df-ef 15653  df-e 15654  df-sin 15655  df-cos 15656  df-pi 15658  df-dvds 15840  df-gcd 16078  df-prm 16253  df-pc 16414  df-struct 16724  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-plusg 16839  df-mulr 16840  df-starv 16841  df-sca 16842  df-vsca 16843  df-ip 16844  df-tset 16845  df-ple 16846  df-ds 16848  df-unif 16849  df-hom 16850  df-cco 16851  df-rest 16951  df-topn 16952  df-0g 16970  df-gsum 16971  df-topgen 16972  df-pt 16973  df-prds 16976  df-xrs 17031  df-qtop 17036  df-imas 17037  df-qus 17038  df-xps 17039  df-mre 17113  df-mrc 17114  df-acs 17116  df-mgm 18138  df-sgrp 18187  df-mnd 18198  df-mhm 18242  df-submnd 18243  df-grp 18392  df-minusg 18393  df-sbg 18394  df-mulg 18513  df-subg 18564  df-nsg 18565  df-eqg 18566  df-ghm 18644  df-cntz 18735  df-cmn 19196  df-abl 19197  df-mgp 19529  df-ur 19541  df-ring 19588  df-cring 19589  df-oppr 19665  df-dvdsr 19683  df-unit 19684  df-invr 19714  df-rnghom 19759  df-subrg 19822  df-lmod 19925  df-lss 19993  df-lsp 20033  df-sra 20233  df-rgmod 20234  df-lidl 20235  df-rsp 20236  df-2idl 20294  df-psmet 20379  df-xmet 20380  df-met 20381  df-bl 20382  df-mopn 20383  df-fbas 20384  df-fg 20385  df-cnfld 20388  df-zring 20460  df-zrh 20494  df-zn 20497  df-top 21815  df-topon 21832  df-topsp 21854  df-bases 21867  df-cld 21940  df-ntr 21941  df-cls 21942  df-nei 22019  df-lp 22057  df-perf 22058  df-cn 22148  df-cnp 22149  df-haus 22236  df-cmp 22308  df-tx 22483  df-hmeo 22676  df-fil 22767  df-fm 22859  df-flim 22860  df-flf 22861  df-xms 23242  df-ms 23243  df-tms 23244  df-cncf 23799  df-limc 24787  df-dv 24788  df-log 25469  df-cxp 25470  df-cht 26003  df-vma 26004  df-chp 26005  df-ppi 26006  df-dchr 26138
This theorem is referenced by:  rpvmasum2  26417
  Copyright terms: Public domain W3C validator