Metamath Proof Explorer


Theorem chpchtsum

Description: The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion chpchtsum
|- ( A e. RR -> ( psi ` A ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( theta ` ( A ^c ( 1 / k ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin )
2 simpr
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
3 2 elin2d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
4 prmnn
 |-  ( p e. Prime -> p e. NN )
5 3 4 syl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN )
6 5 nnrpd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR+ )
7 6 relogcld
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR )
8 7 recnd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. CC )
9 fsumconst
 |-  ( ( ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin /\ ( log ` p ) e. CC ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) )
10 1 8 9 syl2anc
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) )
11 simpl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. RR )
12 1red
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 e. RR )
13 5 nnred
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR )
14 prmuz2
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
15 3 14 syl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ZZ>= ` 2 ) )
16 eluz2gt1
 |-  ( p e. ( ZZ>= ` 2 ) -> 1 < p )
17 15 16 syl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 < p )
18 2 elin1d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( 0 [,] A ) )
19 0re
 |-  0 e. RR
20 elicc2
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
21 19 11 20 sylancr
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
22 18 21 mpbid
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. RR /\ 0 <_ p /\ p <_ A ) )
23 22 simp3d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p <_ A )
24 12 13 11 17 23 ltletrd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 < A )
25 11 24 rplogcld
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` A ) e. RR+ )
26 13 17 rplogcld
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
27 25 26 rpdivcld
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR+ )
28 27 rpred
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR )
29 27 rpge0d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 <_ ( ( log ` A ) / ( log ` p ) ) )
30 flge0nn0
 |-  ( ( ( ( log ` A ) / ( log ` p ) ) e. RR /\ 0 <_ ( ( log ` A ) / ( log ` p ) ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 )
31 28 29 30 syl2anc
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 )
32 hashfz1
 |-  ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) = ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) )
33 31 32 syl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) = ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) )
34 33 oveq1d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( # ` ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) x. ( log ` p ) ) = ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) x. ( log ` p ) ) )
35 28 flcld
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ )
36 35 zcnd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. CC )
37 36 8 mulcomd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) x. ( log ` p ) ) = ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
38 10 34 37 3eqtrrd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) )
39 38 sumeq2dv
 |-  ( A e. RR -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) )
40 chpval2
 |-  ( A e. RR -> ( psi ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
41 simpl
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> A e. RR )
42 0red
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 0 e. RR )
43 1red
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 1 e. RR )
44 0lt1
 |-  0 < 1
45 44 a1i
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 0 < 1 )
46 elfzuz2
 |-  ( k e. ( 1 ... ( |_ ` A ) ) -> ( |_ ` A ) e. ( ZZ>= ` 1 ) )
47 eluzle
 |-  ( ( |_ ` A ) e. ( ZZ>= ` 1 ) -> 1 <_ ( |_ ` A ) )
48 47 adantl
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 1 ) ) -> 1 <_ ( |_ ` A ) )
49 simpl
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 1 ) ) -> A e. RR )
50 1z
 |-  1 e. ZZ
51 flge
 |-  ( ( A e. RR /\ 1 e. ZZ ) -> ( 1 <_ A <-> 1 <_ ( |_ ` A ) ) )
52 49 50 51 sylancl
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 1 ) ) -> ( 1 <_ A <-> 1 <_ ( |_ ` A ) ) )
53 48 52 mpbird
 |-  ( ( A e. RR /\ ( |_ ` A ) e. ( ZZ>= ` 1 ) ) -> 1 <_ A )
54 46 53 sylan2
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 1 <_ A )
55 42 43 41 45 54 ltletrd
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 0 < A )
56 42 41 55 ltled
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ A )
57 elfznn
 |-  ( k e. ( 1 ... ( |_ ` A ) ) -> k e. NN )
58 57 adantl
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> k e. NN )
59 58 nnrecred
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / k ) e. RR )
60 41 56 59 recxpcld
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( A ^c ( 1 / k ) ) e. RR )
61 chtval
 |-  ( ( A ^c ( 1 / k ) ) e. RR -> ( theta ` ( A ^c ( 1 / k ) ) ) = sum_ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ( log ` p ) )
62 60 61 syl
 |-  ( ( A e. RR /\ k e. ( 1 ... ( |_ ` A ) ) ) -> ( theta ` ( A ^c ( 1 / k ) ) ) = sum_ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ( log ` p ) )
