MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chpchtsum Structured version   Unicode version

Theorem chpchtsum 23363
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.)
Assertion
Ref Expression
chpchtsum  |-  ( A  e.  RR  ->  (ψ `  A )  =  sum_ k  e.  ( 1 ... ( |_ `  A ) ) (
theta `  ( A  ^c  ( 1  / 
k ) ) ) )
Distinct variable group:    A, k

Proof of Theorem chpchtsum
Dummy variable  p is distinct from all other variables.
StepHypRef Expression
1 fzfid 12059 . . . . 5  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( 1 ... ( |_ `  ( ( log `  A )  /  ( log `  p ) ) ) )  e.  Fin )
2 inss2 3702 . . . . . . . . . 10  |-  ( ( 0 [,] A )  i^i  Prime )  C_  Prime
3 simpr 461 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  ( (
0 [,] A )  i^i  Prime ) )
42, 3sseldi 3485 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  Prime )
5 prmnn 14094 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  NN )
64, 5syl 16 . . . . . . . 8  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  NN )
76nnrpd 11261 . . . . . . 7  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  RR+ )
87relogcld 22877 . . . . . 6  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( log `  p
)  e.  RR )
98recnd 9622 . . . . 5  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( log `  p
)  e.  CC )
10 fsumconst 13581 . . . . 5  |-  ( ( ( 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 ) ) )
111, 9, 10syl2anc 661 . . . 4  |-  ( ( 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 ) ) )
12 simpl 457 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  A  e.  RR )
13 1red 9611 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
1  e.  RR )
146nnred 10554 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  RR )
15 prmuz2 14109 . . . . . . . . . . . . 13  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
164, 15syl 16 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  ( ZZ>= ` 
2 ) )
17 eluz2b2 11160 . . . . . . . . . . . . 13  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
1817simprbi 464 . . . . . . . . . . . 12  |-  ( p  e.  ( ZZ>= `  2
)  ->  1  <  p )
1916, 18syl 16 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
1  <  p )
20 inss1 3701 . . . . . . . . . . . . . 14  |-  ( ( 0 [,] A )  i^i  Prime )  C_  (
0 [,] A )
2120, 3sseldi 3485 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  ( 0 [,] A ) )
22 0re 9596 . . . . . . . . . . . . . 14  |-  0  e.  RR
23 elicc2 11595 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR  /\  A  e.  RR )  ->  ( p  e.  ( 0 [,] A )  <-> 
( p  e.  RR  /\  0  <_  p  /\  p  <_  A ) ) )
2422, 12, 23sylancr 663 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( p  e.  ( 0 [,] A )  <-> 
( p  e.  RR  /\  0  <_  p  /\  p  <_  A ) ) )
2521, 24mpbid 210 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( p  e.  RR  /\  0  <_  p  /\  p  <_  A ) )
2625simp3d 1009 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  <_  A )
2713, 14, 12, 19, 26ltletrd 9742 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
1  <  A )
2812, 27rplogcld 22883 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( log `  A
)  e.  RR+ )
2914, 19rplogcld 22883 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( log `  p
)  e.  RR+ )
3028, 29rpdivcld 11279 . . . . . . . 8  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( ( log `  A
)  /  ( log `  p ) )  e.  RR+ )
3130rpred 11262 . . . . . . 7  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( ( log `  A
)  /  ( log `  p ) )  e.  RR )
3230rpge0d 11266 . . . . . . 7  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
0  <_  ( ( log `  A )  / 
( log `  p
) ) )
33 flge0nn0 11930 . . . . . . 7  |-  ( ( ( ( log `  A
)  /  ( log `  p ) )  e.  RR  /\  0  <_ 
( ( log `  A
)  /  ( log `  p ) ) )  ->  ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) )  e.  NN0 )
3431, 32, 33syl2anc 661 . . . . . 6  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( |_ `  (
( log `  A
)  /  ( log `  p ) ) )  e.  NN0 )
35 hashfz1 12395 . . . . . 6  |-  ( ( |_ `  ( ( log `  A )  /  ( log `  p
) ) )  e. 
NN0  ->  ( # `  (
1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) ) )  =  ( |_ `  ( ( log `  A )  /  ( log `  p
) ) ) )
3634, 35syl 16 . . . . 5  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( # `  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) ) )  =  ( |_ `  ( ( log `  A )  /  ( log `  p
) ) ) )
3736oveq1d 6293 . . . 4  |-  ( ( 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 ) ) )
3831flcld 11911 . . . . . 6  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( |_ `  (
( log `  A
)  /  ( log `  p ) ) )  e.  ZZ )
3938zcnd 10972 . . . . 5  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( |_ `  (
( log `  A
)  /  ( log `  p ) ) )  e.  CC )
4039, 9mulcomd 9617 . . . 4  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
( ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) )  x.  ( log `  p
) )  =  ( ( log `  p
)  x.  ( |_
`  ( ( log `  A )  /  ( log `  p ) ) ) ) )
4111, 37, 403eqtrrd 2487 . . 3  |-  ( ( 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
) )
4241sumeq2dv 13501 . 2  |-  ( 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 ) )
43 chpval2 23362 . 2  |-  ( A  e.  RR  ->  (ψ `  A )  =  sum_ p  e.  ( ( 0 [,] A )  i^i 
Prime ) ( ( log `  p )  x.  ( |_ `  ( ( log `  A )  /  ( log `  p ) ) ) ) )
44 simpl 457 . . . . . 6  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  A  e.  RR )
45 0red 9597 . . . . . . 7  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  0  e.  RR )
46 1red 9611 . . . . . . . 8  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  1  e.  RR )
47 0lt1 10078 . . . . . . . . 9  |-  0  <  1
4847a1i 11 . . . . . . . 8  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  0  <  1
)
49 elfzuz2 11697 . . . . . . . . 9  |-  ( k  e.  ( 1 ... ( |_ `  A
) )  ->  ( |_ `  A )  e.  ( ZZ>= `  1 )
)
50 eluzle 11099 . . . . . . . . . . 11  |-  ( ( |_ `  A )  e.  ( ZZ>= `  1
)  ->  1  <_  ( |_ `  A ) )
5150adantl 466 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( |_ `  A )  e.  ( ZZ>= `  1
) )  ->  1  <_  ( |_ `  A
) )
52 simpl 457 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( |_ `  A )  e.  ( ZZ>= `  1
) )  ->  A  e.  RR )
53 1z 10897 . . . . . . . . . . 11  |-  1  e.  ZZ
54 flge 11918 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  1  e.  ZZ )  ->  ( 1  <_  A  <->  1  <_  ( |_ `  A ) ) )
5552, 53, 54sylancl 662 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( |_ `  A )  e.  ( ZZ>= `  1
) )  ->  (
1  <_  A  <->  1  <_  ( |_ `  A ) ) )
5651, 55mpbird 232 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( |_ `  A )  e.  ( ZZ>= `  1
) )  ->  1  <_  A )
5749, 56sylan2 474 . . . . . . . 8  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  1  <_  A
)
5845, 46, 44, 48, 57ltletrd 9742 . . . . . . 7  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  0  <  A
)
5945, 44, 58ltled 9733 . . . . . 6  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  0  <_  A
)
60 elfznn 11720 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  A
) )  ->  k  e.  NN )
6160adantl 466 . . . . . . 7  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  k  e.  NN )
6261nnrecred 10584 . . . . . 6  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  ( 1  / 
k )  e.  RR )
6344, 59, 62recxpcld 22973 . . . . 5  |-  ( ( A  e.  RR  /\  k  e.  ( 1 ... ( |_ `  A ) ) )  ->  ( A  ^c  ( 1  / 
k ) )  e.  RR )
64 chtval 23253 . . . . 5  |-  ( ( A  ^c  ( 1  /  k ) )  e.  RR  ->  (
theta `  ( A  ^c  ( 1  / 
k ) ) )  =  sum_ p  e.  ( ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )
( log `  p
) )
6563, 64syl 16 . . . 4  |-  ( ( 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
) )
6665sumeq2dv 13501 . . 3  |-  ( 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
) )
67 ppifi 23248 . . . 4  |-  ( A  e.  RR  ->  (
( 0 [,] A
)  i^i  Prime )  e. 
Fin )
68 fzfid 12059 . . . 4  |-  ( A  e.  RR  ->  (
1 ... ( |_ `  A ) )  e. 
Fin )
692sseli 3483 . . . . . . . 8  |-  ( p  e.  ( ( 0 [,] A )  i^i 
Prime )  ->  p  e. 
Prime )
70 elfznn 11720 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  A
)  /  ( log `  p ) ) ) )  ->  k  e.  NN )
7169, 70anim12i 566 . . . . . . 7  |-  ( ( p  e.  ( ( 0 [,] A )  i^i  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  A )  /  ( log `  p ) ) ) ) )  -> 
( p  e.  Prime  /\  k  e.  NN ) )
7271a1i 11 . . . . . 6  |-  ( A  e.  RR  ->  (
( p  e.  ( ( 0 [,] A
)  i^i  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) ) )  ->  (
p  e.  Prime  /\  k  e.  NN ) ) )
73 0red 9597 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
0  e.  RR )
742a1i 11 . . . . . . . . . . . 12  |-  ( A  e.  RR  ->  (
( 0 [,] A
)  i^i  Prime )  C_  Prime )
7574sselda 3487 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  Prime )
7675, 5syl 16 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  NN )
7776nnred 10554 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  ->  p  e.  RR )
7876nngt0d 10582 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
0  <  p )
7973, 77, 12, 78, 26ltletrd 9742 . . . . . . . 8  |-  ( ( A  e.  RR  /\  p  e.  ( (
0 [,] A )  i^i  Prime ) )  -> 
0  <  A )
8079ex 434 . . . . . . 7  |-  ( A  e.  RR  ->  (
p  e.  ( ( 0 [,] A )  i^i  Prime )  ->  0  <  A ) )
8180adantrd 468 . . . . . 6  |-  ( A  e.  RR  ->  (
( p  e.  ( ( 0 [,] A
)  i^i  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) ) )  ->  0  <  A ) )
8272, 81jcad 533 . . . . 5  |-  ( 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
) ) )
83 inss2 3702 . . . . . . . . 9  |-  ( ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )  C_ 
Prime
8483sseli 3483 . . . . . . . 8  |-  ( p  e.  ( ( 0 [,] ( A  ^c  ( 1  / 
k ) ) )  i^i  Prime )  ->  p  e.  Prime )
8560, 84anim12ci 567 . . . . . . 7  |-  ( ( k  e.  ( 1 ... ( |_ `  A ) )  /\  p  e.  ( (
0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )
)  ->  ( p  e.  Prime  /\  k  e.  NN ) )
8685a1i 11 . . . . . 6  |-  ( A  e.  RR  ->  (
( k  e.  ( 1 ... ( |_
`  A ) )  /\  p  e.  ( ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )
)  ->  ( p  e.  Prime  /\  k  e.  NN ) ) )
8758ex 434 . . . . . . 7  |-  ( A  e.  RR  ->  (
k  e.  ( 1 ... ( |_ `  A ) )  -> 
0  <  A )
)
8887adantrd 468 . . . . . 6  |-  ( A  e.  RR  ->  (
( k  e.  ( 1 ... ( |_
`  A ) )  /\  p  e.  ( ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )
)  ->  0  <  A ) )
8986, 88jcad 533 . . . . 5  |-  ( 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 ) ) )
90 elin 3670 . . . . . . . . 9  |-  ( p  e.  ( ( 0 [,] A )  i^i 
Prime )  <->  ( p  e.  ( 0 [,] A
)  /\  p  e.  Prime ) )
91 simprll 761 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  Prime )
9291biantrud 507 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  e.  ( 0 [,] A )  <->  ( p  e.  ( 0 [,] A
)  /\  p  e.  Prime ) ) )
93 0red 9597 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  0  e.  RR )
94 simpl 457 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  A  e.  RR )
9591, 5syl 16 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  NN )
9695nnred 10554 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  RR )
9795nnnn0d 10855 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  NN0 )
9897nn0ge0d 10858 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  0  <_  p )
99 df-3an 974 . . . . . . . . . . . . 13  |-  ( ( p  e.  RR  /\  0  <_  p  /\  p  <_  A )  <->  ( (
p  e.  RR  /\  0  <_  p )  /\  p  <_  A ) )
10023, 99syl6bb 261 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  A  e.  RR )  ->  ( p  e.  ( 0 [,] A )  <-> 
( ( p  e.  RR  /\  0  <_  p )  /\  p  <_  A ) ) )
101100baibd 907 . . . . . . . . . . 11  |-  ( ( ( 0  e.  RR  /\  A  e.  RR )  /\  ( p  e.  RR  /\  0  <_  p ) )  -> 
( p  e.  ( 0 [,] A )  <-> 
p  <_  A )
)
10293, 94, 96, 98, 101syl22anc 1228 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  e.  ( 0 [,] A )  <->  p  <_  A ) )
10392, 102bitr3d 255 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p  e.  ( 0 [,] A )  /\  p  e.  Prime )  <-> 
p  <_  A )
)
10490, 103syl5bb 257 . . . . . . . 8  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  e.  ( ( 0 [,] A )  i^i  Prime )  <->  p  <_  A ) )
105 simprr 756 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  0  <  A )
10694, 105elrpd 11260 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  A  e.  RR+ )
107106relogcld 22877 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( log `  A )  e.  RR )
10891, 15syl 16 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  ( ZZ>= `  2 )
)
109108, 18syl 16 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  1  <  p )
11096, 109rplogcld 22883 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( log `  p )  e.  RR+ )
111107, 110rerpdivcld 11289 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( log `  A
)  /  ( log `  p ) )  e.  RR )
112 simprlr 762 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  NN )
113112nnzd 10970 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  ZZ )
114 flge 11918 . . . . . . . . . 10  |-  ( ( ( ( log `  A
)  /  ( log `  p ) )  e.  RR  /\  k  e.  ZZ )  ->  (
k  <_  ( ( log `  A )  / 
( log `  p
) )  <->  k  <_  ( |_ `  ( ( log `  A )  /  ( log `  p
) ) ) ) )
115111, 113, 114syl2anc 661 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  <_  ( ( log `  A )  / 
( log `  p
) )  <->  k  <_  ( |_ `  ( ( log `  A )  /  ( log `  p
) ) ) ) )
116112nnnn0d 10855 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  NN0 )
11795, 116nnexpcld 12307 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p ^ k )  e.  NN )
118117nnrpd 11261 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p ^ k )  e.  RR+ )
119118, 106logled 22881 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  <->  ( log `  ( p ^ k
) )  <_  ( log `  A ) ) )
12095nnrpd 11261 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  RR+ )
121 relogexp 22849 . . . . . . . . . . . 12  |-  ( ( p  e.  RR+  /\  k  e.  ZZ )  ->  ( log `  ( p ^
k ) )  =  ( k  x.  ( log `  p ) ) )
122120, 113, 121syl2anc 661 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( log `  ( p ^
k ) )  =  ( k  x.  ( log `  p ) ) )
123122breq1d 4444 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( log `  (
p ^ k ) )  <_  ( log `  A )  <->  ( k  x.  ( log `  p
) )  <_  ( log `  A ) ) )
124112nnred 10554 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  RR )
125124, 107, 110lemuldivd 11307 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( k  x.  ( log `  p ) )  <_  ( log `  A
)  <->  k  <_  (
( log `  A
)  /  ( log `  p ) ) ) )
126119, 123, 1253bitrd 279 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  <->  k  <_  ( ( log `  A
)  /  ( log `  p ) ) ) )
127 nnuz 11122 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
128112, 127syl6eleq 2539 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  ( ZZ>= `  1 )
)
129111flcld 11911 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( |_ `  ( ( log `  A )  /  ( log `  p ) ) )  e.  ZZ )
130 elfz5 11686 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= ` 
1 )  /\  ( |_ `  ( ( log `  A )  /  ( log `  p ) ) )  e.  ZZ )  ->  ( k  e.  ( 1 ... ( |_ `  ( ( log `  A )  /  ( log `  p ) ) ) )  <->  k  <_  ( |_ `  ( ( log `  A )  /  ( log `  p
) ) ) ) )
131128, 129, 130syl2anc 661 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  e.  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) )  <->  k  <_  ( |_ `  ( ( log `  A )  /  ( log `  p ) ) ) ) )
132115, 126, 1313bitr4rd 286 . . . . . . . 8  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  e.  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) )  <->  ( p ^
k )  <_  A
) )
133104, 132anbi12d 710 . . . . . . 7  |-  ( ( 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 ) ) )
13494flcld 11911 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( |_ `  A )  e.  ZZ )
135 elfz5 11686 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= ` 
1 )  /\  ( |_ `  A )  e.  ZZ )  ->  (
k  e.  ( 1 ... ( |_ `  A ) )  <->  k  <_  ( |_ `  A ) ) )
136128, 134, 135syl2anc 661 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  e.  ( 1 ... ( |_ `  A ) )  <->  k  <_  ( |_ `  A ) ) )
137 flge 11918 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  k  e.  ZZ )  ->  ( k  <_  A  <->  k  <_  ( |_ `  A ) ) )
13894, 113, 137syl2anc 661 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  <_  A  <->  k  <_  ( |_ `  A ) ) )
139136, 138bitr4d 256 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
k  e.  ( 1 ... ( |_ `  A ) )  <->  k  <_  A ) )
140 elin 3670 . . . . . . . . . 10  |-  ( p  e.  ( ( 0 [,] ( A  ^c  ( 1  / 
k ) ) )  i^i  Prime )  <->  ( p  e.  ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  /\  p  e. 
Prime ) )
14191biantrud 507 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
142106rpge0d 11266 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  0  <_  A )
143112nnrecred 10584 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
1  /  k )  e.  RR )
14494, 142, 143recxpcld 22973 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( A  ^c  ( 1  /  k ) )  e.  RR )
145 elicc2 11595 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) ) )
146 df-3an 974 . . . . . . . . . . . . . . 15  |-  ( ( p  e.  RR  /\  0  <_  p  /\  p  <_  ( A  ^c 
( 1  /  k
) ) )  <->  ( (
p  e.  RR  /\  0  <_  p )  /\  p  <_  ( A  ^c  ( 1  / 
k ) ) ) )
147145, 146syl6bb 261 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) ) ) )
148147baibd 907 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) )
14993, 144, 96, 98, 148syl22anc 1228 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  e.  ( 0 [,] ( A  ^c  ( 1  / 
k ) ) )  <-> 
p  <_  ( A  ^c  ( 1  /  k ) ) ) )
150141, 149bitr3d 255 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
15194, 142, 143cxpge0d 22974 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  0  <_  ( A  ^c 
( 1  /  k
) ) )
152112nnrpd 11261 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  RR+ )
15396, 98, 144, 151, 152cxple2d 22977 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
15495nncnd 10555 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  e.  CC )
155 cxpexp 22918 . . . . . . . . . . . . 13  |-  ( ( p  e.  CC  /\  k  e.  NN0 )  -> 
( p  ^c 
k )  =  ( p ^ k ) )
156154, 116, 155syl2anc 661 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  ^c  k )  =  ( p ^ k ) )
157112nncnd 10555 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  e.  CC )
158112nnne0d 10583 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  =/=  0 )
159157, 158recid2d 10319 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( 1  /  k
)  x.  k )  =  1 )
160159oveq2d 6294 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( A  ^c  ( ( 1  /  k )  x.  k ) )  =  ( A  ^c  1 ) )
161106, 143, 157cxpmuld 22984 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( A  ^c  ( ( 1  /  k )  x.  k ) )  =  ( ( A  ^c  ( 1  /  k ) )  ^c  k ) )
16294recnd 9622 . . . . . . . . . . . . . 14  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  A  e.  CC )
163162cxp1d 22956 . . . . . . . . . . . . 13  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  ( A  ^c  1 )  =  A )
164160, 161, 1633eqtr3d 2490 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( A  ^c 
( 1  /  k
) )  ^c 
k )  =  A )
165156, 164breq12d 4447 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p  ^c 
k )  <_  (
( A  ^c 
( 1  /  k
) )  ^c 
k )  <->  ( p ^ k )  <_  A ) )
166150, 153, 1653bitrd 279 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p  e.  ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  /\  p  e. 
Prime )  <->  ( p ^
k )  <_  A
) )
167140, 166syl5bb 257 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p  e.  ( ( 0 [,] ( A  ^c  ( 1  /  k ) ) )  i^i  Prime )  <->  ( p ^ k )  <_  A ) )
168139, 167anbi12d 710 . . . . . . . 8  |-  ( ( 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
) ) )
169117nnred 10554 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p ^ k )  e.  RR )
170 bernneq3 12270 . . . . . . . . . . . 12  |-  ( ( p  e.  ( ZZ>= ` 
2 )  /\  k  e.  NN0 )  ->  k  <  ( p ^ k
) )
171108, 116, 170syl2anc 661 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  <  ( p ^ k
) )
172124, 169, 171ltled 9733 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  k  <_  ( p ^ k
) )
173 letr 9678 . . . . . . . . . . 11  |-  ( ( k  e.  RR  /\  ( p ^ k
)  e.  RR  /\  A  e.  RR )  ->  ( ( k  <_ 
( p ^ k
)  /\  ( p ^ k )  <_  A )  ->  k  <_  A ) )
174124, 169, 94, 173syl3anc 1227 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( k  <_  (
p ^ k )  /\  ( p ^
k )  <_  A
)  ->  k  <_  A ) )
175172, 174mpand 675 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  ->  k  <_  A ) )
176175pm4.71rd 635 . . . . . . . 8  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  <->  ( k  <_  A  /\  ( p ^ k )  <_  A ) ) )
177154exp1d 12281 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p ^ 1 )  =  p )
17895nnge1d 10581 . . . . . . . . . . . 12  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  1  <_  p )
17996, 178, 128leexp2ad 12318 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
p ^ 1 )  <_  ( p ^
k ) )
180177, 179eqbrtrrd 4456 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  p  <_  ( p ^ k
) )
181 letr 9678 . . . . . . . . . . 11  |-  ( ( p  e.  RR  /\  ( p ^ k
)  e.  RR  /\  A  e.  RR )  ->  ( ( p  <_ 
( p ^ k
)  /\  ( p ^ k )  <_  A )  ->  p  <_  A ) )
18296, 169, 94, 181syl3anc 1227 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p  <_  (
p ^ k )  /\  ( p ^
k )  <_  A
)  ->  p  <_  A ) )
183180, 182mpand 675 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  ->  p  <_  A ) )
184183pm4.71rd 635 . . . . . . . 8  |-  ( ( A  e.  RR  /\  ( ( p  e. 
Prime  /\  k  e.  NN )  /\  0  <  A
) )  ->  (
( p ^ k
)  <_  A  <->  ( p  <_  A  /\  ( p ^ k )  <_  A ) ) )
185168, 176, 1843bitr2rd 282 . . . . . . 7  |-  ( ( 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 )
) ) )
186133, 185bitrd 253 . . . . . 6  |-  ( ( 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 )
) ) )
187186ex 434 . . . . 5  |-  ( 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 )
) ) ) )
18882, 89, 187pm5.21ndd 354 . . . 4  |-  ( 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 )
) ) )
1899adantrr 716 . . . 4  |-  ( ( A  e.  RR  /\  ( p  e.  (
( 0 [,] A
)  i^i  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  A
)  /  ( log `  p ) ) ) ) ) )  -> 
( log `  p
)  e.  CC )
19067, 68, 1, 188, 189fsumcom2 13565 . . 3  |-  ( 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 ) )
19166, 190eqtr4d 2485 . 2  |-  ( 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 ) )
19242, 43, 1913eqtr4d 2492 1  |-  ( A  e.  RR  ->  (ψ `  A )  =  sum_ k  e.  ( 1 ... ( |_ `  A ) ) (
theta `  ( A  ^c  ( 1  / 
k ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 972    = wceq 1381    e. wcel 1802    i^i cin 3458    C_ wss 3459   class class class wbr 4434   ` cfv 5575  (class class class)co 6278   Fincfn 7515   CCcc 9490   RRcr 9491   0cc0 9492   1c1 9493    x. cmul 9497    < clt 9628    <_ cle 9629    / cdiv 10209   NNcn 10539   2c2 10588   NN0cn0 10798   ZZcz 10867   ZZ>=cuz 11087   RR+crp 11226   [,]cicc 11538   ...cfz 11678   |_cfl 11903   ^cexp 12142   #chash 12381   sum_csu 13484   Primecprime 14091   logclog 22811    ^c ccxp 22812   thetaccht 23233  ψcchp 23235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4545  ax-sep 4555  ax-nul 4563  ax-pow 4612  ax-pr 4673  ax-un 6574  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570  ax-addf 9571  ax-mulf 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3419  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-pss 3475  df-nul 3769  df-if 3924  df-pw 3996  df-sn 4012  df-pr 4014  df-tp 4016  df-op 4018  df-uni 4232  df-int 4269  df-iun 4314  df-iin 4315  df-br 4435  df-opab 4493  df-mpt 4494  df-tr 4528  df-eprel 4778  df-id 4782  df-po 4787  df-so 4788  df-fr 4825  df-se 4826  df-we 4827  df-ord 4868  df-on 4869  df-lim 4870  df-suc 4871  df-xp 4992  df-rel 4993  df-cnv 4994  df-co 4995  df-dm 4996  df-rn 4997  df-res 4998  df-ima 4999  df-iota 5538  df-fun 5577  df-fn 5578  df-f 5579  df-f1 5580  df-fo 5581  df-f1o 5582  df-fv 5583  df-isom 5584  df-riota 6239  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-of 6522  df-om 6683  df-1st 6782  df-2nd 6783  df-supp 6901  df-recs 7041  df-rdg 7075  df-1o 7129  df-2o 7130  df-oadd 7133  df-er 7310  df-map 7421  df-pm 7422  df-ixp 7469  df-en 7516  df-dom 7517  df-sdom 7518  df-fin 7519  df-fsupp 7829  df-fi 7870  df-sup 7900  df-oi 7935  df-card 8320  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9809  df-neg 9810  df-div 10210  df-nn 10540  df-2 10597  df-3 10598  df-4 10599  df-5 10600  df-6 10601  df-7 10602  df-8 10603  df-9 10604  df-10 10605  df-n0 10799  df-z 10868  df-dec 10982  df-uz 11088  df-q 11189  df-rp 11227  df-xneg 11324  df-xadd 11325  df-xmul 11326  df-ioo 11539  df-ioc 11540  df-ico 11541  df-icc 11542  df-fz 11679  df-fzo 11801  df-fl 11905  df-mod 11973  df-seq 12084  df-exp 12143  df-fac 12330  df-bc 12357  df-hash 12382  df-shft 12876  df-cj 12908  df-re 12909  df-im 12910  df-sqrt 13044  df-abs 13045  df-limsup 13270  df-clim 13287  df-rlim 13288  df-sum 13485  df-ef 13678  df-sin 13680  df-cos 13681  df-pi 13683  df-dvds 13861  df-gcd 14019  df-prm 14092  df-pc 14235  df-struct 14508  df-ndx 14509  df-slot 14510  df-base 14511  df-sets 14512  df-ress 14513  df-plusg 14584  df-mulr 14585  df-starv 14586  df-sca 14587  df-vsca 14588  df-ip 14589  df-tset 14590  df-ple 14591  df-ds 14593  df-unif 14594  df-hom 14595  df-cco 14596  df-rest 14694  df-topn 14695  df-0g 14713  df-gsum 14714  df-topgen 14715  df-pt 14716  df-prds 14719  df-xrs 14773  df-qtop 14778  df-imas 14779  df-xps 14781  df-mre 14857  df-mrc 14858  df-acs 14860  df-mgm 15743  df-sgrp 15782  df-mnd 15792  df-submnd 15838  df-mulg 15931  df-cntz 16226  df-cmn 16671  df-psmet 18282  df-xmet 18283  df-met 18284  df-bl 18285  df-mopn 18286  df-fbas 18287  df-fg 18288  df-cnfld 18292  df-top 19269  df-bases 19271  df-topon 19272  df-topsp 19273  df-cld 19390  df-ntr 19391  df-cls 19392  df-nei 19469  df-lp 19507  df-perf 19508  df-cn 19598  df-cnp 19599  df-haus 19686  df-tx 19933  df-hmeo 20126  df-fil 20217  df-fm 20309  df-flim 20310  df-flf 20311  df-xms 20693  df-ms 20694  df-tms 20695  df-cncf 21252  df-limc 22140  df-dv 22141  df-log 22813  df-cxp 22814  df-cht 23239  df-vma 23240  df-chp 23241
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator