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 )