63 62 sumeq2dv
 |-  ( A e. RR -> sum_ k e. ( 1 ... ( |_ ` A ) ) ( theta ` ( A ^c ( 1 / k ) ) ) = sum_ k e. ( 1 ... ( |_ ` A ) ) sum_ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ( log ` p ) )
64 ppifi
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
65 fzfid
 |-  ( A e. RR -> ( 1 ... ( |_ ` A ) ) e. Fin )
66 elinel2
 |-  ( p e. ( ( 0 [,] A ) i^i Prime ) -> p e. Prime )
67 elfznn
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
68 66 67 anim12i
 |-  ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( p e. Prime /\ k e. NN ) )
69 68 a1i
 |-  ( A e. RR -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( p e. Prime /\ k e. NN ) ) )
70 0red
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 e. RR )
71 inss2
 |-  ( ( 0 [,] A ) i^i Prime ) C_ Prime
72 71 a1i
 |-  ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) C_ Prime )
73 72 sselda
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
74 73 4 syl
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN )
75 74 nnred
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR )
76 74 nngt0d
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 < p )
77 70 75 11 76 23 ltletrd
 |-  ( ( A e. RR /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 < A )
78 77 ex
 |-  ( A e. RR -> ( p e. ( ( 0 [,] A ) i^i Prime ) -> 0 < A ) )
79 78 adantrd
 |-  ( A e. RR -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> 0 < A ) )
80 69 79 jcad
 |-  ( A e. RR -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) )
81 elinel2
 |-  ( p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) -> p e. Prime )
82 57 81 anim12ci
 |-  ( ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) -> ( p e. Prime /\ k e. NN ) )
83 82 a1i
 |-  ( A e. RR -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) -> ( p e. Prime /\ k e. NN ) ) )
84 55 ex
 |-  ( A e. RR -> ( k e. ( 1 ... ( |_ ` A ) ) -> 0 < A ) )
85 84 adantrd
 |-  ( A e. RR -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) -> 0 < A ) )
86 83 85 jcad
 |-  ( A e. RR -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) -> ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) )
87 elin
 |-  ( p e. ( ( 0 [,] A ) i^i Prime ) <-> ( p e. ( 0 [,] A ) /\ p e. Prime ) )
88 simprll
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. Prime )
89 88 biantrud
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( 0 [,] A ) <-> ( p e. ( 0 [,] A ) /\ p e. Prime ) ) )
90 0red
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 0 e. RR )
91 simpl
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> A e. RR )
92 88 4 syl
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. NN )
93 92 nnred
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. RR )
94 92 nnnn0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. NN0 )
95 94 nn0ge0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 0 <_ p )
96 df-3an
 |-  ( ( p e. RR /\ 0 <_ p /\ p <_ A ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ A ) )
97 20 96 bitrdi
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ A ) ) )
98 97 baibd
 |-  ( ( ( 0 e. RR /\ A e. RR ) /\ ( p e. RR /\ 0 <_ p ) ) -> ( p e. ( 0 [,] A ) <-> p <_ A ) )
99 90 91 93 95 98 syl22anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( 0 [,] A ) <-> p <_ A ) )
100 89 99 bitr3d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p e. ( 0 [,] A ) /\ p e. Prime ) <-> p <_ A ) )
101 87 100 syl5bb
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( ( 0 [,] A ) i^i Prime ) <-> p <_ A ) )
102 simprr
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 0 < A )
103 91 102 elrpd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> A e. RR+ )
104 103 relogcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( log ` A ) e. RR )
105 88 14 syl
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. ( ZZ>= ` 2 ) )
106 105 16 syl
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 1 < p )
107 93 106 rplogcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( log ` p ) e. RR+ )
108 104 107 rerpdivcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR )
109 simprlr
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. NN )
110 109 nnzd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. ZZ )
111 flge
 |-  ( ( ( ( log ` A ) / ( log ` p ) ) e. RR /\ k e. ZZ ) -> ( k <_ ( ( log ` A ) / ( log ` p ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
112 108 110 111 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k <_ ( ( log ` A ) / ( log ` p ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
113 109 nnnn0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. NN0 )
114 92 113 nnexpcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^ k ) e. NN )
115 114 nnrpd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^ k ) e. RR+ )
116 115 103 logled
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A <-> ( log ` ( p ^ k ) ) <_ ( log ` A ) ) )
117 92 nnrpd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. RR+ )
118 relogexp
 |-  ( ( p e. RR+ /\ k e. ZZ ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
119 117 110 118 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( log ` ( p ^ k ) ) = ( k x. ( log ` p ) ) )
120 119 breq1d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( log ` ( p ^ k ) ) <_ ( log ` A ) <-> ( k x. ( log ` p ) ) <_ ( log ` A ) ) )
121 109 nnred
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. RR )
122 121 104 107 lemuldivd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( k x. ( log ` p ) ) <_ ( log ` A ) <-> k <_ ( ( log ` A ) / ( log ` p ) ) ) )
123 116 120 122 3bitrd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A <-> k <_ ( ( log ` A ) / ( log ` p ) ) ) )
124 nnuz
 |-  NN = ( ZZ>= ` 1 )
