Metamath Proof Explorer


Theorem rplogsumlem2

Description: Lemma for rplogsum . Equation 9.2.14 of Shapiro, p. 331. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion rplogsumlem2 ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ≤ 2 )

Proof

Step Hyp Ref Expression
1 flid ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
2 1 oveq2d ( 𝐴 ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( 1 ... 𝐴 ) )
3 2 sumeq1d ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) )
4 fveq2 ( 𝑛 = ( 𝑝𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝𝑘 ) ) )
5 eleq1 ( 𝑛 = ( 𝑝𝑘 ) → ( 𝑛 ∈ ℙ ↔ ( 𝑝𝑘 ) ∈ ℙ ) )
6 fveq2 ( 𝑛 = ( 𝑝𝑘 ) → ( log ‘ 𝑛 ) = ( log ‘ ( 𝑝𝑘 ) ) )
7 5 6 ifbieq1d ( 𝑛 = ( 𝑝𝑘 ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) = if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) )
8 4 7 oveq12d ( 𝑛 = ( 𝑝𝑘 ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) )
9 id ( 𝑛 = ( 𝑝𝑘 ) → 𝑛 = ( 𝑝𝑘 ) )
10 8 9 oveq12d ( 𝑛 = ( 𝑝𝑘 ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) )
11 zre ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
12 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
13 12 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
14 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
15 13 14 syl ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
16 13 nnrpd ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ+ )
17 16 relogcld ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
18 0re 0 ∈ ℝ
19 ifcl ( ( ( log ‘ 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ∈ ℝ )
20 17 18 19 sylancl ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ∈ ℝ )
21 15 20 resubcld ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) ∈ ℝ )
22 21 13 nndivred ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ∈ ℝ )
23 22 recnd ( ( 𝐴 ∈ ℤ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ∈ ℂ )
24 simprr ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
25 vmaprm ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) = ( log ‘ 𝑛 ) )
26 prmnn ( 𝑛 ∈ ℙ → 𝑛 ∈ ℕ )
27 26 nnred ( 𝑛 ∈ ℙ → 𝑛 ∈ ℝ )
28 prmgt1 ( 𝑛 ∈ ℙ → 1 < 𝑛 )
29 27 28 rplogcld ( 𝑛 ∈ ℙ → ( log ‘ 𝑛 ) ∈ ℝ+ )
30 25 29 eqeltrd ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) ∈ ℝ+ )
31 30 rpne0d ( 𝑛 ∈ ℙ → ( Λ ‘ 𝑛 ) ≠ 0 )
32 31 necon2bi ( ( Λ ‘ 𝑛 ) = 0 → ¬ 𝑛 ∈ ℙ )
33 32 ad2antll ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ¬ 𝑛 ∈ ℙ )
34 33 iffalsed ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) = 0 )
35 24 34 oveq12d ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = ( 0 − 0 ) )
36 0m0e0 ( 0 − 0 ) = 0
37 35 36 eqtrdi ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) = 0 )
38 37 oveq1d ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = ( 0 / 𝑛 ) )
39 12 ad2antrl ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℕ )
40 39 nnrpd ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → 𝑛 ∈ ℝ+ )
41 40 rpcnne0d ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
42 div0 ( ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) → ( 0 / 𝑛 ) = 0 )
43 41 42 syl ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( 0 / 𝑛 ) = 0 )
44 38 43 eqtrd ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = 0 )
45 10 11 23 44 fsumvma2 ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) )
46 3 45 eqtr3d ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) )
47 fzfid ( 𝐴 ∈ ℤ → ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ∈ Fin )
48 simpr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
49 48 elin2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
50 prmnn ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
51 49 50 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
52 51 nnred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
53 11 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
54 zcn ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
55 54 abscld ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℝ )
56 peano2re ( ( abs ‘ 𝐴 ) ∈ ℝ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
57 55 56 syl ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
58 57 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℝ )
59 elinel1 ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
60 elicc2 ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴 ) ) )
61 18 11 60 sylancr ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴 ) ) )
62 59 61 syl5ib ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴 ) ) )
63 62 imp ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴 ) )
64 63 simp3d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝𝐴 )
65 54 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℂ )
66 65 abscld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
67 53 leabsd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
68 66 lep1d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( abs ‘ 𝐴 ) ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
69 53 66 58 67 68 letrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
70 52 53 58 64 69 letrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) )
71 prmuz2 ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ ‘ 2 ) )
72 49 71 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ ‘ 2 ) )
73 nn0abscl ( 𝐴 ∈ ℤ → ( abs ‘ 𝐴 ) ∈ ℕ0 )
74 nn0p1nn ( ( abs ‘ 𝐴 ) ∈ ℕ0 → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ )
75 73 74 syl ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ )
76 75 nnzd ( 𝐴 ∈ ℤ → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ )
77 76 adantr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ )
78 elfz5 ( ( 𝑝 ∈ ( ℤ ‘ 2 ) ∧ ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℤ ) → ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ↔ 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
79 72 77 78 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ↔ 𝑝 ≤ ( ( abs ‘ 𝐴 ) + 1 ) ) )
80 70 79 mpbird ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) )
81 80 ex ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) )
82 81 ssrdv ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) )
83 47 82 ssfid ( 𝐴 ∈ ℤ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
84 fzfid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
85 simprl ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
86 85 elin2d ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℙ )
87 elfznn ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
88 87 ad2antll ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ )
89 vmappw ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝𝑘 ) ) = ( log ‘ 𝑝 ) )
90 86 88 89 syl2anc ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝𝑘 ) ) = ( log ‘ 𝑝 ) )
91 51 adantrr ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℕ )
92 91 nnrpd ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑝 ∈ ℝ+ )
93 92 relogcld ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
94 90 93 eqeltrd ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( Λ ‘ ( 𝑝𝑘 ) ) ∈ ℝ )
95 88 nnnn0d ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → 𝑘 ∈ ℕ0 )
96 nnexpcl ( ( 𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝𝑘 ) ∈ ℕ )
97 91 95 96 syl2anc ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝𝑘 ) ∈ ℕ )
98 97 nnrpd ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( 𝑝𝑘 ) ∈ ℝ+ )
99 98 relogcld ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ ( 𝑝𝑘 ) ) ∈ ℝ )
100 ifcl ( ( ( log ‘ ( 𝑝𝑘 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ∈ ℝ )
101 99 18 100 sylancl ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ∈ ℝ )
102 94 101 resubcld ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) ∈ ℝ )
103 102 97 nndivred ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℝ )
104 103 anassrs ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℝ )
105 84 104 fsumrecl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℝ )
106 83 105 fsumrecl ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℝ )
107 51 nnrpd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
108 107 relogcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
109 uz2m1nn ( 𝑝 ∈ ( ℤ ‘ 2 ) → ( 𝑝 − 1 ) ∈ ℕ )
110 72 109 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 − 1 ) ∈ ℕ )
111 51 110 nnmulcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℕ )
112 108 111 nndivred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
113 83 112 fsumrecl ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
114 2re 2 ∈ ℝ
115 114 a1i ( 𝐴 ∈ ℤ → 2 ∈ ℝ )
116 18 a1i ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ∈ ℝ )
117 51 nngt0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝑝 )
118 116 52 53 117 64 ltletrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝐴 )
119 53 118 elrpd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ )
120 119 relogcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
121 prmgt1 ( 𝑝 ∈ ℙ → 1 < 𝑝 )
122 49 121 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
123 52 122 rplogcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
124 120 123 rerpdivcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
125 123 rpcnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
126 125 mulid2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 · ( log ‘ 𝑝 ) ) = ( log ‘ 𝑝 ) )
127 107 119 logled ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝𝐴 ↔ ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ) )
128 64 127 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) )
129 126 128 eqbrtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) )
130 1re 1 ∈ ℝ
131 130 a1i ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℝ )
132 131 120 123 lemuldivd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
133 129 132 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
134 flge1nn ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ )
135 124 133 134 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ )
136 nnuz ℕ = ( ℤ ‘ 1 )
137 135 136 eleqtrdi ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ( ℤ ‘ 1 ) )
138 103 recnd ( ( 𝐴 ∈ ℤ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℂ )
139 138 anassrs ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ∈ ℂ )
140 oveq2 ( 𝑘 = 1 → ( 𝑝𝑘 ) = ( 𝑝 ↑ 1 ) )
141 140 fveq2d ( 𝑘 = 1 → ( Λ ‘ ( 𝑝𝑘 ) ) = ( Λ ‘ ( 𝑝 ↑ 1 ) ) )
142 140 eleq1d ( 𝑘 = 1 → ( ( 𝑝𝑘 ) ∈ ℙ ↔ ( 𝑝 ↑ 1 ) ∈ ℙ ) )
143 140 fveq2d ( 𝑘 = 1 → ( log ‘ ( 𝑝𝑘 ) ) = ( log ‘ ( 𝑝 ↑ 1 ) ) )
144 142 143 ifbieq1d ( 𝑘 = 1 → if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) = if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) )
145 141 144 oveq12d ( 𝑘 = 1 → ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) = ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) )
146 145 140 oveq12d ( 𝑘 = 1 → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) = ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) )
147 137 139 146 fsum1p ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) = ( ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) + Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ) )
148 51 nncnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℂ )
149 148 exp1d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ 1 ) = 𝑝 )
150 149 fveq2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ ( 𝑝 ↑ 1 ) ) = ( Λ ‘ 𝑝 ) )
151 vmaprm ( 𝑝 ∈ ℙ → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
152 49 151 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
153 150 152 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( Λ ‘ ( 𝑝 ↑ 1 ) ) = ( log ‘ 𝑝 ) )
154 149 49 eqeltrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ 1 ) ∈ ℙ )
155 154 iftrued ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) = ( log ‘ ( 𝑝 ↑ 1 ) ) )
156 149 fveq2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ ( 𝑝 ↑ 1 ) ) = ( log ‘ 𝑝 ) )
157 155 156 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) = ( log ‘ 𝑝 ) )
158 153 157 oveq12d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) = ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) )
159 125 subidd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) = 0 )
160 158 159 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) = 0 )
161 160 149 oveq12d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) = ( 0 / 𝑝 ) )
162 107 rpcnne0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) )
163 div0 ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 0 / 𝑝 ) = 0 )
164 162 163 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 / 𝑝 ) = 0 )
165 161 164 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) = 0 )
166 1p1e2 ( 1 + 1 ) = 2
167 166 oveq1i ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
168 167 a1i ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
169 elfzuz ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ( ℤ ‘ 2 ) )
170 eluz2nn ( 𝑘 ∈ ( ℤ ‘ 2 ) → 𝑘 ∈ ℕ )
171 169 170 syl ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
172 171 167 eleq2s ( 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
173 49 172 89 syl2an ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( Λ ‘ ( 𝑝𝑘 ) ) = ( log ‘ 𝑝 ) )
174 51 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℕ )
175 nnq ( 𝑝 ∈ ℕ → 𝑝 ∈ ℚ )
176 174 175 syl ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑝 ∈ ℚ )
177 169 167 eleq2s ( 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ( ℤ ‘ 2 ) )
178 177 adantl ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 𝑘 ∈ ( ℤ ‘ 2 ) )
179 expnprm ( ( 𝑝 ∈ ℚ ∧ 𝑘 ∈ ( ℤ ‘ 2 ) ) → ¬ ( 𝑝𝑘 ) ∈ ℙ )
180 176 178 179 syl2anc ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ¬ ( 𝑝𝑘 ) ∈ ℙ )
181 180 iffalsed ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) = 0 )
182 173 181 oveq12d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) = ( ( log ‘ 𝑝 ) − 0 ) )
183 125 subid1d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) − 0 ) = ( log ‘ 𝑝 ) )
184 183 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) − 0 ) = ( log ‘ 𝑝 ) )
185 182 184 eqtrd ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) = ( log ‘ 𝑝 ) )
186 185 oveq1d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) = ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) )
187 168 186 sumeq12dv ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) )
188 165 187 oveq12d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( Λ ‘ ( 𝑝 ↑ 1 ) ) − if ( ( 𝑝 ↑ 1 ) ∈ ℙ , ( log ‘ ( 𝑝 ↑ 1 ) ) , 0 ) ) / ( 𝑝 ↑ 1 ) ) + Σ 𝑘 ∈ ( ( 1 + 1 ) ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ) = ( 0 + Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ) )
189 fzfid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
190 108 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℝ )
191 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
192 51 191 96 syl2an ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝𝑘 ) ∈ ℕ )
193 190 192 nndivred ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ∈ ℝ )
194 171 193 sylan2 ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ∈ ℝ )
195 189 194 fsumrecl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ∈ ℝ )
196 195 recnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ∈ ℂ )
197 196 addid2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 + Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) )
198 147 188 197 3eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) )
199 107 rpreccld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℝ+ )
200 124 flcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
201 200 peano2zd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℤ )
202 199 201 rpexpcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ+ )
203 202 rpge0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
204 51 nnrecred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℝ )
205 204 resqcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ 2 ) ∈ ℝ )
206 135 peano2nnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ )
207 206 nnnn0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ℕ0 )
208 204 207 reexpcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ∈ ℝ )
209 205 208 subge02d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 0 ≤ ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 / 𝑝 ) ↑ 2 ) ) )
210 203 209 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 / 𝑝 ) ↑ 2 ) )
211 110 nnrpd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 − 1 ) ∈ ℝ+ )
212 211 rpcnne0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) )
213 199 rpcnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ∈ ℂ )
214 dmdcan ( ( ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ∧ ( 1 / 𝑝 ) ∈ ℂ ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 / 𝑝 ) / 𝑝 ) )
215 212 162 213 214 syl3anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 / 𝑝 ) / 𝑝 ) )
216 131 recnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℂ )
217 divsubdir ( ( 𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
218 148 216 162 217 syl3anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) )
219 divid ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 𝑝 / 𝑝 ) = 1 )
220 162 219 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 / 𝑝 ) = 1 )
221 220 oveq1d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 / 𝑝 ) − ( 1 / 𝑝 ) ) = ( 1 − ( 1 / 𝑝 ) ) )
222 218 221 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 𝑝 − 1 ) / 𝑝 ) = ( 1 − ( 1 / 𝑝 ) ) )
223 divdiv1 ( ( 1 ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ∧ ( ( 𝑝 − 1 ) ∈ ℂ ∧ ( 𝑝 − 1 ) ≠ 0 ) ) → ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) = ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
224 216 162 212 223 syl3anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) = ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
225 222 224 oveq12d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 𝑝 − 1 ) / 𝑝 ) · ( ( 1 / 𝑝 ) / ( 𝑝 − 1 ) ) ) = ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
226 51 nnne0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≠ 0 )
227 213 148 226 divrecd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / 𝑝 ) = ( ( 1 / 𝑝 ) · ( 1 / 𝑝 ) ) )
228 213 sqvald ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) ↑ 2 ) = ( ( 1 / 𝑝 ) · ( 1 / 𝑝 ) ) )
229 227 228 eqtr4d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) / 𝑝 ) = ( ( 1 / 𝑝 ) ↑ 2 ) )
230 215 225 229 3eqtr3d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) = ( ( 1 / 𝑝 ) ↑ 2 ) )
231 210 230 breqtrrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
232 205 208 resubcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ∈ ℝ )
233 111 nnrecred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
234 resubcl ( ( 1 ∈ ℝ ∧ ( 1 / 𝑝 ) ∈ ℝ ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ )
235 130 204 234 sylancr ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ )
236 recgt1 ( ( 𝑝 ∈ ℝ ∧ 0 < 𝑝 ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
237 52 117 236 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 < 𝑝 ↔ ( 1 / 𝑝 ) < 1 ) )
238 122 237 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) < 1 )
239 posdif ( ( ( 1 / 𝑝 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 𝑝 ) < 1 ↔ 0 < ( 1 − ( 1 / 𝑝 ) ) ) )
240 204 130 239 sylancl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( 1 / 𝑝 ) < 1 ↔ 0 < ( 1 − ( 1 / 𝑝 ) ) ) )
241 238 240 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < ( 1 − ( 1 / 𝑝 ) ) )
242 ledivmul ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ∈ ℝ ∧ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ ∧ ( ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ ∧ 0 < ( 1 − ( 1 / 𝑝 ) ) ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
243 232 233 235 241 242 syl112anc ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) ≤ ( ( 1 − ( 1 / 𝑝 ) ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
244 231 243 mpbird ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
245 235 241 elrpd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 − ( 1 / 𝑝 ) ) ∈ ℝ+ )
246 232 245 rerpdivcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ∈ ℝ )
247 246 233 123 lemul2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ≤ ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ↔ ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) ) )
248 244 247 mpbid ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) ≤ ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
249 125 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℂ )
250 192 nncnd ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝𝑘 ) ∈ ℂ )
251 192 nnne0d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑝𝑘 ) ≠ 0 )
252 249 250 251 divrecd ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝𝑘 ) ) ) )
253 148 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℂ )
254 51 adantr ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ∈ ℕ )
255 254 nnne0d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑝 ≠ 0 )
256 nnz ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
257 256 adantl ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ )
258 253 255 257 exprecd ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( 1 / ( 𝑝𝑘 ) ) )
259 258 oveq2d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝𝑘 ) ) ) )
260 252 259 eqtr4d ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ℕ ) → ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
261 171 260 sylan2 ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
262 261 sumeq2dv ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
263 171 nnnn0d ( 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ0 )
264 expcl ( ( ( 1 / 𝑝 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
265 213 263 264 syl2an ( ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 1 / 𝑝 ) ↑ 𝑘 ) ∈ ℂ )
266 189 125 265 fsummulc2 ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) · ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) )
267 fzval3 ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
268 200 267 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) )
269 268 sumeq1d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = Σ 𝑘 ∈ ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) )
270 204 238 ltned ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 / 𝑝 ) ≠ 1 )
271 2nn0 2 ∈ ℕ0
272 271 a1i ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 2 ∈ ℕ0 )
273 eluzp1p1 ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ( ℤ ‘ 1 ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ ‘ ( 1 + 1 ) ) )
274 137 273 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ ‘ ( 1 + 1 ) ) )
275 df-2 2 = ( 1 + 1 )
276 275 fveq2i ( ℤ ‘ 2 ) = ( ℤ ‘ ( 1 + 1 ) )
277 274 276 eleqtrrdi ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ∈ ( ℤ ‘ 2 ) )
278 213 270 272 277 geoserg ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ..^ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) )
279 269 278 eqtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) = ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) )
280 279 oveq2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( 1 / 𝑝 ) ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) )
281 262 266 280 3eqtr2d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ( ( ( 1 / 𝑝 ) ↑ 2 ) − ( ( 1 / 𝑝 ) ↑ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) + 1 ) ) ) / ( 1 − ( 1 / 𝑝 ) ) ) ) )
282 111 nncnd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℂ )
283 111 nnne0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ≠ 0 )
284 125 282 283 divrecd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) = ( ( log ‘ 𝑝 ) · ( 1 / ( 𝑝 · ( 𝑝 − 1 ) ) ) ) )
285 248 281 284 3brtr4d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 2 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( log ‘ 𝑝 ) / ( 𝑝𝑘 ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
286 198 285 eqbrtrd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
287 83 105 112 286 fsumle ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
288 elfzuz ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) → 𝑝 ∈ ( ℤ ‘ 2 ) )
289 eluz2nn ( 𝑝 ∈ ( ℤ ‘ 2 ) → 𝑝 ∈ ℕ )
290 288 289 syl ( 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) → 𝑝 ∈ ℕ )
291 290 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ℕ )
292 291 nnred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ℝ )
293 288 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 𝑝 ∈ ( ℤ ‘ 2 ) )
294 eluz2gt1 ( 𝑝 ∈ ( ℤ ‘ 2 ) → 1 < 𝑝 )
295 293 294 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 1 < 𝑝 )
296 292 295 rplogcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
297 293 109 syl ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 − 1 ) ∈ ℕ )
298 291 297 nnmulcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℕ )
299 298 nnrpd ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( 𝑝 · ( 𝑝 − 1 ) ) ∈ ℝ+ )
300 296 299 rpdivcld ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ+ )
301 300 rpred ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
302 47 301 fsumrecl ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ∈ ℝ )
303 300 rpge0d ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ) → 0 ≤ ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
304 47 301 303 82 fsumless ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) )
305 rplogsumlem1 ( ( ( abs ‘ 𝐴 ) + 1 ) ∈ ℕ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
306 75 305 syl ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( 2 ... ( ( abs ‘ 𝐴 ) + 1 ) ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
307 113 302 115 304 306 letrd ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) / ( 𝑝 · ( 𝑝 − 1 ) ) ) ≤ 2 )
308 106 113 115 287 307 letrd ( 𝐴 ∈ ℤ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( ( ( Λ ‘ ( 𝑝𝑘 ) ) − if ( ( 𝑝𝑘 ) ∈ ℙ , ( log ‘ ( 𝑝𝑘 ) ) , 0 ) ) / ( 𝑝𝑘 ) ) ≤ 2 )
309 46 308 eqbrtrd ( 𝐴 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... 𝐴 ) ( ( ( Λ ‘ 𝑛 ) − if ( 𝑛 ∈ ℙ , ( log ‘ 𝑛 ) , 0 ) ) / 𝑛 ) ≤ 2 )