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