125 109 124 eleqtrdi
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. ( ZZ>= ` 1 ) )
126 108 flcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ )
127 elfz5
 |-  ( ( k e. ( ZZ>= ` 1 ) /\ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
128 125 126 127 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) <-> k <_ ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
129 112 123 128 3bitr4rd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) <-> ( p ^ k ) <_ A ) )
130 101 129 anbi12d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( p <_ A /\ ( p ^ k ) <_ A ) ) )
131 91 flcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( |_ ` A ) e. ZZ )
132 elfz5
 |-  ( ( k e. ( ZZ>= ` 1 ) /\ ( |_ ` A ) e. ZZ ) -> ( k e. ( 1 ... ( |_ ` A ) ) <-> k <_ ( |_ ` A ) ) )
133 125 131 132 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k e. ( 1 ... ( |_ ` A ) ) <-> k <_ ( |_ ` A ) ) )
134 flge
 |-  ( ( A e. RR /\ k e. ZZ ) -> ( k <_ A <-> k <_ ( |_ ` A ) ) )
135 91 110 134 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k <_ A <-> k <_ ( |_ ` A ) ) )
136 133 135 bitr4d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( k e. ( 1 ... ( |_ ` A ) ) <-> k <_ A ) )
137 elin
 |-  ( p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) <-> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) /\ p e. Prime ) )
138 88 biantrud
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) <-> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) /\ p e. Prime ) ) )
139 103 rpge0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 0 <_ A )
140 109 nnrecred
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( 1 / k ) e. RR )
141 91 139 140 recxpcld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( A ^c ( 1 / k ) ) e. RR )
142 elicc2
 |-  ( ( 0 e. RR /\ ( A ^c ( 1 / k ) ) e. RR ) -> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) <-> ( p e. RR /\ 0 <_ p /\ p <_ ( A ^c ( 1 / k ) ) ) ) )
143 df-3an
 |-  ( ( p e. RR /\ 0 <_ p /\ p <_ ( A ^c ( 1 / k ) ) ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ ( A ^c ( 1 / k ) ) ) )
144 142 143 bitrdi
 |-  ( ( 0 e. RR /\ ( A ^c ( 1 / k ) ) e. RR ) -> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) <-> ( ( p e. RR /\ 0 <_ p ) /\ p <_ ( A ^c ( 1 / k ) ) ) ) )
145 144 baibd
 |-  ( ( ( 0 e. RR /\ ( A ^c ( 1 / k ) ) e. RR ) /\ ( p e. RR /\ 0 <_ p ) ) -> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) <-> p <_ ( A ^c ( 1 / k ) ) ) )
146 90 141 93 95 145 syl22anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) <-> p <_ ( A ^c ( 1 / k ) ) ) )
147 138 146 bitr3d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) /\ p e. Prime ) <-> p <_ ( A ^c ( 1 / k ) ) ) )
148 91 139 140 cxpge0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 0 <_ ( A ^c ( 1 / k ) ) )
149 109 nnrpd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. RR+ )
150 93 95 141 148 149 cxple2d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p <_ ( A ^c ( 1 / k ) ) <-> ( p ^c k ) <_ ( ( A ^c ( 1 / k ) ) ^c k ) ) )
151 92 nncnd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p e. CC )
152 cxpexp
 |-  ( ( p e. CC /\ k e. NN0 ) -> ( p ^c k ) = ( p ^ k ) )
