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

Theorem rpvmasumlem 24921
Description: Lemma for rpvmasum 24960. 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 9884 . . . . . 6 ℝ ∈ V
2 rpssre 11678 . . . . . 6 + ⊆ ℝ
31, 2ssexi 4726 . . . . 5 + ∈ V
43a1i 11 . . . 4 (𝜑 → ℝ+ ∈ V)
5 fzfid 12592 . . . . . . 7 (𝜑 → (1...(⌊‘𝑥)) ∈ Fin)
6 elfznn 12199 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
76adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8 vmacl 24589 . . . . . . . . . 10 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
97, 8syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
109, 7nndivred 10919 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
1110recnd 9925 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
125, 11fsumcl 14260 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
1312adantr 480 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
14 relogcl 24071 . . . . . . 7 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
1514adantl 481 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
1615recnd 9925 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
1713, 16subcld 10244 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
18 1re 9896 . . . . . . . . 9 1 ∈ ℝ
19 rpvmasum.g . . . . . . . . . . . 12 𝐺 = (DChr‘𝑁)
20 rpvmasum.z . . . . . . . . . . . 12 𝑍 = (ℤ/nℤ‘𝑁)
21 rpvmasum.1 . . . . . . . . . . . 12 1 = (0g𝐺)
22 eqid 2610 . . . . . . . . . . . 12 (Base‘𝑍) = (Base‘𝑍)
23 rpvmasum.a . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ)
2419, 20, 21, 22, 23dchr1re 24733 . . . . . . . . . . 11 (𝜑1 :(Base‘𝑍)⟶ℝ)
2524adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ)
2623nnnn0d 11201 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
27 rpvmasum.l . . . . . . . . . . . . 13 𝐿 = (ℤRHom‘𝑍)
2820, 22, 27znzrhfo 19663 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
29 fof 6013 . . . . . . . . . . . 12 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
3026, 28, 293syl 18 . . . . . . . . . . 11 (𝜑𝐿:ℤ⟶(Base‘𝑍))
31 elfzelz 12171 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
32 ffvelrn 6250 . . . . . . . . . . 11 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿𝑛) ∈ (Base‘𝑍))
3330, 31, 32syl2an 493 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
3425, 33ffvelrnd 6253 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
35 resubcl 10197 . . . . . . . . 9 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
3618, 34, 35sylancr 694 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
3736, 10remulcld 9927 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
3837recnd 9925 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
395, 38fsumcl 14260 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
4039adantr 480 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
41 eqidd 2611 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
42 eqidd 2611 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
434, 17, 40, 41, 42offval2 6790 . . 3 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))))
4413, 16, 40sub32d 10276 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)))
455, 11, 38fsumsub 14311 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
46 1cnd 9913 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
4736recnd 9925 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℂ)
4846, 47, 11subdird 10339 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
49 ax-1cn 9851 . . . . . . . . . . . 12 1 ∈ ℂ
5034recnd 9925 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℂ)
51 nncan 10162 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℂ) → (1 − (1 − ( 1 ‘(𝐿𝑛)))) = ( 1 ‘(𝐿𝑛)))
5249, 50, 51sylancr 694 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 − ( 1 ‘(𝐿𝑛)))) = ( 1 ‘(𝐿𝑛)))
5352oveq1d 6542 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5411mulid2d 9915 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (1 · ((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
5554oveq1d 6542 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))))
5648, 53, 553eqtr3rd 2653 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5756sumeq2dv 14230 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5845, 57eqtr3d 2646 . . . . . . 7 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
5958oveq1d 6542 . . . . . 6 (𝜑 → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6059adantr 480 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6144, 60eqtrd 2644 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
6261mpteq2dva 4667 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
6343, 62eqtrd 2644 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
64 vmadivsum 24916 . . 3 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
652a1i 11 . . . 4 (𝜑 → ℝ+ ⊆ ℝ)
66 1red 9912 . . . 4 (𝜑 → 1 ∈ ℝ)
67 prmdvdsfi 24578 . . . . . 6 (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
6823, 67syl 17 . . . . 5 (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
69 elrabi 3328 . . . . . 6 (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} → 𝑝 ∈ ℙ)
70 prmnn 15175 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
7170adantl 481 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
7271nnrpd 11705 . . . . . . . 8 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+)
7372relogcld 24118 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
74 prmuz2 15195 . . . . . . . . 9 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
7574adantl 481 . . . . . . . 8 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ‘2))
76 uz2m1nn 11598 . . . . . . . 8 (𝑝 ∈ (ℤ‘2) → (𝑝 − 1) ∈ ℕ)
7775, 76syl 17 . . . . . . 7 ((𝜑𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
7873, 77nndivred 10919 . . . . . 6 ((𝜑𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
7969, 78sylan2 490 . . . . 5 ((𝜑𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
8068, 79fsumrecl 14261 . . . 4 (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
81 fzfid 12592 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
82 simpr 476 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) = 0) → ( 1 ‘(𝐿𝑛)) = 0)
83 0re 9897 . . . . . . . . . . 11 0 ∈ ℝ
8482, 83syl6eqel 2696 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) = 0) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
85 eqid 2610 . . . . . . . . . . . 12 (Unit‘𝑍) = (Unit‘𝑍)
8623ad3antrrr 762 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → 𝑁 ∈ ℕ)
87 rpvmasum.d . . . . . . . . . . . . . 14 𝐷 = (Base‘𝐺)
8819dchrabl 24724 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
89 ablgrp 17970 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
9087, 21grpidcl 17222 . . . . . . . . . . . . . . . 16 (𝐺 ∈ Grp → 1𝐷)
9123, 88, 89, 904syl 19 . . . . . . . . . . . . . . 15 (𝜑1𝐷)
9291ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1𝐷)
9333adantlr 747 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
9419, 20, 87, 22, 85, 92, 93dchrn0 24720 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (( 1 ‘(𝐿𝑛)) ≠ 0 ↔ (𝐿𝑛) ∈ (Unit‘𝑍)))
9594biimpa 500 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → (𝐿𝑛) ∈ (Unit‘𝑍))
9619, 20, 21, 85, 86, 95dchr1 24727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) = 1)
9796, 18syl6eqel 2696 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
9884, 97pm2.61dane 2869 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ∈ ℝ)
9918, 98, 35sylancr 694 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℝ)
10010adantlr 747 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
10199, 100remulcld 9927 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
10281, 101fsumrecl 14261 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
103 0le1 10403 . . . . . . . . . . 11 0 ≤ 1
10482, 103syl6eqbr 4617 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) = 0) → ( 1 ‘(𝐿𝑛)) ≤ 1)
10518leidi 10414 . . . . . . . . . . 11 1 ≤ 1
10696, 105syl6eqbr 4617 . . . . . . . . . 10 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿𝑛)) ≠ 0) → ( 1 ‘(𝐿𝑛)) ≤ 1)
107104, 106pm2.61dane 2869 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿𝑛)) ≤ 1)
108 subge0 10393 . . . . . . . . . 10 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿𝑛)) ∈ ℝ) → (0 ≤ (1 − ( 1 ‘(𝐿𝑛))) ↔ ( 1 ‘(𝐿𝑛)) ≤ 1))
10918, 98, 108sylancr 694 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (1 − ( 1 ‘(𝐿𝑛))) ↔ ( 1 ‘(𝐿𝑛)) ≤ 1))
110107, 109mpbird 246 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (1 − ( 1 ‘(𝐿𝑛))))
1119adantlr 747 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
1126adantl 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
113 vmage0 24592 . . . . . . . . . 10 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
114112, 113syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
115112nnred 10885 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
116112nngt0d 10914 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 < 𝑛)
117 divge0 10744 . . . . . . . . 9 ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
118111, 114, 115, 116, 117syl22anc 1319 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
11999, 100, 110, 118mulge0d 10456 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
12081, 101, 119fsumge0 14317 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
121102, 120absidd 13958 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))
12268adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin)
123 inss2 3796 . . . . . . . . 9 ((0[,]𝑥) ∩ ℙ) ⊆ ℙ
124 rabss2 3648 . . . . . . . . 9 (((0[,]𝑥) ∩ ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞𝑁})
125123, 124mp1i 13 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞𝑁})
126 ssfi 8043 . . . . . . . 8 (({𝑞 ∈ ℙ ∣ 𝑞𝑁} ∈ Fin ∧ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ∈ Fin)
127122, 125, 126syl2anc 691 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ∈ Fin)
128 ssrab2 3650 . . . . . . . . . 10 {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)
129128, 123sstri 3577 . . . . . . . . 9 {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ℙ
130129sseli 3564 . . . . . . . 8 (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} → 𝑝 ∈ ℙ)
13178adantlr 747 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
132130, 131sylan2 490 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
133127, 132fsumrecl 14261 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
13480adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
135 fveq2 6088 . . . . . . . . . . . 12 (𝑛 = (𝑝𝑘) → (𝐿𝑛) = (𝐿‘(𝑝𝑘)))
136135fveq2d 6092 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → ( 1 ‘(𝐿𝑛)) = ( 1 ‘(𝐿‘(𝑝𝑘))))
137136oveq2d 6543 . . . . . . . . . 10 (𝑛 = (𝑝𝑘) → (1 − ( 1 ‘(𝐿𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))))
138 fveq2 6088 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
139 id 22 . . . . . . . . . . 11 (𝑛 = (𝑝𝑘) → 𝑛 = (𝑝𝑘))
140138, 139oveq12d 6545 . . . . . . . . . 10 (𝑛 = (𝑝𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
141137, 140oveq12d 6545 . . . . . . . . 9 (𝑛 = (𝑝𝑘) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
142 rpre 11674 . . . . . . . . . 10 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
143142ad2antrl 760 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
14438adantlr 747 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
145 simprr 792 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
146145oveq1d 6542 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛))
1476ad2antrl 760 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
148147nncnd 10886 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℂ)
149147nnne0d 10915 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ≠ 0)
150148, 149div0d 10652 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
151146, 150eqtrd 2644 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = 0)
152151oveq2d 6543 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿𝑛))) · 0))
15347ad2ant2r 779 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (1 − ( 1 ‘(𝐿𝑛))) ∈ ℂ)
154153mul01d 10087 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · 0) = 0)
155152, 154eqtrd 2644 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0)
156141, 143, 144, 155fsumvma2 24684 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
157128a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ⊆ ((0[,]𝑥) ∩ ℙ))
158 fzfid 12592 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
15924ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 :(Base‘𝑍)⟶ℝ)
16030ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝐿:ℤ⟶(Base‘𝑍))
16170ad2antrl 760 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
162 elfznn 12199 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
163162ad2antll 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
164163nnnn0d 11201 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0)
165161, 164nnexpcld 12850 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℕ)
166165nnzd 11316 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℤ)
167160, 166ffvelrnd 6253 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝𝑘)) ∈ (Base‘𝑍))
168159, 167ffvelrnd 6253 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ)
169 resubcl 10197 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ∈ ℝ)
17018, 168, 169sylancr 694 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ∈ ℝ)
171 vmacl 24589 . . . . . . . . . . . . . . . 16 ((𝑝𝑘) ∈ ℕ → (Λ‘(𝑝𝑘)) ∈ ℝ)
172165, 171syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℝ)
173172, 165nndivred 10919 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℝ)
174170, 173remulcld 9927 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
175174anassrs 678 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
176175recnd 9925 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
177158, 176fsumcl 14260 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
178130, 177sylan2 490 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℂ)
179 breq1 4581 . . . . . . . . . . . 12 (𝑞 = 𝑝 → (𝑞𝑁𝑝𝑁))
180179notbid 307 . . . . . . . . . . 11 (𝑞 = 𝑝 → (¬ 𝑞𝑁 ↔ ¬ 𝑝𝑁))
181 notrab 3863 . . . . . . . . . . 11 (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞𝑁}
182180, 181elrab2 3333 . . . . . . . . . 10 (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝𝑁))
183123sseli 3564 . . . . . . . . . . 11 (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ)
18423ad3antrrr 762 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ)
185 simplrr 797 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝𝑁)
186 simplrl 796 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ)
187184nnzd 11316 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ)
188 coprm 15210 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑝𝑁 ↔ (𝑝 gcd 𝑁) = 1))
189186, 187, 188syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝𝑁 ↔ (𝑝 gcd 𝑁) = 1))
190185, 189mpbid 221 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1)
191 prmz 15176 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
192186, 191syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ)
193162adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ)
194193nnnn0d 11201 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ0)
195 rpexp1i 15220 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → ((𝑝 gcd 𝑁) = 1 → ((𝑝𝑘) gcd 𝑁) = 1))
196192, 187, 194, 195syl3anc 1318 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝 gcd 𝑁) = 1 → ((𝑝𝑘) gcd 𝑁) = 1))
197190, 196mpd 15 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝𝑘) gcd 𝑁) = 1)
198184nnnn0d 11201 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ0)
199166anassrs 678 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝𝑘) ∈ ℤ)
200199adantlrr 753 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝𝑘) ∈ ℤ)
20120, 85, 27znunit 19679 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℕ0 ∧ (𝑝𝑘) ∈ ℤ) → ((𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝𝑘) gcd 𝑁) = 1))
202198, 200, 201syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝𝑘) gcd 𝑁) = 1))
203197, 202mpbird 246 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍))
20419, 20, 21, 85, 184, 203dchr1 24727 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 1)
205204oveq2d 6543 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) = (1 − 1))
206 1m1e0 10939 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
207205, 206syl6eq 2660 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) = 0)
208207oveq1d 6542 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = (0 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
209173recnd 9925 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
210209anassrs 678 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
211210adantlrr 753 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) ∈ ℂ)
212211mul02d 10086 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
213208, 212eqtrd 2644 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
214213sumeq2dv 14230 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0)
215 fzfid 12592 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
216215olcd 407 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → ((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ‘1) ∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin))
217 sumz 14249 . . . . . . . . . . . . 13 (((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ‘1) ∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0)
218216, 217syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0)
219214, 218eqtrd 2644 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
220183, 219sylanr1 682 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
221182, 220sylan2b 491 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = 0)
222 ppifi 24577 . . . . . . . . . 10 (𝑥 ∈ ℝ → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
223143, 222syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
224157, 178, 221, 223fsumss 14252 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
225156, 224eqtr4d 2647 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
226158, 175fsumrecl 14261 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
227130, 226sylan2 490 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ∈ ℝ)
22873adantlr 747 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
22970adantl 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
230229nnrecred 10916 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ)
231229nnrpd 11705 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+)
232231rpreccld 11717 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ+)
233 simplrl 796 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈ ℝ+)
234233relogcld 24118 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑥) ∈ ℝ)
235229nnred 10885 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
23674adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ‘2))
237 eluz2b2 11596 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ (ℤ‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
238237simprbi 479 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
239236, 238syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
240235, 239rplogcld 24124 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ+)
241234, 240rerpdivcld 11738 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑥) / (log‘𝑝)) ∈ ℝ)
242241flcld 12419 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ)
243242peano2zd 11320 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ)
244232, 243rpexpcld 12852 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ+)
245244rpred 11707 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ)
246230, 245resubcld 10310 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈ ℝ)
247236, 76syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
248247nnrpd 11705 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℝ+)
249248, 231rpdivcld 11724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈ ℝ+)
250246, 249rerpdivcld 11738 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ)
251228, 250remulcld 9927 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ)
252172recnd 9925 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℂ)
253165nncnd 10886 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℂ)
254165nnne0d 10915 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ≠ 0)
255252, 253, 254divrecd 10656 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) = ((Λ‘(𝑝𝑘)) · (1 / (𝑝𝑘))))
256 simprl 790 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
257 vmappw 24587 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
258256, 163, 257syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
259161nncnd 10886 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ)
260161nnne0d 10915 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0)
261 elfzelz 12171 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ)
262261ad2antll 761 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ)
263259, 260, 262exprecd 12836 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝𝑘)))
264263eqcomd 2616 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝𝑘)) = ((1 / 𝑝)↑𝑘))
265258, 264oveq12d 6545 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) · (1 / (𝑝𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
266255, 265eqtrd 2644 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
267266, 173eqeltrrd 2689 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
268267anassrs 678 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
269 1red 9912 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ ℝ)
270 vmage0 24592 . . . . . . . . . . . . . . . . 17 ((𝑝𝑘) ∈ ℕ → 0 ≤ (Λ‘(𝑝𝑘)))
271165, 270syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝𝑘)))
272165nnred 10885 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℝ)
273165nngt0d 10914 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝𝑘))
274 divge0 10744 . . . . . . . . . . . . . . . 16 ((((Λ‘(𝑝𝑘)) ∈ ℝ ∧ 0 ≤ (Λ‘(𝑝𝑘))) ∧ ((𝑝𝑘) ∈ ℝ ∧ 0 < (𝑝𝑘))) → 0 ≤ ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
275172, 271, 272, 273, 274syl22anc 1319 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
27683leidi 10414 . . . . . . . . . . . . . . . . . 18 0 ≤ 0
277 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 0)
278276, 277syl5breqr 4616 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) = 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
27923ad3antrrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → 𝑁 ∈ ℕ)
28091ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1𝐷)
28119, 20, 87, 22, 85, 280, 167dchrn0 24720 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0 ↔ (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍)))
282281biimpa 500 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → (𝐿‘(𝑝𝑘)) ∈ (Unit‘𝑍))
28319, 20, 21, 85, 279, 282dchr1 24727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝𝑘))) = 1)
284103, 283syl5breqr 4616 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
285278, 284pm2.61dane 2869 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))))
286 subge02 10396 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1))
28718, 168, 286sylancr 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (0 ≤ ( 1 ‘(𝐿‘(𝑝𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1))
288285, 287mpbid 221 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) ≤ 1)
289170, 269, 173, 275, 288lemul1ad 10815 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))))
290209mulid2d 9915 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = ((Λ‘(𝑝𝑘)) / (𝑝𝑘)))
291290, 266eqtrd 2644 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
292289, 291breqtrd 4604 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
293292anassrs 678 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
294158, 175, 268, 293fsumle 14321 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
295228recnd 9925 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℂ)
296161nnrecred 10916 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ)
297296, 164reexpcld 12845 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ)
298297recnd 9925 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
299298anassrs 678 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
300158, 295, 299fsummulc2 14307 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
301 fzval3 12362 . . . . . . . . . . . . . . . 16 ((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
302242, 301syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
303302sumeq1d 14228 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
304230recnd 9925 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℂ)
305229nngt0d 10914 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 < 𝑝)
306 recgt1 10771 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
307235, 305, 306syl2anc 691 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
308239, 307mpbid 221 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) < 1)
309230, 308ltned 10025 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ≠ 1)
310 1nn0 11158 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
311310a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℕ0)
312 log1 24081 . . . . . . . . . . . . . . . . . . . . 21 (log‘1) = 0
313 simprr 792 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
314 1rp 11671 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ+
315 simprl 790 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
316 logleb 24098 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ+𝑥 ∈ ℝ+) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
317314, 315, 316sylancr 694 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
318313, 317mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
319312, 318syl5eqbrr 4614 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
320319adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ (log‘𝑥))
321234, 240, 320divge0d 11747 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑥) / (log‘𝑝)))
322 flge0nn0 12441 . . . . . . . . . . . . . . . . . 18 ((((log‘𝑥) / (log‘𝑝)) ∈ ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0)
323241, 321, 322syl2anc 691 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0)
324 nn0p1nn 11182 . . . . . . . . . . . . . . . . 17 ((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0 → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
325323, 324syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
326 nnuz 11558 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
327325, 326syl6eleq 2698 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ (ℤ‘1))
328304, 309, 311, 327geoserg 14386 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
329304exp1d 12823 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑1) = (1 / 𝑝))
330329oveq1d 6542 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))))
331229nncnd 10886 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℂ)
332 1cnd 9913 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℂ)
333231rpcnne0d 11716 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
334 divsubdir 10573 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
335331, 332, 333, 334syl3anc 1318 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
336 divid 10566 . . . . . . . . . . . . . . . . . 18 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
337333, 336syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1)
338337oveq1d 6542 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
339335, 338eqtr2d 2645 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 − (1 / 𝑝)) = ((𝑝 − 1) / 𝑝))
340330, 339oveq12d 6545 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
341303, 328, 3403eqtrd 2648 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
342341oveq2d 6543 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
343300, 342eqtr3d 2646 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
344294, 343breqtrd 4604 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
345244rpge0d 11711 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
346230, 245subge02d 10471 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝)))
347345, 346mpbid 221 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝))
348248rpcnne0d 11716 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
349 dmdcan 10587 . . . . . . . . . . . . . . 15 ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ 1 ∈ ℂ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
350348, 333, 332, 349syl3anc 1318 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
351347, 350breqtrrd 4606 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))
352247nnrecred 10916 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / (𝑝 − 1)) ∈ ℝ)
353246, 352, 249ledivmuld 11760 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1)))))
354351, 353mpbird 246 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)))
355250, 352, 240lemul2d 11751 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1)))))
356354, 355mpbid 221 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1))))
357247nncnd 10886 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℂ)
358247nnne0d 10915 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠ 0)
359295, 357, 358divrecd 10656 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1))))
360356, 359breqtrrd 4606 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1)))
361226, 251, 131, 344, 360letrd 10046 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
362130, 361sylan2 490 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
363127, 227, 132, 362fsumle 14321 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝𝑘)))) · ((Λ‘(𝑝𝑘)) / (𝑝𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
364225, 363eqbrtrd 4600 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
36579adantlr 747 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
366240, 248rpdivcld 11724 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ+)
367366rpge0d 11711 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
36869, 367sylan2 490 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
369122, 365, 368, 125fsumless 14318 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
370102, 133, 134, 364, 369letrd 10046 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
371121, 370eqbrtrd 4600 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞𝑁} ((log‘𝑝) / (𝑝 − 1)))
37265, 40, 66, 80, 371elo1d 14064 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
373 o1sub 14143 . . 3 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
37464, 372, 373sylancr 694 . 2 (𝜑 → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
37563, 374eqeltrrd 2689 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383   = wceq 1475  wcel 1977  wne 2780  {crab 2900  Vcvv 3173  cdif 3537  cin 3539  wss 3540   class class class wbr 4578  cmpt 4638  wf 5786  ontowfo 5788  cfv 5790  (class class class)co 6527  𝑓 cof 6771  Fincfn 7819  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798   < clt 9931  cle 9932  cmin 10118   / cdiv 10536  cn 10870  2c2 10920  0cn0 11142  cz 11213  cuz 11522  +crp 11667  [,]cicc 12008  ...cfz 12155  ..^cfzo 12292  cfl 12411  cexp 12680  abscabs 13771  𝑂(1)co1 14014  Σcsu 14213  cdvds 14770   gcd cgcd 15003  cprime 15172  Basecbs 15644  0gc0g 15872  Grpcgrp 17194  Abelcabl 17966  Unitcui 18411  ℤRHomczrh 19615  ℤ/nczn 19618  logclog 24050  Λcvma 24563  DChrcdchr 24702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-iin 4453  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-tpos 7217  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-ec 7609  df-qs 7613  df-map 7724  df-pm 7725  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ioc 12010  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-mod 12489  df-seq 12622  df-exp 12681  df-fac 12881  df-bc 12910  df-hash 12938  df-shft 13604  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-limsup 13999  df-clim 14016  df-rlim 14017  df-o1 14018  df-lo1 14019  df-sum 14214  df-ef 14586  df-e 14587  df-sin 14588  df-cos 14589  df-pi 14591  df-dvds 14771  df-gcd 15004  df-prm 15173  df-pc 15329  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-qus 15941  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-mhm 17107  df-submnd 17108  df-grp 17197  df-minusg 17198  df-sbg 17199  df-mulg 17313  df-subg 17363  df-nsg 17364  df-eqg 17365  df-ghm 17430  df-cntz 17522  df-cmn 17967  df-abl 17968  df-mgp 18262  df-ur 18274  df-ring 18321  df-cring 18322  df-oppr 18395  df-dvdsr 18413  df-unit 18414  df-invr 18444  df-rnghom 18487  df-subrg 18550  df-lmod 18637  df-lss 18703  df-lsp 18742  df-sra 18942  df-rgmod 18943  df-lidl 18944  df-rsp 18945  df-2idl 19002  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-fbas 19513  df-fg 19514  df-cnfld 19517  df-zring 19587  df-zrh 19619  df-zn 19622  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-nei 20660  df-lp 20698  df-perf 20699  df-cn 20789  df-cnp 20790  df-haus 20877  df-cmp 20948  df-tx 21123  df-hmeo 21316  df-fil 21408  df-fm 21500  df-flim 21501  df-flf 21502  df-xms 21883  df-ms 21884  df-tms 21885  df-cncf 22437  df-limc 23381  df-dv 23382  df-log 24052  df-cxp 24053  df-cht 24568  df-vma 24569  df-chp 24570  df-ppi 24571  df-dchr 24703
This theorem is referenced by:  rpvmasum2  24946
  Copyright terms: Public domain W3C validator