This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( 𝐴 ∈ ℤ → ( 𝑝 ∈ ( ( 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 mullidd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 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 addlidd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑝 ∈ ( ( 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 )