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 bitrid 
 |-  ( ( 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 bitrid 
 |-  ( ( 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 ) ) ) )