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

Theorem selbergr 22706
Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.)
Hypothesis
Ref Expression
pntrval.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
Assertion
Ref Expression
selbergr  |-  ( x  e.  RR+  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) )  /  x ) )  e.  O(1)
Distinct variable groups:    a, d, x    R, d, x
Allowed substitution hint:    R( a)

Proof of Theorem selbergr
StepHypRef Expression
1 reex 9365 . . . . . . 7  |-  RR  e.  _V
2 rpssre 10993 . . . . . . 7  |-  RR+  C_  RR
31, 2ssexi 4429 . . . . . 6  |-  RR+  e.  _V
43a1i 11 . . . . 5  |-  ( T. 
->  RR+  e.  _V )
5 ovex 6109 . . . . . 6  |-  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  e.  _V
65a1i 11 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  e.  _V )
7 ovex 6109 . . . . . 6  |-  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) )  e.  _V
87a1i 11 . . . . 5  |-  ( ( T.  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) )  e.  _V )
9 eqidd 2438 . . . . 5  |-  ( T. 
->  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) )  =  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) ) )
10 eqidd 2438 . . . . 5  |-  ( T. 
->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) )  =  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )
114, 6, 8, 9, 10offval2 6329 . . . 4  |-  ( T. 
->  ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  oF  -  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )  =  ( x  e.  RR+  |->  ( ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) ) ) )
1211trud 1373 . . 3  |-  ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  oF  -  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )  =  ( x  e.  RR+  |->  ( ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) ) )
13 pntrval.r . . . . . . . . . . . 12  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
1413pntrf 22701 . . . . . . . . . . 11  |-  R : RR+
--> RR
1514ffvelrni 5834 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  RR )
1615recnd 9404 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( R `
 x )  e.  CC )
17 relogcl 21916 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
1817recnd 9404 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
1916, 18mulcld 9398 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( ( R `  x )  x.  ( log `  x
) )  e.  CC )
20 fzfid 11783 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
21 elfznn 11469 . . . . . . . . . . . . 13  |-  ( d  e.  ( 1 ... ( |_ `  x
) )  ->  d  e.  NN )
2221adantl 463 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  NN )
23 vmacl 22345 . . . . . . . . . . . 12  |-  ( d  e.  NN  ->  (Λ `  d )  e.  RR )
2422, 23syl 16 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  d
)  e.  RR )
2524recnd 9404 . . . . . . . . . 10  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  d
)  e.  CC )
26 rpre 10989 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  x  e.  RR )
27 nndivre 10349 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  d  e.  NN )  ->  ( x  /  d
)  e.  RR )
2826, 21, 27syl2an 474 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  d )  e.  RR )
29 chpcl 22351 . . . . . . . . . . . 12  |-  ( ( x  /  d )  e.  RR  ->  (ψ `  ( x  /  d
) )  e.  RR )
3028, 29syl 16 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  d ) )  e.  RR )
3130recnd 9404 . . . . . . . . . 10  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  d ) )  e.  CC )
3225, 31mulcld 9398 . . . . . . . . 9  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  x.  (ψ `  ( x  /  d
) ) )  e.  CC )
3320, 32fsumcl 13198 . . . . . . . 8  |-  ( x  e.  RR+  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  e.  CC )
3419, 33addcld 9397 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( ( R `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  e.  CC )
35 rpcn 10991 . . . . . . 7  |-  ( x  e.  RR+  ->  x  e.  CC )
36 rpne0 10998 . . . . . . 7  |-  ( x  e.  RR+  ->  x  =/=  0 )
3734, 35, 36divcld 10099 . . . . . 6  |-  ( x  e.  RR+  ->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  e.  CC )
3824, 22nndivred 10362 . . . . . . . 8  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  /  d
)  e.  RR )
3938recnd 9404 . . . . . . 7  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  /  d
)  e.  CC )
4020, 39fsumcl 13198 . . . . . 6  |-  ( x  e.  RR+  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  e.  CC )
4137, 40, 18nnncan2d 9746 . . . . 5  |-  ( x  e.  RR+  ->  ( ( ( ( ( ( R `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( log `  x ) )  -  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) )  =  ( ( ( ( ( R `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d ) ) )
42 chpcl 22351 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
4326, 42syl 16 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  (ψ `  x )  e.  RR )
4443recnd 9404 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  (ψ `  x )  e.  CC )
4544, 18mulcld 9398 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( (ψ `  x )  x.  ( log `  x ) )  e.  CC )
4645, 33addcld 9397 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  e.  CC )
4746, 35, 36divcld 10099 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  e.  CC )
4847, 18, 18subsub4d 9742 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( log `  x ) )  -  ( log `  x ) )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( ( log `  x )  +  ( log `  x
) ) ) )
4913pntrval 22700 . . . . . . . . . . . . . 14  |-  ( x  e.  RR+  ->  ( R `
 x )  =  ( (ψ `  x
)  -  x ) )
5049oveq1d 6099 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  ( ( R `  x )  x.  ( log `  x
) )  =  ( ( (ψ `  x
)  -  x )  x.  ( log `  x
) ) )
5144, 35, 18subdird 9793 . . . . . . . . . . . . 13  |-  ( x  e.  RR+  ->  ( ( (ψ `  x )  -  x )  x.  ( log `  x ) )  =  ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( x  x.  ( log `  x
) ) ) )
5250, 51eqtrd 2469 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  ( ( R `  x )  x.  ( log `  x
) )  =  ( ( (ψ `  x
)  x.  ( log `  x ) )  -  ( x  x.  ( log `  x ) ) ) )
5352oveq1d 6099 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( ( ( R `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  =  ( ( ( (ψ `  x )  x.  ( log `  x
) )  -  (
x  x.  ( log `  x ) ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) ) )
5435, 18mulcld 9398 . . . . . . . . . . . 12  |-  ( x  e.  RR+  ->  ( x  x.  ( log `  x
) )  e.  CC )
5545, 33, 54addsubd 9732 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  -  ( x  x.  ( log `  x
) ) )  =  ( ( ( (ψ `  x )  x.  ( log `  x ) )  -  ( x  x.  ( log `  x
) ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) ) )
5653, 55eqtr4d 2472 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( ( ( R `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  =  ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  -  (
x  x.  ( log `  x ) ) ) )
5756oveq1d 6099 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  -  (
x  x.  ( log `  x ) ) )  /  x ) )
58 rpcnne0 11000 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
59 divsubdir 10019 . . . . . . . . . 10  |-  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  e.  CC  /\  (
x  x.  ( log `  x ) )  e.  CC  /\  ( x  e.  CC  /\  x  =/=  0 ) )  -> 
( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  -  (
x  x.  ( log `  x ) ) )  /  x )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( ( x  x.  ( log `  x ) )  /  x ) ) )
6046, 54, 58, 59syl3anc 1213 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  -  ( x  x.  ( log `  x
) ) )  /  x )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( ( x  x.  ( log `  x
) )  /  x
) ) )
6118, 35, 36divcan3d 10104 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( ( x  x.  ( log `  x ) )  /  x )  =  ( log `  x ) )
6261oveq2d 6100 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( ( x  x.  ( log `  x
) )  /  x
) )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( log `  x ) ) )
6357, 60, 623eqtrd 2473 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( log `  x ) ) )
6463oveq1d 6099 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( log `  x ) )  =  ( ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( log `  x ) )  -  ( log `  x ) ) )
65182timesd 10559 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( 2  x.  ( log `  x
) )  =  ( ( log `  x
)  +  ( log `  x ) ) )
6665oveq2d 6100 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( ( log `  x
)  +  ( log `  x ) ) ) )
6748, 64, 663eqtr4d 2479 . . . . . 6  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( log `  x ) )  =  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) )
6867oveq1d 6099 . . . . 5  |-  ( x  e.  RR+  ->  ( ( ( ( ( ( R `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( log `  x ) )  -  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) )  =  ( ( ( ( ( (ψ `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) ) )
6935, 40mulcld 9398 . . . . . . 7  |-  ( x  e.  RR+  ->  ( x  x.  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) )  e.  CC )
70 divsubdir 10019 . . . . . . 7  |-  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  e.  CC  /\  ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d ) )  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  -  ( x  x. 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) ) )  /  x
)  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) )  /  x ) ) )
7134, 69, 58, 70syl3anc 1213 . . . . . 6  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  -  (
x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) ) )  /  x
)  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) )  /  x ) ) )
7219, 33, 69addsubassd 9731 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  -  ( x  x. 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) ) )  =  ( ( ( R `  x )  x.  ( log `  x ) )  +  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) ) ) ) )
7335adantr 462 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
7473, 39mulcld 9398 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( (Λ `  d
)  /  d ) )  e.  CC )
7520, 32, 74fsumsub 13242 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  ( x  x.  (
(Λ `  d )  / 
d ) ) )  =  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( x  x.  ( (Λ `  d )  /  d
) ) ) )
7628recnd 9404 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  d )  e.  CC )
7725, 31, 76subdid 9792 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  x.  (
(ψ `  ( x  /  d ) )  -  ( x  / 
d ) ) )  =  ( ( (Λ `  d )  x.  (ψ `  ( x  /  d
) ) )  -  ( (Λ `  d )  x.  ( x  /  d
) ) ) )
7821nnrpd 11018 . . . . . . . . . . . . . . 15  |-  ( d  e.  ( 1 ... ( |_ `  x
) )  ->  d  e.  RR+ )
79 rpdivcl 11005 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR+  /\  d  e.  RR+ )  ->  (
x  /  d )  e.  RR+ )
8078, 79sylan2 471 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  d )  e.  RR+ )
8113pntrval 22700 . . . . . . . . . . . . . 14  |-  ( ( x  /  d )  e.  RR+  ->  ( R `
 ( x  / 
d ) )  =  ( (ψ `  (
x  /  d ) )  -  ( x  /  d ) ) )
8280, 81syl 16 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  d
) )  =  ( (ψ `  ( x  /  d ) )  -  ( x  / 
d ) ) )
8382oveq2d 6100 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  x.  ( R `  ( x  /  d ) ) )  =  ( (Λ `  d )  x.  (
(ψ `  ( x  /  d ) )  -  ( x  / 
d ) ) ) )
8422nnrpd 11018 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  RR+ )
85 rpcnne0 11000 . . . . . . . . . . . . . . 15  |-  ( d  e.  RR+  ->  ( d  e.  CC  /\  d  =/=  0 ) )
8684, 85syl 16 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( d  e.  CC  /\  d  =/=  0 ) )
87 div12 10008 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  (Λ `  d )  e.  CC  /\  ( d  e.  CC  /\  d  =/=  0 ) )  -> 
( x  x.  (
(Λ `  d )  / 
d ) )  =  ( (Λ `  d
)  x.  ( x  /  d ) ) )
8873, 25, 86, 87syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  x.  ( (Λ `  d
)  /  d ) )  =  ( (Λ `  d )  x.  (
x  /  d ) ) )
8988oveq2d 6100 . . . . . . . . . . . 12  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  d )  x.  (ψ `  ( x  /  d ) ) )  -  ( x  x.  ( (Λ `  d
)  /  d ) ) )  =  ( ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  ( (Λ `  d )  x.  ( x  /  d
) ) ) )
9077, 83, 893eqtr4d 2479 . . . . . . . . . . 11  |-  ( ( x  e.  RR+  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  d )  x.  ( R `  ( x  /  d ) ) )  =  ( ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) )  -  ( x  x.  ( (Λ `  d
)  /  d ) ) ) )
9190sumeq2dv 13168 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  ( x  x.  (
(Λ `  d )  / 
d ) ) ) )
9220, 35, 39fsummulc2 13238 . . . . . . . . . . 11  |-  ( x  e.  RR+  ->  ( x  x.  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) )  =  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( x  x.  (
(Λ `  d )  / 
d ) ) )
9392oveq2d 6100 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) )  -  ( x  x.  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) ) )  =  (
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( x  x.  ( (Λ `  d )  /  d
) ) ) )
9475, 91, 933eqtr4rd 2480 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) )  -  ( x  x.  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) ) )  =  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  ( R `  (
x  /  d ) ) ) )
9594oveq2d 6100 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( ( ( R `  x
)  x.  ( log `  x ) )  +  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) )  -  ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) ) ) )  =  ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  ( R `  (
x  /  d ) ) ) ) )
9672, 95eqtrd 2469 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  -  ( x  x. 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) ) )  =  ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) ) )
9796oveq1d 6099 . . . . . 6  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  -  (
x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) ) )  /  x
)  =  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) )  /  x ) )
9840, 35, 36divcan3d 10104 . . . . . . 7  |-  ( x  e.  RR+  ->  ( ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) )  /  x )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  /  d ) )
9998oveq2d 6100 . . . . . 6  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( ( x  x.  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) )  /  x ) )  =  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) ) )
10071, 97, 993eqtr3rd 2478 . . . . 5  |-  ( x  e.  RR+  ->  ( ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d ) )  =  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) )  /  x ) )
10141, 68, 1003eqtr3d 2477 . . . 4  |-  ( x  e.  RR+  ->  ( ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) )  =  ( ( ( ( R `
 x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  ( R `  (
x  /  d ) ) ) )  /  x ) )
102101mpteq2ia 4366 . . 3  |-  ( x  e.  RR+  |->  ( ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) )  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) ) )  =  ( x  e.  RR+  |->  ( ( ( ( R `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  ( R `  (
x  /  d ) ) ) )  /  x ) )
10312, 102eqtri 2457 . 2  |-  ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  oF  -  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )  =  ( x  e.  RR+  |->  ( ( ( ( R `  x
)  x.  ( log `  x ) )  + 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) )  /  x ) )
104 selberg2 22689 . . 3  |-  ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  e.  O(1)
105 vmadivsum 22620 . . 3  |-  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) )  e.  O(1)
106 o1sub 13081 . . 3  |-  ( ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x
) )  +  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  x.  (ψ `  ( x  /  d ) ) ) )  /  x
)  -  ( 2  x.  ( log `  x
) ) ) )  e.  O(1)  /\  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d )  /  d )  -  ( log `  x ) ) )  e.  O(1) )  ->  ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  oF  -  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )  e.  O(1) )
107104, 105, 106mp2an 667 . 2  |-  ( ( x  e.  RR+  |->  ( ( ( ( (ψ `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  (ψ `  ( x  /  d
) ) ) )  /  x )  -  ( 2  x.  ( log `  x ) ) ) )  oF  -  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  d
)  /  d )  -  ( log `  x
) ) ) )  e.  O(1)
108103, 107eqeltrri 2508 1  |-  ( x  e.  RR+  |->  ( ( ( ( R `  x )  x.  ( log `  x ) )  +  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  d
)  x.  ( R `
 ( x  / 
d ) ) ) )  /  x ) )  e.  O(1)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1364   T. wtru 1365    e. wcel 1757    =/= wne 2600   _Vcvv 2966    e. cmpt 4342   ` cfv 5410  (class class class)co 6084    oFcof 6311   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    - cmin 9587    / cdiv 9985   NNcn 10314   2c2 10363   RR+crp 10983   ...cfz 11428   |_cfl 11628   O(1)co1 12952   sum_csu 13151   logclog 21895  Λcvma 22318  ψcchp 22319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-tp 3874  df-op 3876  df-uni 4084  df-int 4121  df-iun 4165  df-iin 4166  df-disj 4255  df-br 4285  df-opab 4343  df-mpt 4344  df-tr 4378  df-eprel 4623  df-id 4627  df-po 4632  df-so 4633  df-fr 4670  df-se 4671  df-we 4672  df-ord 4713  df-on 4714  df-lim 4715  df-suc 4716  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-isom 5419  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6313  df-om 6470  df-1st 6570  df-2nd 6571  df-supp 6684  df-recs 6822  df-rdg 6856  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-map 7208  df-pm 7209  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-ioc 11297  df-ico 11298  df-icc 11299  df-fz 11429  df-fzo 11537  df-fl 11630  df-mod 11697  df-seq 11795  df-exp 11854  df-fac 12040  df-bc 12067  df-hash 12092  df-shft 12544  df-cj 12576  df-re 12577  df-im 12578  df-sqr 12712  df-abs 12713  df-limsup 12937  df-clim 12954  df-rlim 12955  df-o1 12956  df-lo1 12957  df-sum 13152  df-ef 13340  df-e 13341  df-sin 13342  df-cos 13343  df-pi 13345  df-dvds 13523  df-gcd 13678  df-prm 13751  df-pc 13891  df-struct 14163  df-ndx 14164  df-slot 14165  df-base 14166  df-sets 14167  df-ress 14168  df-plusg 14238  df-mulr 14239  df-starv 14240  df-sca 14241  df-vsca 14242  df-ip 14243  df-tset 14244  df-ple 14245  df-ds 14247  df-unif 14248  df-hom 14249  df-cco 14250  df-rest 14348  df-topn 14349  df-0g 14367  df-gsum 14368  df-topgen 14369  df-pt 14370  df-prds 14373  df-xrs 14427  df-qtop 14432  df-imas 14433  df-xps 14435  df-mre 14511  df-mrc 14512  df-acs 14514  df-mnd 15402  df-submnd 15452  df-mulg 15532  df-cntz 15819  df-cmn 16263  df-psmet 17657  df-xmet 17658  df-met 17659  df-bl 17660  df-mopn 17661  df-fbas 17662  df-fg 17663  df-cnfld 17667  df-top 18349  df-bases 18351  df-topon 18352  df-topsp 18353  df-cld 18469  df-ntr 18470  df-cls 18471  df-nei 18548  df-lp 18586  df-perf 18587  df-cn 18677  df-cnp 18678  df-haus 18765  df-cmp 18836  df-tx 18981  df-hmeo 19174  df-fil 19265  df-fm 19357  df-flim 19358  df-flf 19359  df-xms 19741  df-ms 19742  df-tms 19743  df-cncf 20300  df-limc 21187  df-dv 21188  df-log 21897  df-cxp 21898  df-em 22275  df-cht 22323  df-vma 22324  df-chp 22325  df-ppi 22326  df-mu 22327
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator