rpvmasumlem

Description: Lemma for rpvmasum . Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n ) Lam ( n ) / n ) = log x + O(1) , where .1. ( x ) is the principal Dirichlet character. Equation 9.4.7 of Shapiro, p. 376. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
Assertion	rpvmasumlem	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
7		reex	⊢ ℝ ∈ V
8		rpssre	⊢ ℝ⁺ ⊆ ℝ
9	7 8	ssexi	⊢ ℝ⁺ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℝ⁺ ∈ V )
11		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
12		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
14		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
16	15 13	nndivred	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
17	16	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
18	11 17	fsumcl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
20		relogcl	⊢ ( 𝑥 ∈ ℝ⁺ → ( log ‘ 𝑥 ) ∈ ℝ )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( log ‘ 𝑥 ) ∈ ℝ )
22	21	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( log ‘ 𝑥 ) ∈ ℂ )
23	19 22	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
24		1re	⊢ 1 ∈ ℝ
25		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
26	4 1 6 25 3	dchr1re	⊢ ( 𝜑 → 1 : ( Base ‘ 𝑍 ) ⟶ ℝ )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 : ( Base ‘ 𝑍 ) ⟶ ℝ )
28	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
29	1 25 2	znzrhfo	⊢ ( 𝑁 ∈ ℕ₀ → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
30		fof	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
31	28 29 30	3syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
32		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
33		ffvelcdm	⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) )
34	31 32 33	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) )
35	27 34	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ )
36		resubcl	⊢ ( ( 1 ∈ ℝ ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
37	24 35 36	sylancr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
38	37 16	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
39	38	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
40	11 39	fsumcl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
42		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) )
43		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
44	10 23 41 42 43	offval2	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘_f − ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) )
45	19 22 41	sub32d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( log ‘ 𝑥 ) ) )
46	11 17 39	fsumsub	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
47		1cnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
48	37	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
49	47 48 17	subdird	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
50		ax-1cn	⊢ 1 ∈ ℂ
51	35	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
52		nncan	⊢ ( ( 1 ∈ ℂ ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ ) → ( 1 − ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) )
53	50 51 52	sylancr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 − ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) = ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) )
54	53	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
55	17	mullidd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
56	55	oveq1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
57	49 54 56	3eqtr3rd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
58	57	sumeq2dv	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
59	46 58	eqtr3d	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
60	59	oveq1d	⊢ ( 𝜑 → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
62	45 61	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
63	62	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) )
64	44 63	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘_f − ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) = ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) )
65		vmadivsum	⊢ ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
66	8	a1i	⊢ ( 𝜑 → ℝ⁺ ⊆ ℝ )
67		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
68		prmdvdsfi	⊢ ( 𝑁 ∈ ℕ → { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ∈ Fin )
69	3 68	syl	⊢ ( 𝜑 → { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ∈ Fin )
70		elrabi	⊢ ( 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } → 𝑝 ∈ ℙ )
71		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
72	71	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
73	72	nnrpd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ⁺ )
74	73	relogcld	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ∈ ℝ )
75		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ_≥ ‘ 2 ) )
76	75	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ( ℤ_≥ ‘ 2 ) )
77		uz2m1nn	⊢ ( 𝑝 ∈ ( ℤ_≥ ‘ 2 ) → ( 𝑝 − 1 ) ∈ ℕ )
78	76 77	syl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ∈ ℕ )
79	74 78	nndivred	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
80	70 79	sylan2	⊢ ( ( 𝜑 ∧ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
81	69 80	fsumrecl	⊢ ( 𝜑 → Σ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
82		fzfid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
83		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 )
84		0re	⊢ 0 ∈ ℝ
85	83 84	eqeltrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ )
86		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
87	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ) → 𝑁 ∈ ℕ )
88	4	dchrabl	⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
89		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
90	5 6	grpidcl	⊢ ( 𝐺 ∈ Grp → 1 ∈ 𝐷 )
91	3 88 89 90	4syl	⊢ ( 𝜑 → 1 ∈ 𝐷 )
92	91	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ 𝐷 )
93	34	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) )
94	4 1 5 25 86 92 93	dchrn0	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ↔ ( 𝐿 ‘ 𝑛 ) ∈ ( Unit ‘ 𝑍 ) ) )
95	94	biimpa	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Unit ‘ 𝑍 ) )
96	4 1 6 86 87 95	dchr1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = 1 )
97	96 24	eqeltrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ )
98	85 97	pm2.61dane	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ )
99	24 98 36	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℝ )
100	16	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
101	99 100	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
102	82 101	fsumrecl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
103		0le1	⊢ 0 ≤ 1
104	83 103	eqbrtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≤ 1 )
105	24	leidi	⊢ 1 ≤ 1
106	96 105	eqbrtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≠ 0 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≤ 1 )
107	104 106	pm2.61dane	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≤ 1 )
108		subge0	⊢ ( ( 1 ∈ ℝ ∧ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ↔ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≤ 1 ) )
109	24 98 108	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 0 ≤ ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ↔ ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ≤ 1 ) )
110	107 109	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) )
111	15	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
112	12	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
113		vmage0	⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
114	112 113	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
115	112	nnred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
116	112	nngt0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 < 𝑛 )
117		divge0	⊢ ( ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( Λ ‘ 𝑛 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
118	111 114 115 116 117	syl22anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
119	99 100 110 118	mulge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
120	82 101 119	fsumge0	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
121	102 120	absidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
122	69	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ∈ Fin )
123		inss2	⊢ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ⊆ ℙ
124		rabss2	⊢ ( ( ( 0 [,] 𝑥 ) ∩ ℙ ) ⊆ ℙ → { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ⊆ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } )
125	123 124	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ⊆ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } )
126	122 125	ssfid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ∈ Fin )
127		ssrab2	⊢ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ⊆ ( ( 0 [,] 𝑥 ) ∩ ℙ )
128	127 123	sstri	⊢ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ⊆ ℙ
129	128	sseli	⊢ ( 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } → 𝑝 ∈ ℙ )
130	79	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
131	129 130	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
132	126 131	fsumrecl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
133	81	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
134		2fveq3	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
135	134	oveq2d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) = ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) )
136		fveq2	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
137		id	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → 𝑛 = ( 𝑝 ↑ 𝑘 ) )
138	136 137	oveq12d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) = ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
139	135 138	oveq12d	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
140		rpre	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ )
141	140	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
142	39	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
143		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
144	143	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) = ( 0 / 𝑛 ) )
145	12	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℕ )
146	145	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℂ )
147	145	nnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ≠ 0 )
148	146 147	div0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 0 / 𝑛 ) = 0 )
149	144 148	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) = 0 )
150	149	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · 0 ) )
151	48	ad2ant2r	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) ∈ ℂ )
152	151	mul01d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · 0 ) = 0 )
153	150 152	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = 0 )
154	139 141 142 153	fsumvma2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
155	127	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ⊆ ( ( 0 [,] 𝑥 ) ∩ ℙ ) )
156		fzfid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
157	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 1 : ( Base ‘ 𝑍 ) ⟶ ℝ )
158	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
159	71	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℕ )
160		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
161	160	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ )
162	161	nnnn0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ₀ )
163	159 162	nnexpcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
164	163	nnzd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
165	158 164	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Base ‘ 𝑍 ) )
166	157 165	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ )
167		resubcl	⊢ ( ( 1 ∈ ℝ ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) ∈ ℝ )
168	24 166 167	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) ∈ ℝ )
169		vmacl	⊢ ( ( 𝑝 ↑ 𝑘 ) ∈ ℕ → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
170	163 169	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
171	170 163	nndivred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ )
172	168 171	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ )
173	172	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ )
174	173	recnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℂ )
175	156 174	fsumcl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℂ )
176	129 175	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℂ )
177		breq1	⊢ ( 𝑞 = 𝑝 → ( 𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁 ) )
178	177	notbid	⊢ ( 𝑞 = 𝑝 → ( ¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁 ) )
179		notrab	⊢ ( ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∖ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) = { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ ¬ 𝑞 ∥ 𝑁 }
180	178 179	elrab2	⊢ ( 𝑝 ∈ ( ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∖ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) ↔ ( 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∧ ¬ 𝑝 ∥ 𝑁 ) )
181	123	sseli	⊢ ( 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) → 𝑝 ∈ ℙ )
182	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑁 ∈ ℕ )
183		simplrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ¬ 𝑝 ∥ 𝑁 )
184		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℙ )
185	182	nnzd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑁 ∈ ℤ )
186		coprm	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑝 ∥ 𝑁 ↔ ( 𝑝 gcd 𝑁 ) = 1 ) )
187	184 185 186	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ¬ 𝑝 ∥ 𝑁 ↔ ( 𝑝 gcd 𝑁 ) = 1 ) )
188	183 187	mpbid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 gcd 𝑁 ) = 1 )
189		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
190	184 189	syl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℤ )
191	160	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑘 ∈ ℕ )
192	191	nnnn0d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑘 ∈ ℕ₀ )
193		rpexp1i	⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ₀ ) → ( ( 𝑝 gcd 𝑁 ) = 1 → ( ( 𝑝 ↑ 𝑘 ) gcd 𝑁 ) = 1 ) )
194	190 185 192 193	syl3anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 𝑝 gcd 𝑁 ) = 1 → ( ( 𝑝 ↑ 𝑘 ) gcd 𝑁 ) = 1 ) )
195	188 194	mpd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 𝑝 ↑ 𝑘 ) gcd 𝑁 ) = 1 )
196	182	nnnn0d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑁 ∈ ℕ₀ )
197	164	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
198	197	adantlrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
199	1 86 2	znunit	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Unit ‘ 𝑍 ) ↔ ( ( 𝑝 ↑ 𝑘 ) gcd 𝑁 ) = 1 ) )
200	196 198 199	syl2anc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Unit ‘ 𝑍 ) ↔ ( ( 𝑝 ↑ 𝑘 ) gcd 𝑁 ) = 1 ) )
201	195 200	mpbird	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Unit ‘ 𝑍 ) )
202	4 1 6 86 182 201	dchr1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) = 1 )
203	202	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) = ( 1 − 1 ) )
204		1m1e0	⊢ ( 1 − 1 ) = 0
205	203 204	eqtrdi	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) = 0 )
206	205	oveq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = ( 0 · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
207	171	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
208	207	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
209	208	adantlrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
210	209	mul02d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 0 · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
211	206 210	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
212	211	sumeq2dv	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) 0 )
213		fzfid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
214	213	olcd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ⊆ ( ℤ_≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ) )
215		sumz	⊢ ( ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ⊆ ( ℤ_≥ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) 0 = 0 )
216	214 215	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) 0 = 0 )
217	212 216	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
218	181 217	sylanr1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∧ ¬ 𝑝 ∥ 𝑁 ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
219	180 218	sylan2b	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∖ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
220		ppifi	⊢ ( 𝑥 ∈ ℝ → ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∈ Fin )
221	141 220	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∈ Fin )
222	155 176 219 221	fsumss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
223	154 222	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
224	156 173	fsumrecl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ )
225	129 224	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ )
226	74	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ∈ ℝ )
227	71	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
228	227	nnrecred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / 𝑝 ) ∈ ℝ )
229	227	nnrpd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ⁺ )
230	229	rpreccld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / 𝑝 ) ∈ ℝ⁺ )
231		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑥 ∈ ℝ⁺ )
232	231	relogcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑥 ) ∈ ℝ )
233	227	nnred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ )
234	75	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ( ℤ_≥ ‘ 2 ) )
235		eluz2gt1	⊢ ( 𝑝 ∈ ( ℤ_≥ ‘ 2 ) → 1 < 𝑝 )
236	234 235	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 1 < 𝑝 )
237	233 236	rplogcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ∈ ℝ⁺ )
238	232 237	rerpdivcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
239	238	flcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
240	239	peano2zd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℤ )
241	230 240	rpexpcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ⁺ )
242	241	rpred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ )
243	228 242	resubcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ∈ ℝ )
244	234 77	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ∈ ℕ )
245	244	nnrpd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ∈ ℝ⁺ )
246	245 229	rpdivcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 − 1 ) / 𝑝 ) ∈ ℝ⁺ )
247	243 246	rerpdivcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ∈ ℝ )
248	226 247	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) ∈ ℝ )
249	170	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℂ )
250	163	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℂ )
251	163	nnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ≠ 0 )
252	249 250 251	divrecd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) · ( 1 / ( 𝑝 ↑ 𝑘 ) ) ) )
253		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℙ )
254		vmappw	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
255	253 161 254	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
256	159	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℂ )
257	159	nnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ≠ 0 )
258		elfzelz	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℤ )
259	258	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℤ )
260	256 257 259	exprecd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( 1 / ( 𝑝 ↑ 𝑘 ) ) )
261	260	eqcomd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 / ( 𝑝 ↑ 𝑘 ) ) = ( ( 1 / 𝑝 ) ↑ 𝑘 ) )
262	255 261	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) · ( 1 / ( 𝑝 ↑ 𝑘 ) ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
263	252 262	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
264	263 171	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) ∈ ℝ )
265	264	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) ∈ ℝ )
266		1red	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 1 ∈ ℝ )
267		vmage0	⊢ ( ( 𝑝 ↑ 𝑘 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
268	163 267	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 0 ≤ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
269	163	nnred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ )
270	163	nngt0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 0 < ( 𝑝 ↑ 𝑘 ) )
271		divge0	⊢ ( ( ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ℝ ∧ 0 ≤ ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∧ ( ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 0 < ( 𝑝 ↑ 𝑘 ) ) ) → 0 ≤ ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
272	170 268 269 270 271	syl22anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 0 ≤ ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
273	84	leidi	⊢ 0 ≤ 0
274		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) = 0 ) → ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) = 0 )
275	273 274	breqtrrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) = 0 ) → 0 ≤ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
276	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ≠ 0 ) → 𝑁 ∈ ℕ )
277	91	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 1 ∈ 𝐷 )
278	4 1 5 25 86 277 165	dchrn0	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ≠ 0 ↔ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Unit ‘ 𝑍 ) ) )
279	278	biimpa	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ≠ 0 ) → ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Unit ‘ 𝑍 ) )
280	4 1 6 86 276 279	dchr1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ≠ 0 ) → ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) = 1 )
281	103 280	breqtrrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ≠ 0 ) → 0 ≤ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
282	275 281	pm2.61dane	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 0 ≤ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) )
283		subge02	⊢ ( ( 1 ∈ ℝ ∧ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ∈ ℝ ) → ( 0 ≤ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ↔ ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) ≤ 1 ) )
284	24 166 283	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 0 ≤ ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ↔ ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) ≤ 1 ) )
285	282 284	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) ≤ 1 )
286	168 266 171 272 285	lemul1ad	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( 1 · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) )
287	207	mullidd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) )
288	287 263	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
289	286 288	breqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
290	289	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
291	156 173 265 290	fsumle	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
292	226	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ∈ ℂ )
293	159	nnrecred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 1 / 𝑝 ) ∈ ℝ )
294	293 162	reexpcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℝ )
295	294	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
296	295	anassrs	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
297	156 292 296	fsummulc2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
298		fzval3	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) = ( 1 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
299	239 298	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) = ( 1 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
300	299	sumeq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( 1 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) )
301	228	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / 𝑝 ) ∈ ℂ )
302	227	nngt0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 0 < 𝑝 )
303		recgt1	⊢ ( ( 𝑝 ∈ ℝ ∧ 0 < 𝑝 ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
304	233 302 303	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
305	236 304	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / 𝑝 ) < 1 )
306	228 305	ltned	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / 𝑝 ) ≠ 1 )
307		1nn0	⊢ 1 ∈ ℕ₀
308	307	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 1 ∈ ℕ₀ )
309		log1	⊢ ( log ‘ 1 ) = 0
310		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
311		1rp	⊢ 1 ∈ ℝ⁺
312		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ⁺ )
313		logleb	⊢ ( ( 1 ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺ ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
314	311 312 313	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) ) )
315	310 314	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 1 ) ≤ ( log ‘ 𝑥 ) )
316	309 315	eqbrtrrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
317	316	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( log ‘ 𝑥 ) )
318	232 237 317	divge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) )
319		flge0nn0	⊢ ( ( ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ₀ )
320	238 318 319	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ₀ )
321		nn0p1nn	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ₀ → ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ )
322	320 321	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ )
323		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
324	322 323	eleqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ_≥ ‘ 1 ) )
325	301 306 308 324	geoserg	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( ( 1 / 𝑝 ) ↑ 1 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) )
326	301	exp1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) ↑ 1 ) = ( 1 / 𝑝 ) )
327	326	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 / 𝑝 ) ↑ 1 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) = ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) )
328	227	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℂ )
329		1cnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 1 ∈ ℂ )
330	229	rpcnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) )
331		divsubdir	⊢ ( ( 𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
332	328 329 330 331	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
333		divid	⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 𝑝 / 𝑝 ) = 1 )
334	330 333	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 / 𝑝 ) = 1 )
335	334	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) = ( 1 − ( 1 / 𝑝 ) ) )
336	332 335	eqtr2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 − ( 1 / 𝑝 ) ) = ( ( 𝑝 − 1 ) / 𝑝 ) )
337	327 336	oveq12d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( ( 1 / 𝑝 ) ↑ 1 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) = ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) )
338	300 325 337	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) )
339	338	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) )
340	297 339	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) )
341	291 340	breqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) )
342	241	rpge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
343	228 242	subge02d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ↔ ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( 1 / 𝑝 ) ) )
344	342 343	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( 1 / 𝑝 ) )
345	245	rpcnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) )
346		dmdcan	⊢ ( ( ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ∧ 1 ∈ ℂ ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) = ( 1 / 𝑝 ) )
347	345 330 329 346	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) = ( 1 / 𝑝 ) )
348	344 347	breqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) )
349	244	nnrecred	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 1 / ( 𝑝 − 1 ) ) ∈ ℝ )
350	243 349 246	ledivmuld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ≤ ( 1 / ( 𝑝 − 1 ) ) ↔ ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) ) )
351	348 350	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ≤ ( 1 / ( 𝑝 − 1 ) ) )
352	247 349 237	lemul2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ≤ ( 1 / ( 𝑝 − 1 ) ) ↔ ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) ) )
353	351 352	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) )
354	244	nncnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ∈ ℂ )
355	244	nnne0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 − 1 ) ≠ 0 )
356	292 354 355	divrecd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 − 1 ) ) ) )
357	353 356	breqtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) · ( ( ( 1 / 𝑝 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( ( 𝑝 − 1 ) / 𝑝 ) ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
358	224 248 130 341 357	letrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
359	129 358	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
360	126 225 131 359	fsumle	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ) ) · ( ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) / ( 𝑝 ↑ 𝑘 ) ) ) ≤ Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
361	223 360	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ≤ Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
362	80	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ )
363	237 245	rpdivcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ∈ ℝ⁺ )
364	363	rpge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
365	70 364	sylan2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ) → 0 ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
366	122 362 365 125	fsumless	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑝 ∈ { 𝑞 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) ≤ Σ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
367	102 132 133 361 366	letrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ≤ Σ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
368	121 367	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ≤ Σ 𝑝 ∈ { 𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁 } ( ( log ‘ 𝑝 ) / ( 𝑝 − 1 ) ) )
369	66 41 67 81 368	elo1d	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )
370		o1sub	⊢ ( ( ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘_f − ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) ∈ 𝑂(1) )
371	65 369 370	sylancr	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘_f − ( 𝑥 ∈ ℝ⁺ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 − ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ) ∈ 𝑂(1) )
372	64 371	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )

Metamath Proof Explorer

Theorem rpvmasumlem

Proof