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 27467

Description: Lemma for rpvmasum 27506. 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 11123	. . . . . 6 ⊢ ℝ ∈ V
2		rpssre 12944	. . . . . 6 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5260	. . . . 5 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . 4 ⊢ (𝜑 → ℝ⁺ ∈ V)
5		fzfid 13929	. . . . . . 7 ⊢ (𝜑 → (1...(⌊‘𝑥)) ∈ Fin)
6		elfznn 13501	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
8		vmacl 27098	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
10	9, 7	nndivred 12225	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
11	10	recnd 11167	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
12	5, 11	fsumcl 15689	. . . . . 6 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
13	12	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
14		relogcl 26555	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
15	14	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℝ)
16	15	recnd 11167	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (log‘𝑥) ∈ ℂ)
17	13, 16	subcld 11499	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
18		1re 11138	. . . . . . . . 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 27243	. . . . . . . . . . 11 ⊢ (𝜑 → 1 :(Base‘𝑍)⟶ℝ)
25	24	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ)
26	23	nnnn0d 12492	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
27		rpvmasum.l	. . . . . . . . . . . . 13 ⊢ 𝐿 = (ℤRHom‘𝑍)
28	20, 22, 27	znzrhfo 21540	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → 𝐿:ℤ–onto→(Base‘𝑍))
29		fof 6747	. . . . . . . . . . . 12 ⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
30	26, 28, 29	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍))
31		elfzelz 13472	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
32		ffvelcdm 7028	. . . . . . . . . . 11 ⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍))
33	30, 31, 32	syl2an 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍))
34	25, 33	ffvelcdmd 7032	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
35		resubcl 11452	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ)
36	18, 34, 35	sylancr 588	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ)
37	36, 10	remulcld 11169	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
38	37	recnd 11167	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
39	5, 38	fsumcl 15689	. . . . 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 7645	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))))
44	13, 16, 40	sub32d 11531	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)))
45	5, 11, 38	fsumsub 15744	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
46		1cnd 11133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
47	36	recnd 11167	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ)
48	46, 47, 11	subdird 11601	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
49		ax-1cn 11090	. . . . . . . . . . . 12 ⊢ 1 ∈ ℂ
50	34	recnd 11167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℂ)
51		nncan 11417	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) → (1 − (1 − ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛)))
52	49, 50, 51	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 − ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛)))
53	52	oveq1d 7376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1 − ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
54	11	mullidd 11157	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · ((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
55	54	oveq1d 7376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))
56	48, 53, 55	3eqtr3rd 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
57	56	sumeq2dv 15658	. . . . . . . 8 ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
58	45, 57	eqtr3d 2774	. . . . . . 7 ⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))
59	58	oveq1d 7376	. . . . . 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 2772	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
62	61	mpteq2dva 5179	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
63	43, 62	eqtrd 2772	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
64		vmadivsum 27462	. . 3 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
65	2	a1i 11	. . . 4 ⊢ (𝜑 → ℝ⁺ ⊆ ℝ)
66		1red 11139	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
67		prmdvdsfi 27087	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
68	23, 67	syl 17	. . . . 5 ⊢ (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
69		elrabi 3631	. . . . . 6 ⊢ (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ)
70		prmnn 16637	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
71	70	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
72	71	nnrpd 12978	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ⁺)
73	72	relogcld 26603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
74		prmuz2 16659	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
75	74	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ_≥‘2))
76		uz2m1nn 12867	. . . . . . . 8 ⊢ (𝑝 ∈ (ℤ_≥‘2) → (𝑝 − 1) ∈ ℕ)
77	75, 76	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
78	73, 77	nndivred 12225	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
79	69, 78	sylan2 594	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
80	68, 79	fsumrecl 15690	. . . 4 ⊢ (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
81		fzfid 13929	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
82		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) = 0)
83		0re 11140	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
84	82, 83	eqeltrdi 2845	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
85		eqid 2737	. . . . . . . . . . . 12 ⊢ (Unit‘𝑍) = (Unit‘𝑍)
86	23	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → 𝑁 ∈ ℕ)
87		rpvmasum.d	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (Base‘𝐺)
88	19	dchrabl 27234	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
89		ablgrp 19754	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
90	87, 21	grpidcl 18935	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷)
91	23, 88, 89, 90	4syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ 𝐷)
92	91	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ 𝐷)
93	33	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍))
94	19, 20, 87, 22, 85, 92, 93	dchrn0 27230	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (( 1 ‘(𝐿‘𝑛)) ≠ 0 ↔ (𝐿‘𝑛) ∈ (Unit‘𝑍)))
95	94	biimpa 476	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → (𝐿‘𝑛) ∈ (Unit‘𝑍))
96	19, 20, 21, 85, 86, 95	dchr1 27237	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) = 1)
97	96, 18	eqeltrdi 2845	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
98	84, 97	pm2.61dane 3020	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ)
99	18, 98, 35	sylancr 588	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ)
100	10	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
101	99, 100	remulcld 11169	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
102	81, 101	fsumrecl 15690	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
103		0le1 11667	. . . . . . . . . . 11 ⊢ 0 ≤ 1
104	82, 103	eqbrtrdi 5125	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
105	18	leidi 11678	. . . . . . . . . . 11 ⊢ 1 ≤ 1
106	96, 105	eqbrtrdi 5125	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ ( 1 ‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
107	104, 106	pm2.61dane 3020	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ≤ 1)
108		subge0 11657	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1))
109	18, 98, 108	sylancr 588	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1))
110	107, 109	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))))
111	9	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
112	6	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
113		vmage0 27101	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
114	112, 113	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
115	112	nnred 12183	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
116	112	nngt0d 12220	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 < 𝑛)
117		divge0 12019	. . . . . . . . 9 ⊢ ((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤ (Λ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((Λ‘𝑛) / 𝑛))
118	111, 114, 115, 116, 117	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
119	99, 100, 110, 118	mulge0d 11721	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
120	81, 101, 119	fsumge0 15752	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
121	102, 120	absidd 15379	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))
122	68	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin)
123		inss2 4179	. . . . . . . . 9 ⊢ ((0[,]𝑥) ∩ ℙ) ⊆ ℙ
124		rabss2 4018	. . . . . . . . 9 ⊢ (((0[,]𝑥) ∩ ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁})
125	123, 124	mp1i 13	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁})
126	122, 125	ssfid 9173	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin)
127		ssrab2 4021	. . . . . . . . . 10 ⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)
128	127, 123	sstri 3932	. . . . . . . . 9 ⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ℙ
129	128	sseli 3918	. . . . . . . 8 ⊢ (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ)
130	78	adantlr 716	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
131	129, 130	sylan2 594	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
132	126, 131	fsumrecl 15690	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
133	80	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
134		2fveq3 6840	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → ( 1 ‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘(𝑝↑𝑘))))
135	134	oveq2d 7377	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝↑𝑘) → (1 − ( 1 ‘(𝐿‘𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))))
136		fveq2 6835	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘)))
137		id 22	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘))
138	136, 137	oveq12d 7379	. . . . . . . . . 10 ⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
139	135, 138	oveq12d 7379	. . . . . . . . 9 ⊢ (𝑛 = (𝑝↑𝑘) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
140		rpre 12945	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
141	140	ad2antrl 729	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
142	38	adantlr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
143		simprr 773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
144	143	oveq1d 7376	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛))
145	6	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
146	145	nncnd 12184	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℂ)
147	145	nnne0d 12221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ≠ 0)
148	146, 147	div0d 11924	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
149	144, 148	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) / 𝑛) = 0)
150	149	oveq2d 7377	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘𝑛))) · 0))
151	47	ad2ant2r 748	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ)
152	151	mul01d 11339	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · 0) = 0)
153	150, 152	eqtrd 2772	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ (Λ‘𝑛) = 0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0)
154	139, 141, 142, 153	fsumvma2 27194	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
155	127	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ))
156		fzfid 13929	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
157	24	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 :(Base‘𝑍)⟶ℝ)
158	30	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝐿:ℤ⟶(Base‘𝑍))
159	70	ad2antrl 729	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
160		elfznn 13501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
161	160	ad2antll 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
162	161	nnnn0d 12492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ₀)
163	159, 162	nnexpcld 14201	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ)
164	163	nnzd 12544	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℤ)
165	158, 164	ffvelcdmd 7032	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Base‘𝑍))
166	157, 165	ffvelcdmd 7032	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ)
167		resubcl 11452	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ)
168	18, 166, 167	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ)
169		vmacl 27098	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝↑𝑘) ∈ ℕ → (Λ‘(𝑝↑𝑘)) ∈ ℝ)
170	163, 169	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℝ)
171	170, 163	nndivred 12225	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℝ)
172	168, 171	remulcld 11169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
173	172	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
174	173	recnd 11167	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
175	156, 174	fsumcl 15689	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
176	129, 175	sylan2 594	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ)
177		breq1 5089	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁))
178	177	notbid 318	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → (¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁))
179		notrab 4263	. . . . . . . . . . 11 ⊢ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞 ∥ 𝑁}
180	178, 179	elrab2 3638	. . . . . . . . . 10 ⊢ (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁))
181	123	sseli 3918	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ)
182	23	ad3antrrr 731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ)
183		simplrr 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝 ∥ 𝑁)
184		simplrl 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ)
185	182	nnzd 12544	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ)
186		coprm 16675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1))
187	184, 185, 186	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1))
188	183, 187	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1)
189		prmz 16638	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
190	184, 189	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ)
191	160	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ)
192	191	nnnn0d 12492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ₀)
193		rpexp1i 16687	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ₀) → ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1))
194	190, 185, 192, 193	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1))
195	188, 194	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝↑𝑘) gcd 𝑁) = 1)
196	182	nnnn0d 12492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ₀)
197	164	anassrs 467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ)
198	197	adantlrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ)
199	20, 85, 27	znunit 21556	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑝↑𝑘) ∈ ℤ) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1))
200	196, 198, 199	syl2anc 585	. . . . . . . . . . . . . . . . . . 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 27237	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1)
203	202	oveq2d 7377	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = (1 − 1))
204		1m1e0 12247	. . . . . . . . . . . . . . . 16 ⊢ (1 − 1) = 0
205	203, 204	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = 0)
206	205	oveq1d 7376	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
207	171	recnd 11167	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ)
208	207	anassrs 467	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ)
209	208	adantlrr 722	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ)
210	209	mul02d 11338	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
211	206, 210	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
212	211	sumeq2dv 15658	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0)
213		fzfid 13929	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)
214	213	olcd 875	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → ((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ_≥‘1) ∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin))
215		sumz 15678	. . . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
218	181, 217	sylanr1 683	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
219	180, 218	sylan2b 595	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0)
220		ppifi 27086	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
221	141, 220	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈ Fin)
222	155, 176, 219, 221	fsumss 15681	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
223	154, 222	eqtr4d 2775	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
224	156, 173	fsumrecl 15690	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
225	129, 224	sylan2 594	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ)
226	73	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
227	70	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
228	227	nnrecred 12222	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ)
229	227	nnrpd 12978	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ⁺)
230	229	rpreccld 12990	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℝ⁺)
231		simplrl 777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈ ℝ⁺)
232	231	relogcld 26603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑥) ∈ ℝ)
233	227	nnred 12183	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
234	74	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ (ℤ_≥‘2))
235		eluz2gt1 12864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
237	233, 236	rplogcld 26609	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ⁺)
238	232, 237	rerpdivcld 13011	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑥) / (log‘𝑝)) ∈ ℝ)
239	238	flcld 13751	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ)
240	239	peano2zd 12630	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ)
241	230, 240	rpexpcld 14203	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ⁺)
242	241	rpred 12980	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈ ℝ)
243	228, 242	resubcld 11572	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈ ℝ)
244	234, 76	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ)
245	244	nnrpd 12978	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℝ⁺)
246	245, 229	rpdivcld 12997	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈ ℝ⁺)
247	243, 246	rerpdivcld 13011	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ)
248	226, 247	remulcld 11169	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ)
249	170	recnd 11167	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℂ)
250	163	nncnd 12184	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℂ)
251	163	nnne0d 12221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ≠ 0)
252	249, 250, 251	divrecd 11928	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))))
253		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
254		vmappw 27096	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝))
255	253, 161, 254	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝))
256	159	nncnd 12184	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ)
257	159	nnne0d 12221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0)
258		elfzelz 13472	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ)
259	258	ad2antll 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ)
260	256, 257, 259	exprecd 14110	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘)))
261	260	eqcomd 2743	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝↑𝑘)) = ((1 / 𝑝)↑𝑘))
262	255, 261	oveq12d 7379	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
263	252, 262	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
264	263, 171	eqeltrrd 2838	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
265	264	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ)
266		1red 11139	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ ℝ)
267		vmage0 27101	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝↑𝑘) ∈ ℕ → 0 ≤ (Λ‘(𝑝↑𝑘)))
268	163, 267	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝↑𝑘)))
269	163	nnred 12183	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℝ)
270	163	nngt0d 12220	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝↑𝑘))
271		divge0 12019	. . . . . . . . . . . . . . . 16 ⊢ ((((Λ‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ≤ (Λ‘(𝑝↑𝑘))) ∧ ((𝑝↑𝑘) ∈ ℝ ∧ 0 < (𝑝↑𝑘))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
272	170, 268, 269, 270, 271	syl22anc 839	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
273	83	leidi 11678	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ≤ 0
274		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0)
275	273, 274	breqtrrid 5124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))))
276	23	ad3antrrr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 𝑁 ∈ ℕ)
277	91	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ 𝐷)
278	19, 20, 87, 22, 85, 277, 165	dchrn0 27230	. . . . . . . . . . . . . . . . . . . 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 27237	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1)
281	103, 280	breqtrrid 5124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))))
282	275, 281	pm2.61dane 3020	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))))
283		subge02 11660	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1))
284	18, 166, 283	sylancr 588	. . . . . . . . . . . . . . . 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 12089	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))))
287	207	mullidd 11157	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))
288	287, 263	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
289	286, 288	breqtrd 5112	. . . . . . . . . . . . 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 15756	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
292	226	recnd 11167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℂ)
293	159	nnrecred 12222	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ)
294	293, 162	reexpcld 14119	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ)
295	294	recnd 11167	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
296	295	anassrs 467	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
297	156, 292, 296	fsummulc2 15740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
298		fzval3 13683	. . . . . . . . . . . . . . . 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 15656	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
301	228	recnd 11167	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ∈ ℂ)
302	227	nngt0d 12220	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 < 𝑝)
303		recgt1 12046	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
304	233, 302, 303	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
305	236, 304	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) < 1)
306	228, 305	ltned 11276	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / 𝑝) ≠ 1)
307		1nn0 12447	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℕ₀
308	307	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℕ₀)
309		log1 26565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (log‘1) = 0
310		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
311		1rp 12940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ⁺
312		simprl 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ⁺)
313		logleb 26583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
314	311, 312, 313	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤ (log‘𝑥)))
315	310, 314	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (log‘1) ≤ (log‘𝑥))
316	309, 315	eqbrtrrid 5122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 0 ≤ (log‘𝑥))
317	316	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ (log‘𝑥))
318	232, 237, 317	divge0d 13020	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑥) / (log‘𝑝)))
319		flge0nn0 13773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((log‘𝑥) / (log‘𝑝)) ∈ ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀)
320	238, 318, 319	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀)
321		nn0p1nn 12470	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ₀ → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
322	320, 321	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ)
323		nnuz 12821	. . . . . . . . . . . . . . . 16 ⊢ ℕ = (ℤ_≥‘1)
324	322, 323	eleqtrdi 2847	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ (ℤ_≥‘1))
325	301, 306, 308, 324	geoserg 15825	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
326	301	exp1d 14097	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝)↑1) = (1 / 𝑝))
327	326	oveq1d 7376	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))))
328	227	nncnd 12184	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℂ)
329		1cnd 11133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈ ℂ)
330	229	rpcnne0d 12989	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
331		divsubdir 11842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
332	328, 329, 330, 331	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
333		divid 11834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
334	330, 333	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1)
335	334	oveq1d 7376	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
336	332, 335	eqtr2d 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 − (1 / 𝑝)) = ((𝑝 − 1) / 𝑝))
337	327, 336	oveq12d 7379	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
338	300, 325, 337	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))
339	338	oveq2d 7377	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
340	297, 339	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
341	291, 340	breqtrd 5112	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))))
342	241	rpge0d 12984	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))
343	228, 242	subge02d 11736	. . . . . . . . . . . . . . 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 12989	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
346		dmdcan 11859	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ 1 ∈ ℂ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
347	345, 330, 329, 346	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝))
348	344, 347	breqtrrd 5114	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))
349	244	nnrecred 12222	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (1 / (𝑝 − 1)) ∈ ℝ)
350	243, 349, 246	ledivmuld 13033	. . . . . . . . . . . . 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 13024	. . . . . . . . . . . 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 12184	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℂ)
355	244	nnne0d 12221	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠ 0)
356	292, 354, 355	divrecd 11928	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1))))
357	353, 356	breqtrrd 5114	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1)))
358	224, 248, 130, 341, 357	letrd 11297	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
359	129, 358	sylan2 594	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1)))
360	126, 225, 131, 359	fsumle 15756	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
361	223, 360	eqbrtrd 5108	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
362	79	adantlr 716	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ)
363	237, 245	rpdivcld 12997	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ⁺)
364	363	rpge0d 12984	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
365	69, 364	sylan2 594	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1)))
366	122, 362, 365, 125	fsumless 15753	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
367	102, 132, 133, 361, 366	letrd 11297	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
368	121, 367	eqbrtrd 5108	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)))
369	65, 40, 66, 80, 368	elo1d 15492	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
370		o1sub 15572	. . 3 ⊢ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
371	64, 369, 370	sylancr 588	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1))
372	63, 371	eqeltrrd 2838	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 {crab 3390 Vcvv 3430 ∖ cdif 3887 ∩ cin 3889 ⊆ wss 3890 class class class wbr 5086 ↦ cmpt 5167 ⟶wf 6489 –onto→wfo 6491 ‘cfv 6493 (class class class)co 7361 ∘_f cof 7623 Fincfn 8887 ℂcc 11030 ℝcr 11031 0cc0 11032 1c1 11033 + caddc 11035 · cmul 11037 < clt 11173 ≤ cle 11174 − cmin 11371 / cdiv 11801 ℕcn 12168 2c2 12230 ℕ₀cn0 12431 ℤcz 12518 ℤ_≥cuz 12782 ℝ⁺crp 12936 [,]cicc 13295 ...cfz 13455 ..^cfzo 13602 ⌊cfl 13743 ↑cexp 14017 abscabs 15190 𝑂(1)co1 15442 Σcsu 15642 ∥ cdvds 16215 gcd cgcd 16457 ℙcprime 16634 Basecbs 17173 0_gc0g 17396 Grpcgrp 18903 Abelcabl 19750 Unitcui 20329 ℤRHomczrh 21492 ℤ/nℤczn 21495 logclog 26534 Λcvma 27072 DChrcdchr 27212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111 ax-mulf 11112

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-tpos 8170 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-er 8637 df-ec 8639 df-qs 8643 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-dju 9819 df-card 9857 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-xnn0 12505 df-z 12519 df-dec 12639 df-uz 12783 df-q 12893 df-rp 12937 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13296 df-ioc 13297 df-ico 13298 df-icc 13299 df-fz 13456 df-fzo 13603 df-fl 13745 df-mod 13823 df-seq 13958 df-exp 14018 df-fac 14230 df-bc 14259 df-hash 14287 df-shft 15023 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-limsup 15427 df-clim 15444 df-rlim 15445 df-o1 15446 df-lo1 15447 df-sum 15643 df-ef 16026 df-e 16027 df-sin 16028 df-cos 16029 df-pi 16031 df-dvds 16216 df-gcd 16458 df-prm 16635 df-pc 16802 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-rest 17379 df-topn 17380 df-0g 17398 df-gsum 17399 df-topgen 17400 df-pt 17401 df-prds 17404 df-xrs 17460 df-qtop 17465 df-imas 17466 df-qus 17467 df-xps 17468 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-mhm 18745 df-submnd 18746 df-grp 18906 df-minusg 18907 df-sbg 18908 df-mulg 19038 df-subg 19093 df-nsg 19094 df-eqg 19095 df-ghm 19182 df-cntz 19286 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-rhm 20446 df-subrng 20517 df-subrg 20541 df-lmod 20851 df-lss 20921 df-lsp 20961 df-sra 21163 df-rgmod 21164 df-lidl 21201 df-rsp 21202 df-2idl 21243 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-fbas 21344 df-fg 21345 df-cnfld 21348 df-zring 21440 df-zrh 21496 df-zn 21499 df-top 22872 df-topon 22889 df-topsp 22911 df-bases 22924 df-cld 22997 df-ntr 22998 df-cls 22999 df-nei 23076 df-lp 23114 df-perf 23115 df-cn 23205 df-cnp 23206 df-haus 23293 df-cmp 23365 df-tx 23540 df-hmeo 23733 df-fil 23824 df-fm 23916 df-flim 23917 df-flf 23918 df-xms 24298 df-ms 24299 df-tms 24300 df-cncf 24858 df-limc 25846 df-dv 25847 df-log 26536 df-cxp 26537 df-cht 27077 df-vma 27078 df-chp 27079 df-ppi 27080 df-dchr 27213

This theorem is referenced by: rpvmasum2 27492

W3C validator