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 27396

Description: Lemma for rpvmasum 27435. 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 11100	. . . . . 6 ⊢ ℝ ∈ V
2		rpssre 12901	. . . . . 6 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5261	. . . . 5 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℝ⁺ ∈ V)
5		fzfid 13880	. . . . . . 7 ⊢ (𝜑 → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13456	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		vmacl 27026	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
10	9, 7	nndivred 12182	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
11	10	recnd 11143	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
12	5, 11	fsumcl 15640	. . . . . 6 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
13	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
14		relogcl 26482	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
15	14	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
16	15	recnd 11143	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
17	13, 16	subcld 11475	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
18		1re 11115	. . . . . . . . 9 ⊢ 1 ∈ ℝ
19		rpvmasum.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (DChr‘𝑁)
20		rpvmasum.z	. . . . . . . . . . . 12 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
21		rpvmasum.1	. . . . . . . . . . . 12 ⊢ 1 = (0_g‘𝐺)
22		eqid 2729	. . . . . . . . . . . 12 ⊢ (Base‘𝑍) = (Base‘𝑍)
23		rpvmasum.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ)
24	19, 20, 21, 22, 23	dchr1re 27172	. . . . . . . . . . 11 ⊢ (𝜑 → 1 :(Base‘𝑍)⟶ℝ)
25	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ)
26	23	nnnn0d 12445	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
27		rpvmasum.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (ℤRHom‘𝑍)
28	20, 22, 27	znzrhfo 21454	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → 𝐿:ℤ–onto→(Base‘𝑍))
29		fof 6736	. . . . . . . . . . . 12 ⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
30	26, 28, 29	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍))
31		elfzelz 13427	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
32		ffvelcdm 7015	. . . . . . . . . . 11 ⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍))
33	30, 31, 32	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍))
34	25, 33	ffvelcdmd 7019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
35		resubcl 11428	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ)
36	18, 34, 35	sylancr 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ)
37	36, 10	remulcld 11145	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
38	37	recnd 11143	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
39	5, 38	fsumcl 15640	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
40	39	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
41		eqidd 2730	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
42		eqidd 2730	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
43	4, 17, 40, 41, 42	offval2 7633	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))))
44	13, 16, 40	sub32d 11507	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)))
45	5, 11, 38	fsumsub 15695	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
46		1cnd 11110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
47	36	recnd 11143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ)
48	46, 47, 11	subdird 11577	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
49		ax-1cn 11067	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
50	34	recnd 11143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℂ)
51		nncan 11393	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) → (1 − (1 − ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛)))
52	49, 50, 51	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 − ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛)))
53	52	oveq1d 7364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
54	11	mullidd 11133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · ((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
55	54	oveq1d 7364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
56	48, 53, 55	3eqtr3rd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
57	56	sumeq2dv 15609	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
58	45, 57	eqtr3d 2766	. . . . . . 7 ⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
59	58	oveq1d 7364	. . . . . 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 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
62	61	mpteq2dva 5185	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
63	43, 62	eqtrd 2764	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
64		vmadivsum 27391	. . 3 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
65	2	a1i 11	. . . 4 ⊢ (𝜑 → ℝ⁺ ⊆ ℝ)
66		1red 11116	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
67		prmdvdsfi 27015	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
68	23, 67	syl 17	. . . . 5 ⊢ (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
69		elrabi 3643	. . . . . 6 ⊢ (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ)
70		prmnn 16585	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
71	70	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
72	71	nnrpd 12935	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ⁺)
73	72	relogcld 26530	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
74		prmuz2 16607	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
75	74	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ_≥‘2))
76		uz2m1nn 12824	. . . . . . . 8 ⊢ (𝑝 ∈ (ℤ_≥‘2) → (𝑝 − 1) ∈ ℕ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
78	73, 77	nndivred 12182	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
79	69, 78	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
80	68, 79	fsumrecl 15641	. . . 4 ⊢ (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
81		fzfid 13880	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
82		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) = 0)
83		0re 11117	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
84	82, 83	eqeltrdi 2836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
85		eqid 2729	. . . . . . . . . . . 12 ⊢ (Unit‘𝑍) = (Unit‘𝑍)
86	23	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → 𝑁 ∈ ℕ)
87		rpvmasum.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (Base‘𝐺)
88	19	dchrabl 27163	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
89		ablgrp 19664	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
90	87, 21	grpidcl 18844	. . . . . . . . . . . . . . . 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 27159	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (( 1 ‘(𝐿‘𝑛)) ≠ 0 ↔ (𝐿‘𝑛) ∈ (Unit‘𝑍)))
95	94	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → (𝐿‘𝑛) ∈ (Unit‘𝑍))
96	19, 20, 21, 85, 86, 95	dchr1 27166	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) = 1)
97	96, 18	eqeltrdi 2836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
98	84, 97	pm2.61dane 3012	. . . . . . . . 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 11145	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
102	81, 101	fsumrecl 15641	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
103		0le1 11643	. . . . . . . . . . 11 ⊢ 0 ≤ 1
104	82, 103	eqbrtrdi 5131	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
105	18	leidi 11654	. . . . . . . . . . 11 ⊢ 1 ≤ 1
106	96, 105	eqbrtrdi 5131	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
107	104, 106	pm2.61dane 3012	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
108		subge0 11633	. . . . . . . . . 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 27029	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
114	112, 113	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
115	112	nnred 12143	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
116	112	nngt0d 12177	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 < 𝑛)
117		divge0 11994	. . . . . . . . 9 ⊢ ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
118	111, 114, 115, 116, 117	syl22anc 838	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
119	99, 100, 110, 118	mulge0d 11697	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
120	81, 101, 119	fsumge0 15702	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
121	102, 120	absidd 15330	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
122	68	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
123		inss2 4189	. . . . . . . . 9 ⊢ ((0[,]𝑥) ∩ ℙ) ⊆ ℙ
124		rabss2 4029	. . . . . . . . 9 ⊢ (((0[,]𝑥) ∩ ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁})
125	123, 124	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁})
126	122, 125	ssfid 9158	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin)
127		ssrab2 4031	. . . . . . . . . 10 ⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)
128	127, 123	sstri 3945	. . . . . . . . 9 ⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ℙ
129	128	sseli 3931	. . . . . . . 8 ⊢ (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ)
130	78	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
131	129, 130	sylan2 593	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
132	126, 131	fsumrecl 15641	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
133	80	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
134		2fveq3 6827	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → ( 1 ‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘(𝑝↑𝑘))))
135	134	oveq2d 7365	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝↑𝑘) → (1 − ( 1 ‘(𝐿‘𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))))
136		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘)))
137		id 22	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘))
138	136, 137	oveq12d 7367	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
139	135, 138	oveq12d 7367	. . . . . . . . 9 ⊢ (𝑛 = (𝑝↑𝑘) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
140		rpre 12902	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
141	140	ad2antrl 728	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
142	38	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
143		simprr 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
144	143	oveq1d 7364	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛))
145	6	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
146	145	nncnd 12144	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℂ)
147	145	nnne0d 12178	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ≠ 0)
148	146, 147	div0d 11899	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
149	144, 148	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = 0)
150	149	oveq2d 7365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘𝑛))) · 0))
151	47	ad2ant2r 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ)
152	151	mul01d 11315	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · 0) = 0)
153	150, 152	eqtrd 2764	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0)
154	139, 141, 142, 153	fsumvma2 27123	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
155	127	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ))
156		fzfid 13880	. . . . . . . . . . 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 13456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
161	160	ad2antll 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
162	161	nnnn0d 12445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ₀)
163	159, 162	nnexpcld 14152	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ)
164	163	nnzd 12498	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℤ)
165	158, 164	ffvelcdmd 7019	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Base‘𝑍))
166	157, 165	ffvelcdmd 7019	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ)
167		resubcl 11428	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ)
168	18, 166, 167	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ)
169		vmacl 27026	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝↑𝑘) ∈ ℕ → (Λ‘(𝑝↑𝑘)) ∈ ℝ)
170	163, 169	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℝ)
171	170, 163	nndivred 12182	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℝ)
172	168, 171	remulcld 11145	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
173	172	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
174	173	recnd 11143	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
175	156, 174	fsumcl 15640	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
176	129, 175	sylan2 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
177		breq1 5095	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁))
178	177	notbid 318	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁))
179		notrab 4273	. . . . . . . . . . 11 ⊢ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞 ∥ 𝑁}
180	178, 179	elrab2 3651	. . . . . . . . . 10 ⊢ (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁))
181	123	sseli 3931	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ)
182	23	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ)
183		simplrr 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝 ∥ 𝑁)
184		simplrl 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ)
185	182	nnzd 12498	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ)
186		coprm 16622	. . . . . . . . . . . . . . . . . . . . . 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 16586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
190	184, 189	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ)
191	160	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ)
192	191	nnnn0d 12445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ₀)
193		rpexp1i 16634	. . . . . . . . . . . . . . . . . . . . 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 12445	. . . . . . . . . . . . . . . . . . . 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 21470	. . . . . . . . . . . . . . . . . . . 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 27166	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1)
203	202	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = (1 − 1))
204		1m1e0 12200	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
205	203, 204	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = 0)
206	205	oveq1d 7364	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
207	171	recnd 11143	. . . . . . . . . . . . . . . . 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 11314	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
211	206, 210	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
212	211	sumeq2dv 15609	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0)
213		fzfid 13880	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
214	213	olcd 874	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → ((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ_≥‘1) ∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin))
215		sumz 15629	. . . . . . . . . . . . 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 2764	. . . . . . . . . . 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 27014	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
221	141, 220	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
222	155, 176, 219, 221	fsumss 15632	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
223	154, 222	eqtr4d 2767	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
224	156, 173	fsumrecl 15641	. . . . . . . . 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 12179	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ)
229	227	nnrpd 12935	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ⁺)
230	229	rpreccld 12947	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ⁺)
231		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈ ℝ⁺)
232	231	relogcld 26530	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑥) ∈ ℝ)
233	227	nnred 12143	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
234	74	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ_≥‘2))
235		eluz2gt1 12821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
237	233, 236	rplogcld 26536	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ⁺)
238	232, 237	rerpdivcld 12968	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑥) / (log‘𝑝)) ∈ ℝ)
239	238	flcld 13702	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ)
240	239	peano2zd 12583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ)
241	230, 240	rpexpcld 14154	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ⁺)
242	241	rpred 12937	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ)
243	228, 242	resubcld 11548	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈ ℝ)
244	234, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
245	244	nnrpd 12935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℝ⁺)
246	245, 229	rpdivcld 12954	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈ ℝ⁺)
247	243, 246	rerpdivcld 12968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ)
248	226, 247	remulcld 11145	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ)
249	170	recnd 11143	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℂ)
250	163	nncnd 12144	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℂ)
251	163	nnne0d 12178	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ≠ 0)
252	249, 250, 251	divrecd 11903	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))))
253		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
254		vmappw 27024	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝))
255	253, 161, 254	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝))
256	159	nncnd 12144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ)
257	159	nnne0d 12178	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0)
258		elfzelz 13427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ)
259	258	ad2antll 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ)
260	256, 257, 259	exprecd 14061	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘)))
261	260	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝↑𝑘)) = ((1 / 𝑝)↑𝑘))
262	255, 261	oveq12d 7367	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
263	252, 262	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
264	263, 171	eqeltrrd 2829	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
265	264	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
266		1red 11116	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ ℝ)
267		vmage0 27029	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝↑𝑘) ∈ ℕ → 0 ≤ (Λ‘(𝑝↑𝑘)))
268	163, 267	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝↑𝑘)))
269	163	nnred 12143	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℝ)
270	163	nngt0d 12177	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝↑𝑘))
271		divge0 11994	. . . . . . . . . . . . . . . 16 ⊢ ((((Λ‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ≤ (Λ‘(𝑝↑𝑘))) ∧ ((𝑝↑𝑘) ∈ ℝ ∧ 0 < (𝑝↑𝑘))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
272	170, 268, 269, 270, 271	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
273	83	leidi 11654	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
274		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0)
275	273, 274	breqtrrid 5130	. . . . . . . . . . . . . . . . 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 27159	. . . . . . . . . . . . . . . . . . . 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 27166	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1)
281	103, 280	breqtrrid 5130	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))))
282	275, 281	pm2.61dane 3012	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))))
283		subge02 11636	. . . . . . . . . . . . . . . . 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 12064	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
287	207	mullidd 11133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
288	287, 263	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
289	286, 288	breqtrd 5118	. . . . . . . . . . . . 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 15706	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
292	226	recnd 11143	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℂ)
293	159	nnrecred 12179	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ)
294	293, 162	reexpcld 14070	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ)
295	294	recnd 11143	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
296	295	anassrs 467	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
297	156, 292, 296	fsummulc2 15691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
298		fzval3 13637	. . . . . . . . . . . . . . . 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 15607	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
301	228	recnd 11143	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℂ)
302	227	nngt0d 12177	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 < 𝑝)
303		recgt1 12021	. . . . . . . . . . . . . . . . . 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 11252	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ≠ 1)
307		1nn0 12400	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
308	307	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℕ₀)
309		log1 26492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (log‘1) = 0
310		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
311		1rp 12897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ⁺
312		simprl 770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ⁺)
313		logleb 26510	. . . . . . . . . . . . . . . . . . . . . . 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 5128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
317	316	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ (log‘𝑥))
318	232, 237, 317	divge0d 12977	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑥) / (log‘𝑝)))
319		flge0nn0 13724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((log‘𝑥) / (log‘𝑝)) ∈ ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀)
320	238, 318, 319	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀)
321		nn0p1nn 12423	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀ → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
322	320, 321	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
323		nnuz 12778	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
324	322, 323	eleqtrdi 2838	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ (ℤ_≥‘1))
325	301, 306, 308, 324	geoserg 15773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
326	301	exp1d 14048	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑1) = (1 / 𝑝))
327	326	oveq1d 7364	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))))
328	227	nncnd 12144	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℂ)
329		1cnd 11110	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℂ)
330	229	rpcnne0d 12946	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
331		divsubdir 11818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
332	328, 329, 330, 331	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
333		divid 11810	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
334	330, 333	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1)
335	334	oveq1d 7364	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
336	332, 335	eqtr2d 2765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 − (1 / 𝑝)) = ((𝑝 − 1) / 𝑝))
337	327, 336	oveq12d 7367	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
338	300, 325, 337	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
339	338	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
340	297, 339	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
341	291, 340	breqtrd 5118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
342	241	rpge0d 12941	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
343	228, 242	subge02d 11712	. . . . . . . . . . . . . . 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 12946	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
346		dmdcan 11834	. . . . . . . . . . . . . . 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 5120	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))
349	244	nnrecred 12179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / (𝑝 − 1)) ∈ ℝ)
350	243, 349, 246	ledivmuld 12990	. . . . . . . . . . . . 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 12981	. . . . . . . . . . . 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 12144	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℂ)
355	244	nnne0d 12178	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠ 0)
356	292, 354, 355	divrecd 11903	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1))))
357	353, 356	breqtrrd 5120	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1)))
358	224, 248, 130, 341, 357	letrd 11273	. . . . . . . . 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 15706	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
361	223, 360	eqbrtrd 5114	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
362	79	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
363	237, 245	rpdivcld 12954	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ⁺)
364	363	rpge0d 12941	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
365	69, 364	sylan2 593	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
366	122, 362, 365, 125	fsumless 15703	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
367	102, 132, 133, 361, 366	letrd 11273	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
368	121, 367	eqbrtrd 5114	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
369	65, 40, 66, 80, 368	elo1d 15443	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
370		o1sub 15523	. . 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 2829	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 {crab 3394 Vcvv 3436 ∖ cdif 3900 ∩ cin 3902 ⊆ wss 3903 class class class wbr 5092 ↦ cmpt 5173 ⟶wf 6478 –onto→wfo 6480 ‘cfv 6482 (class class class)co 7349 ∘_f cof 7611 Fincfn 8872 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 − cmin 11347 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤcz 12471 ℤ_≥cuz 12735 ℝ⁺crp 12893 [,]cicc 13251 ...cfz 13410 ..^cfzo 13557 ⌊cfl 13694 ↑cexp 13968 abscabs 15141 𝑂(1)co1 15393 Σcsu 15593 ∥ cdvds 16163 gcd cgcd 16405 ℙcprime 16582 Basecbs 17120 0_gc0g 17343 Grpcgrp 18812 Abelcabl 19660 Unitcui 20240 ℤRHomczrh 21406 ℤ/nℤczn 21409 logclog 26461 Λcvma 27000 DChrcdchr 27141

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088 ax-mulf 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-tpos 8159 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-ec 8627 df-qs 8631 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-xnn0 12458 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-ioc 13253 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-shft 14974 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-o1 15397 df-lo1 15398 df-sum 15594 df-ef 15974 df-e 15975 df-sin 15976 df-cos 15977 df-pi 15979 df-dvds 16164 df-gcd 16406 df-prm 16583 df-pc 16749 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-qus 17413 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-mhm 18657 df-submnd 18658 df-grp 18815 df-minusg 18816 df-sbg 18817 df-mulg 18947 df-subg 19002 df-nsg 19003 df-eqg 19004 df-ghm 19092 df-cntz 19196 df-cmn 19661 df-abl 19662 df-mgp 20026 df-rng 20038 df-ur 20067 df-ring 20120 df-cring 20121 df-oppr 20222 df-dvdsr 20242 df-unit 20243 df-invr 20273 df-rhm 20357 df-subrng 20431 df-subrg 20455 df-lmod 20765 df-lss 20835 df-lsp 20875 df-sra 21077 df-rgmod 21078 df-lidl 21115 df-rsp 21116 df-2idl 21157 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-fbas 21258 df-fg 21259 df-cnfld 21262 df-zring 21354 df-zrh 21410 df-zn 21413 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-ntr 22905 df-cls 22906 df-nei 22983 df-lp 23021 df-perf 23022 df-cn 23112 df-cnp 23113 df-haus 23200 df-cmp 23272 df-tx 23447 df-hmeo 23640 df-fil 23731 df-fm 23823 df-flim 23824 df-flf 23825 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769 df-limc 25765 df-dv 25766 df-log 26463 df-cxp 26464 df-cht 27005 df-vma 27006 df-chp 27007 df-ppi 27008 df-dchr 27142

This theorem is referenced by: rpvmasum2 27421

W3C validator