Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝐺 )
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 = ( 0g ‘ 𝐺 )
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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
29 1 25 2 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
30 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
31 28 29 30 3syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
32 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
33 ffvelrn ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) )
34 31 32 33 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑛 ) ∈ ( Base ‘ 𝑍 ) )
35 27 34 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 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 mulid2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 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 ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ0 )
163 159 162 nnexpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
164 163 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
165 158 164 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( Base ‘ 𝑍 ) )
166 157 165 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 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 ‘ 𝑝 ) ) ) ) ) → 𝑘 ∈ ℕ0 )
193 rpexp1i ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑝 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 ‘ 𝑝 ) ) ) ) ) → 𝑁 ∈ ℕ0 )
197 164 anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
198 197 adantlrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑝 ∈ ℙ ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
199 1 86 2 znunit ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑝 ↑ 𝑘 ) ) ∈ ( 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 mulid2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 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 ∈ ℕ0
308 307 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → 1 ∈ ℕ0 )
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 ‘ 𝑝 ) ) ) ∈ ℕ0 )
320 238 318 319 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑝 ∈ ℙ ) → ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
321 nn0p1nn ⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( ( 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) )