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
|- ( A e. ZZ -> sum_ n e. ( 1 ... A ) ( ( ( Lam ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) <_ 2 )

Proof

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