153 151 113 152 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^c k ) = ( p ^ k ) )
154 109 nncnd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k e. CC )
155 109 nnne0d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k =/= 0 )
156 154 155 recid2d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( 1 / k ) x. k ) = 1 )
157 156 oveq2d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( A ^c ( ( 1 / k ) x. k ) ) = ( A ^c 1 ) )
158 103 140 154 cxpmuld
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( A ^c ( ( 1 / k ) x. k ) ) = ( ( A ^c ( 1 / k ) ) ^c k ) )
159 91 recnd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> A e. CC )
160 159 cxp1d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( A ^c 1 ) = A )
161 157 158 160 3eqtr3d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( A ^c ( 1 / k ) ) ^c k ) = A )
162 153 161 breq12d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^c k ) <_ ( ( A ^c ( 1 / k ) ) ^c k ) <-> ( p ^ k ) <_ A ) )
163 147 150 162 3bitrd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p e. ( 0 [,] ( A ^c ( 1 / k ) ) ) /\ p e. Prime ) <-> ( p ^ k ) <_ A ) )
164 137 163 syl5bb
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) <-> ( p ^ k ) <_ A ) )
165 136 164 anbi12d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) <-> ( k <_ A /\ ( p ^ k ) <_ A ) ) )
166 114 nnred
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^ k ) e. RR )
167 bernneq3
 |-  ( ( p e. ( ZZ>= ` 2 ) /\ k e. NN0 ) -> k < ( p ^ k ) )
168 105 113 167 syl2anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k < ( p ^ k ) )
169 121 166 168 ltled
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> k <_ ( p ^ k ) )
170 letr
 |-  ( ( k e. RR /\ ( p ^ k ) e. RR /\ A e. RR ) -> ( ( k <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> k <_ A ) )
171 121 166 91 170 syl3anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( k <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> k <_ A ) )
172 169 171 mpand
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A -> k <_ A ) )
173 172 pm4.71rd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A <-> ( k <_ A /\ ( p ^ k ) <_ A ) ) )
174 151 exp1d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^ 1 ) = p )
175 92 nnge1d
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> 1 <_ p )
176 93 175 125 leexp2ad
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( p ^ 1 ) <_ ( p ^ k ) )
177 174 176 eqbrtrrd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> p <_ ( p ^ k ) )
178 letr
 |-  ( ( p e. RR /\ ( p ^ k ) e. RR /\ A e. RR ) -> ( ( p <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> p <_ A ) )
179 93 166 91 178 syl3anc
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p <_ ( p ^ k ) /\ ( p ^ k ) <_ A ) -> p <_ A ) )
180 177 179 mpand
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A -> p <_ A ) )
181 180 pm4.71rd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p ^ k ) <_ A <-> ( p <_ A /\ ( p ^ k ) <_ A ) ) )
182 165 173 181 3bitr2rd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p <_ A /\ ( p ^ k ) <_ A ) <-> ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) ) )
183 130 182 bitrd
 |-  ( ( A e. RR /\ ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) ) )
184 183 ex
 |-  ( A e. RR -> ( ( ( p e. Prime /\ k e. NN ) /\ 0 < A ) -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) ) ) )
185 80 86 184 pm5.21ndd
 |-  ( A e. RR -> ( ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) <-> ( k e. ( 1 ... ( |_ ` A ) ) /\ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ) ) )
186 8 adantrr
 |-  ( ( A e. RR /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( log ` p ) e. CC )
187 64 65 1 185 186 fsumcom2
 |-  ( A e. RR -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) = sum_ k e. ( 1 ... ( |_ ` A ) ) sum_ p e. ( ( 0 [,] ( A ^c ( 1 / k ) ) ) i^i Prime ) ( log ` p ) )
188 63 187 eqtr4d
 |-  ( A e. RR -> sum_ k e. ( 1 ... ( |_ ` A ) ) ( theta ` ( A ^c ( 1 / k ) ) ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( log ` p ) )
189 39 40 188 3eqtr4d
 |-  ( A e. RR -> ( psi ` A ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( theta ` ( A ^c ( 1 / k ) ) ) )