rpvmasumlem - Metamath Proof Explorer

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

Theorem rpvmasumlem 27531

Description: Lemma for rpvmasum 27570. 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 = (0_g‘𝐺)

**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.

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 {crab 3436 Vcvv 3480 ∖ cdif 3948 ∩ cin 3950 ⊆ wss 3951 class class class wbr 5143 ↦ cmpt 5225 ⟶wf 6557 –onto→wfo 6559 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 ℝ⁺crp 13034 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 ⌊cfl 13830 ↑cexp 14102 abscabs 15273 𝑂(1)co1 15522 Σcsu 15722 ∥ cdvds 16290 gcd cgcd 16531 ℙcprime 16708 Basecbs 17247 0_gc0g 17484 Grpcgrp 18951 Abelcabl 19799 Unitcui 20355 ℤRHomczrh 21510 ℤ/nℤczn 21513 logclog 26596 Λcvma 27135 DChrcdchr 27276

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234 ax-mulf 11235

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-tpos 8251 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-ec 8747 df-qs 8751 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-xnn0 12600 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-shft 15106 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-o1 15526 df-lo1 15527 df-sum 15723 df-ef 16103 df-e 16104 df-sin 16105 df-cos 16106 df-pi 16108 df-dvds 16291 df-gcd 16532 df-prm 16709 df-pc 16875 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-qus 17554 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-mhm 18796 df-submnd 18797 df-grp 18954 df-minusg 18955 df-sbg 18956 df-mulg 19086 df-subg 19141 df-nsg 19142 df-eqg 19143 df-ghm 19231 df-cntz 19335 df-cmn 19800 df-abl 19801 df-mgp 20138 df-rng 20150 df-ur 20179 df-ring 20232 df-cring 20233 df-oppr 20334 df-dvdsr 20357 df-unit 20358 df-invr 20388 df-rhm 20472 df-subrng 20546 df-subrg 20570 df-lmod 20860 df-lss 20930 df-lsp 20970 df-sra 21172 df-rgmod 21173 df-lidl 21218 df-rsp 21219 df-2idl 21260 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-zring 21458 df-zrh 21514 df-zn 21517 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-limc 25901 df-dv 25902 df-log 26598 df-cxp 26599 df-cht 27140 df-vma 27141 df-chp 27142 df-ppi 27143 df-dchr 27277

This theorem is referenced by: rpvmasum2 27556

W3C validator