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

Theorem dvfsum2 21642
Description: The reverse of dvfsumrlim 21639, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.)
Hypotheses
Ref Expression
dvfsum2.s  |-  S  =  ( T (,) +oo )
dvfsum2.z  |-  Z  =  ( ZZ>= `  M )
dvfsum2.m  |-  ( ph  ->  M  e.  ZZ )
dvfsum2.d  |-  ( ph  ->  D  e.  RR )
dvfsum2.u  |-  ( ph  ->  U  e.  RR* )
dvfsum2.md  |-  ( ph  ->  M  <_  ( D  +  1 ) )
dvfsum2.t  |-  ( ph  ->  T  e.  RR )
dvfsum2.a  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  RR )
dvfsum2.b1  |-  ( (
ph  /\  x  e.  S )  ->  B  e.  V )
dvfsum2.b2  |-  ( (
ph  /\  x  e.  Z )  ->  B  e.  RR )
dvfsum2.b3  |-  ( ph  ->  ( RR  _D  (
x  e.  S  |->  A ) )  =  ( x  e.  S  |->  B ) )
dvfsum2.c  |-  ( x  =  k  ->  B  =  C )
dvfsum2.l  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  B  <_  C )
dvfsum2.g  |-  G  =  ( x  e.  S  |->  ( sum_ k  e.  ( M ... ( |_
`  x ) ) C  -  A ) )
dvfsum2.0  |-  ( (
ph  /\  ( x  e.  S  /\  D  <_  x ) )  -> 
0  <_  B )
dvfsum2.1  |-  ( ph  ->  X  e.  S )
dvfsum2.2  |-  ( ph  ->  Y  e.  S )
dvfsum2.3  |-  ( ph  ->  D  <_  X )
dvfsum2.4  |-  ( ph  ->  X  <_  Y )
dvfsum2.5  |-  ( ph  ->  Y  <_  U )
dvfsum2.e  |-  ( x  =  Y  ->  B  =  E )
Assertion
Ref Expression
dvfsum2  |-  ( ph  ->  ( abs `  (
( G `  Y
)  -  ( G `
 X ) ) )  <_  E )
Distinct variable groups:    B, k    x, C    x, k, D    ph, k, x    x, E   
k, M, x    S, k, x    k, X, x   
k, Y, x    x, T    U, k, x    x, V    x, Z
Allowed substitution hints:    A( x, k)    B( x)    C( k)    T( k)    E( k)    G( x, k)    V( k)    Z( k)

Proof of Theorem dvfsum2
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 dvfsum2.2 . . . . . 6  |-  ( ph  ->  Y  e.  S )
2 fzfid 11915 . . . . . . . 8  |-  ( ph  ->  ( M ... ( |_ `  Y ) )  e.  Fin )
3 dvfsum2.b2 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  Z )  ->  B  e.  RR )
43ralrimiva 2830 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  Z  B  e.  RR )
5 elfzuz 11569 . . . . . . . . . 10  |-  ( k  e.  ( M ... ( |_ `  Y ) )  ->  k  e.  ( ZZ>= `  M )
)
6 dvfsum2.z . . . . . . . . . 10  |-  Z  =  ( ZZ>= `  M )
75, 6syl6eleqr 2553 . . . . . . . . 9  |-  ( k  e.  ( M ... ( |_ `  Y ) )  ->  k  e.  Z )
8 dvfsum2.c . . . . . . . . . . 11  |-  ( x  =  k  ->  B  =  C )
98eleq1d 2523 . . . . . . . . . 10  |-  ( x  =  k  ->  ( B  e.  RR  <->  C  e.  RR ) )
109rspccva 3178 . . . . . . . . 9  |-  ( ( A. x  e.  Z  B  e.  RR  /\  k  e.  Z )  ->  C  e.  RR )
114, 7, 10syl2an 477 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M ... ( |_
`  Y ) ) )  ->  C  e.  RR )
122, 11fsumrecl 13332 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  e.  RR )
13 dvfsum2.a . . . . . . . . 9  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  RR )
1413ralrimiva 2830 . . . . . . . 8  |-  ( ph  ->  A. x  e.  S  A  e.  RR )
15 nfcsb1v 3414 . . . . . . . . . 10  |-  F/_ x [_ Y  /  x ]_ A
1615nfel1 2632 . . . . . . . . 9  |-  F/ x [_ Y  /  x ]_ A  e.  RR
17 csbeq1a 3407 . . . . . . . . . 10  |-  ( x  =  Y  ->  A  =  [_ Y  /  x ]_ A )
1817eleq1d 2523 . . . . . . . . 9  |-  ( x  =  Y  ->  ( A  e.  RR  <->  [_ Y  /  x ]_ A  e.  RR ) )
1916, 18rspc 3173 . . . . . . . 8  |-  ( Y  e.  S  ->  ( A. x  e.  S  A  e.  RR  ->  [_ Y  /  x ]_ A  e.  RR )
)
201, 14, 19sylc 60 . . . . . . 7  |-  ( ph  ->  [_ Y  /  x ]_ A  e.  RR )
2112, 20resubcld 9890 . . . . . 6  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  e.  RR )
22 nfcv 2616 . . . . . . 7  |-  F/_ x Y
23 nfcv 2616 . . . . . . . 8  |-  F/_ x sum_ k  e.  ( M ... ( |_ `  Y ) ) C
24 nfcv 2616 . . . . . . . 8  |-  F/_ x  -
2523, 24, 15nfov 6226 . . . . . . 7  |-  F/_ x
( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )
26 fveq2 5802 . . . . . . . . . 10  |-  ( x  =  Y  ->  ( |_ `  x )  =  ( |_ `  Y
) )
2726oveq2d 6219 . . . . . . . . 9  |-  ( x  =  Y  ->  ( M ... ( |_ `  x ) )  =  ( M ... ( |_ `  Y ) ) )
2827sumeq1d 13299 . . . . . . . 8  |-  ( x  =  Y  ->  sum_ k  e.  ( M ... ( |_ `  x ) ) C  =  sum_ k  e.  ( M ... ( |_ `  Y ) ) C )
2928, 17oveq12d 6221 . . . . . . 7  |-  ( x  =  Y  ->  ( sum_ k  e.  ( M ... ( |_ `  x ) ) C  -  A )  =  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )
30 dvfsum2.g . . . . . . 7  |-  G  =  ( x  e.  S  |->  ( sum_ k  e.  ( M ... ( |_
`  x ) ) C  -  A ) )
3122, 25, 29, 30fvmptf 5902 . . . . . 6  |-  ( ( Y  e.  S  /\  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  e.  RR )  -> 
( G `  Y
)  =  ( sum_ k  e.  ( M ... ( |_ `  Y
) ) C  -  [_ Y  /  x ]_ A ) )
321, 21, 31syl2anc 661 . . . . 5  |-  ( ph  ->  ( G `  Y
)  =  ( sum_ k  e.  ( M ... ( |_ `  Y
) ) C  -  [_ Y  /  x ]_ A ) )
33 dvfsum2.1 . . . . . 6  |-  ( ph  ->  X  e.  S )
34 fzfid 11915 . . . . . . . 8  |-  ( ph  ->  ( M ... ( |_ `  X ) )  e.  Fin )
35 elfzuz 11569 . . . . . . . . . 10  |-  ( k  e.  ( M ... ( |_ `  X ) )  ->  k  e.  ( ZZ>= `  M )
)
3635, 6syl6eleqr 2553 . . . . . . . . 9  |-  ( k  e.  ( M ... ( |_ `  X ) )  ->  k  e.  Z )
374, 36, 10syl2an 477 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M ... ( |_
`  X ) ) )  ->  C  e.  RR )
3834, 37fsumrecl 13332 . . . . . . 7  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  X ) ) C  e.  RR )
39 nfcsb1v 3414 . . . . . . . . . 10  |-  F/_ x [_ X  /  x ]_ A
4039nfel1 2632 . . . . . . . . 9  |-  F/ x [_ X  /  x ]_ A  e.  RR
41 csbeq1a 3407 . . . . . . . . . 10  |-  ( x  =  X  ->  A  =  [_ X  /  x ]_ A )
4241eleq1d 2523 . . . . . . . . 9  |-  ( x  =  X  ->  ( A  e.  RR  <->  [_ X  /  x ]_ A  e.  RR ) )
4340, 42rspc 3173 . . . . . . . 8  |-  ( X  e.  S  ->  ( A. x  e.  S  A  e.  RR  ->  [_ X  /  x ]_ A  e.  RR )
)
4433, 14, 43sylc 60 . . . . . . 7  |-  ( ph  ->  [_ X  /  x ]_ A  e.  RR )
4538, 44resubcld 9890 . . . . . 6  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  e.  RR )
46 nfcv 2616 . . . . . . 7  |-  F/_ x X
47 nfcv 2616 . . . . . . . 8  |-  F/_ x sum_ k  e.  ( M ... ( |_ `  X ) ) C
4847, 24, 39nfov 6226 . . . . . . 7  |-  F/_ x
( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )
49 fveq2 5802 . . . . . . . . . 10  |-  ( x  =  X  ->  ( |_ `  x )  =  ( |_ `  X
) )
5049oveq2d 6219 . . . . . . . . 9  |-  ( x  =  X  ->  ( M ... ( |_ `  x ) )  =  ( M ... ( |_ `  X ) ) )
5150sumeq1d 13299 . . . . . . . 8  |-  ( x  =  X  ->  sum_ k  e.  ( M ... ( |_ `  x ) ) C  =  sum_ k  e.  ( M ... ( |_ `  X ) ) C )
5251, 41oveq12d 6221 . . . . . . 7  |-  ( x  =  X  ->  ( sum_ k  e.  ( M ... ( |_ `  x ) ) C  -  A )  =  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )
5346, 48, 52, 30fvmptf 5902 . . . . . 6  |-  ( ( X  e.  S  /\  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  e.  RR )  -> 
( G `  X
)  =  ( sum_ k  e.  ( M ... ( |_ `  X
) ) C  -  [_ X  /  x ]_ A ) )
5433, 45, 53syl2anc 661 . . . . 5  |-  ( ph  ->  ( G `  X
)  =  ( sum_ k  e.  ( M ... ( |_ `  X
) ) C  -  [_ X  /  x ]_ A ) )
5532, 54oveq12d 6221 . . . 4  |-  ( ph  ->  ( ( G `  Y )  -  ( G `  X )
)  =  ( (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )
5655fveq2d 5806 . . 3  |-  ( ph  ->  ( abs `  (
( G `  Y
)  -  ( G `
 X ) ) )  =  ( abs `  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
5721recnd 9526 . . . 4  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  e.  CC )
5845recnd 9526 . . . 4  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  e.  CC )
5957, 58abssubd 13060 . . 3  |-  ( ph  ->  ( abs `  (
( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )  =  ( abs `  ( (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
6056, 59eqtrd 2495 . 2  |-  ( ph  ->  ( abs `  (
( G `  Y
)  -  ( G `
 X ) ) )  =  ( abs `  ( ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
61 dvfsum2.s . . . . . . . . . 10  |-  S  =  ( T (,) +oo )
62 ioossre 11471 . . . . . . . . . 10  |-  ( T (,) +oo )  C_  RR
6361, 62eqsstri 3497 . . . . . . . . 9  |-  S  C_  RR
6463a1i 11 . . . . . . . 8  |-  ( ph  ->  S  C_  RR )
65 dvfsum2.b1 . . . . . . . 8  |-  ( (
ph  /\  x  e.  S )  ->  B  e.  V )
66 dvfsum2.b3 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
x  e.  S  |->  A ) )  =  ( x  e.  S  |->  B ) )
6764, 13, 65, 66dvmptrecl 21632 . . . . . . 7  |-  ( (
ph  /\  x  e.  S )  ->  B  e.  RR )
6867ralrimiva 2830 . . . . . 6  |-  ( ph  ->  A. x  e.  S  B  e.  RR )
69 dvfsum2.e . . . . . . . 8  |-  ( x  =  Y  ->  B  =  E )
7069eleq1d 2523 . . . . . . 7  |-  ( x  =  Y  ->  ( B  e.  RR  <->  E  e.  RR ) )
7170rspcv 3175 . . . . . 6  |-  ( Y  e.  S  ->  ( A. x  e.  S  B  e.  RR  ->  E  e.  RR ) )
721, 68, 71sylc 60 . . . . 5  |-  ( ph  ->  E  e.  RR )
7321, 72resubcld 9890 . . . 4  |-  ( ph  ->  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  E )  e.  RR )
7463, 33sseldi 3465 . . . . . . . 8  |-  ( ph  ->  X  e.  RR )
75 reflcl 11766 . . . . . . . . 9  |-  ( X  e.  RR  ->  ( |_ `  X )  e.  RR )
7674, 75syl 16 . . . . . . . 8  |-  ( ph  ->  ( |_ `  X
)  e.  RR )
7774, 76resubcld 9890 . . . . . . 7  |-  ( ph  ->  ( X  -  ( |_ `  X ) )  e.  RR )
78 nfv 1674 . . . . . . . . . 10  |-  F/ m  B  e.  RR
79 nfcsb1v 3414 . . . . . . . . . . 11  |-  F/_ x [_ m  /  x ]_ B
8079nfel1 2632 . . . . . . . . . 10  |-  F/ x [_ m  /  x ]_ B  e.  RR
81 csbeq1a 3407 . . . . . . . . . . 11  |-  ( x  =  m  ->  B  =  [_ m  /  x ]_ B )
8281eleq1d 2523 . . . . . . . . . 10  |-  ( x  =  m  ->  ( B  e.  RR  <->  [_ m  /  x ]_ B  e.  RR ) )
8378, 80, 82cbvral 3049 . . . . . . . . 9  |-  ( A. x  e.  S  B  e.  RR  <->  A. m  e.  S  [_ m  /  x ]_ B  e.  RR )
8468, 83sylib 196 . . . . . . . 8  |-  ( ph  ->  A. m  e.  S  [_ m  /  x ]_ B  e.  RR )
85 csbeq1 3401 . . . . . . . . . 10  |-  ( m  =  X  ->  [_ m  /  x ]_ B  = 
[_ X  /  x ]_ B )
8685eleq1d 2523 . . . . . . . . 9  |-  ( m  =  X  ->  ( [_ m  /  x ]_ B  e.  RR  <->  [_ X  /  x ]_ B  e.  RR )
)
8786rspcv 3175 . . . . . . . 8  |-  ( X  e.  S  ->  ( A. m  e.  S  [_ m  /  x ]_ B  e.  RR  ->  [_ X  /  x ]_ B  e.  RR )
)
8833, 84, 87sylc 60 . . . . . . 7  |-  ( ph  ->  [_ X  /  x ]_ B  e.  RR )
8977, 88remulcld 9528 . . . . . 6  |-  ( ph  ->  ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  e.  RR )
9089, 45readdcld 9527 . . . . 5  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  e.  RR )
9190, 88resubcld 9890 . . . 4  |-  ( ph  ->  ( ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  e.  RR )
9263, 1sseldi 3465 . . . . . . . . 9  |-  ( ph  ->  Y  e.  RR )
93 reflcl 11766 . . . . . . . . . 10  |-  ( Y  e.  RR  ->  ( |_ `  Y )  e.  RR )
9492, 93syl 16 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  Y
)  e.  RR )
9592, 94resubcld 9890 . . . . . . . 8  |-  ( ph  ->  ( Y  -  ( |_ `  Y ) )  e.  RR )
9695, 72remulcld 9528 . . . . . . 7  |-  ( ph  ->  ( ( Y  -  ( |_ `  Y ) )  x.  E )  e.  RR )
9796, 21readdcld 9527 . . . . . 6  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  e.  RR )
9897, 72resubcld 9890 . . . . 5  |-  ( ph  ->  ( ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E )  e.  RR )
99 fracge0 11774 . . . . . . . . 9  |-  ( Y  e.  RR  ->  0  <_  ( Y  -  ( |_ `  Y ) ) )
10092, 99syl 16 . . . . . . . 8  |-  ( ph  ->  0  <_  ( Y  -  ( |_ `  Y ) ) )
101 dvfsum2.0 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  S  /\  D  <_  x ) )  -> 
0  <_  B )
102101expr 615 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  S )  ->  ( D  <_  x  ->  0  <_  B ) )
103102ralrimiva 2830 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  S  ( D  <_  x  -> 
0  <_  B )
)
104 dvfsum2.d . . . . . . . . . 10  |-  ( ph  ->  D  e.  RR )
105 dvfsum2.3 . . . . . . . . . 10  |-  ( ph  ->  D  <_  X )
106 dvfsum2.4 . . . . . . . . . 10  |-  ( ph  ->  X  <_  Y )
107104, 74, 92, 105, 106letrd 9642 . . . . . . . . 9  |-  ( ph  ->  D  <_  Y )
108 breq2 4407 . . . . . . . . . . 11  |-  ( x  =  Y  ->  ( D  <_  x  <->  D  <_  Y ) )
10969breq2d 4415 . . . . . . . . . . 11  |-  ( x  =  Y  ->  (
0  <_  B  <->  0  <_  E ) )
110108, 109imbi12d 320 . . . . . . . . . 10  |-  ( x  =  Y  ->  (
( D  <_  x  ->  0  <_  B )  <->  ( D  <_  Y  ->  0  <_  E ) ) )
111110rspcv 3175 . . . . . . . . 9  |-  ( Y  e.  S  ->  ( A. x  e.  S  ( D  <_  x  -> 
0  <_  B )  ->  ( D  <_  Y  ->  0  <_  E )
) )
1121, 103, 107, 111syl3c 61 . . . . . . . 8  |-  ( ph  ->  0  <_  E )
11395, 72, 100, 112mulge0d 10030 . . . . . . 7  |-  ( ph  ->  0  <_  ( ( Y  -  ( |_ `  Y ) )  x.  E ) )
11421, 96addge02d 10042 . . . . . . 7  |-  ( ph  ->  ( 0  <_  (
( Y  -  ( |_ `  Y ) )  x.  E )  <->  ( sum_ k  e.  ( M ... ( |_ `  Y
) ) C  -  [_ Y  /  x ]_ A )  <_  (
( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
115113, 114mpbid 210 . . . . . 6  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  <_  ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
11621, 97, 72, 115lesub1dd 10069 . . . . 5  |-  ( ph  ->  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  E )  <_ 
( ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E ) )
117 dvfsum2.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ZZ )
118 dvfsum2.md . . . . . . . . . . 11  |-  ( ph  ->  M  <_  ( D  +  1 ) )
119 dvfsum2.t . . . . . . . . . . 11  |-  ( ph  ->  T  e.  RR )
12013renegcld 9889 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  S )  ->  -u A  e.  RR )
12167renegcld 9889 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  S )  ->  -u B  e.  RR )
1223renegcld 9889 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  Z )  ->  -u B  e.  RR )
123 reelprrecn 9488 . . . . . . . . . . . . 13  |-  RR  e.  { RR ,  CC }
124123a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  { RR ,  CC } )
12513recnd 9526 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  S )  ->  A  e.  CC )
126124, 125, 65, 66dvmptneg 21576 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  (
x  e.  S  |->  -u A ) )  =  ( x  e.  S  |-> 
-u B ) )
1278negeqd 9718 . . . . . . . . . . 11  |-  ( x  =  k  ->  -u B  =  -u C )
128 dvfsum2.u . . . . . . . . . . 11  |-  ( ph  ->  U  e.  RR* )
129 dvfsum2.l . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  B  <_  C )
13067adantrr 716 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S ) )  ->  B  e.  RR )
1311303adant3 1008 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  B  e.  RR )
132 simp2r 1015 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  -> 
k  e.  S )
133683ad2ant1 1009 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  A. x  e.  S  B  e.  RR )
1349rspcv 3175 . . . . . . . . . . . . . 14  |-  ( k  e.  S  ->  ( A. x  e.  S  B  e.  RR  ->  C  e.  RR ) )
135132, 133, 134sylc 60 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  C  e.  RR )
136131, 135lenegd 10032 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  -> 
( B  <_  C  <->  -u C  <_  -u B ) )
137129, 136mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  S  /\  k  e.  S )  /\  ( D  <_  x  /\  x  <_  k  /\  k  <_  U ) )  ->  -u C  <_  -u B )
138 eqid 2454 . . . . . . . . . . 11  |-  ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) )  =  ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  (
sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) )
139 dvfsum2.5 . . . . . . . . . . 11  |-  ( ph  ->  Y  <_  U )
14061, 6, 117, 104, 118, 119, 120, 121, 122, 126, 127, 128, 137, 138, 33, 1, 105, 106, 139dvfsumlem3 21636 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  <_  (
( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  (
sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  /\  (
( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  -  [_ X  /  x ]_ -u B
)  <_  ( (
( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  (
sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  -  [_ Y  /  x ]_ -u B
) ) )
141140simprd 463 . . . . . . . . 9  |-  ( ph  ->  ( ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  -  [_ X  /  x ]_ -u B
)  <_  ( (
( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  (
sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  -  [_ Y  /  x ]_ -u B
) )
14277recnd 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( X  -  ( |_ `  X ) )  e.  CC )
14388recnd 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  [_ X  /  x ]_ B  e.  CC )
144142, 143mulneg2d 9912 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  =  -u ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B ) )
14538recnd 9526 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  X ) ) C  e.  CC )
14644recnd 9526 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  [_ X  /  x ]_ A  e.  CC )
147145, 146neg2subd 9850 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  -u [_ X  /  x ]_ A )  =  ( [_ X  /  x ]_ A  -  sum_ k  e.  ( M ... ( |_ `  X ) ) C ) )
14837recnd 9526 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( M ... ( |_
`  X ) ) )  ->  C  e.  CC )
14934, 148fsumneg 13375 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  =  -u sum_ k  e.  ( M ... ( |_ `  X ) ) C )
150149oveq1d 6218 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A )  =  ( -u sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  -u [_ X  /  x ]_ A ) )
151145, 146negsubdi2d 9849 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A )  =  ( [_ X  /  x ]_ A  -  sum_ k  e.  ( M ... ( |_ `  X ) ) C ) )
152147, 150, 1513eqtr4d 2505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A )  =  -u ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) )
153144, 152oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )  =  ( -u ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  -u ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )
15489recnd 9526 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  e.  CC )
155154, 58negdid 9846 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  =  ( -u ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  -u ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )
156153, 155eqtr4d 2498 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )  =  -u (
( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )
15790renegcld 9889 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  e.  RR )
158156, 157eqeltrd 2542 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )  e.  RR )
159 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ x
( X  -  ( |_ `  X ) )
160 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ x  x.
161 nfcsb1v 3414 . . . . . . . . . . . . . . . 16  |-  F/_ x [_ X  /  x ]_ B
162161nfneg 9720 . . . . . . . . . . . . . . 15  |-  F/_ x -u
[_ X  /  x ]_ B
163159, 160, 162nfov 6226 . . . . . . . . . . . . . 14  |-  F/_ x
( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )
164 nfcv 2616 . . . . . . . . . . . . . 14  |-  F/_ x  +
165 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ x sum_ k  e.  ( M ... ( |_ `  X ) ) -u C
16639nfneg 9720 . . . . . . . . . . . . . . 15  |-  F/_ x -u
[_ X  /  x ]_ A
167165, 24, 166nfov 6226 . . . . . . . . . . . . . 14  |-  F/_ x
( sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A )
168163, 164, 167nfov 6226 . . . . . . . . . . . . 13  |-  F/_ x
( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )
169 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  x  =  X )
170169, 49oveq12d 6221 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  (
x  -  ( |_
`  x ) )  =  ( X  -  ( |_ `  X ) ) )
171 csbeq1a 3407 . . . . . . . . . . . . . . . 16  |-  ( x  =  X  ->  B  =  [_ X  /  x ]_ B )
172171negeqd 9718 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  -u B  =  -u [_ X  /  x ]_ B )
173170, 172oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  (
( x  -  ( |_ `  x ) )  x.  -u B )  =  ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B ) )
17450sumeq1d 13299 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  sum_ k  e.  ( M ... ( |_ `  x ) )
-u C  =  sum_ k  e.  ( M ... ( |_ `  X
) ) -u C
)
17541negeqd 9718 . . . . . . . . . . . . . . 15  |-  ( x  =  X  ->  -u A  =  -u [_ X  /  x ]_ A )
176174, 175oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( x  =  X  ->  ( sum_ k  e.  ( M ... ( |_ `  x ) ) -u C  -  -u A )  =  ( sum_ k  e.  ( M ... ( |_ `  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )
177173, 176oveq12d 6221 . . . . . . . . . . . . 13  |-  ( x  =  X  ->  (
( ( x  -  ( |_ `  x ) )  x.  -u B
)  +  ( sum_ k  e.  ( M ... ( |_ `  x
) ) -u C  -  -u A ) )  =  ( ( ( X  -  ( |_
`  X ) )  x.  -u [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) ) )
17846, 168, 177, 138fvmptf 5902 . . . . . . . . . . . 12  |-  ( ( X  e.  S  /\  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) )
-u C  -  -u [_ X  /  x ]_ A ) )  e.  RR )  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  =  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_ `  X ) )
-u C  -  -u [_ X  /  x ]_ A ) ) )
17933, 158, 178syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  =  ( ( ( X  -  ( |_ `  X ) )  x.  -u [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_ `  X ) )
-u C  -  -u [_ X  /  x ]_ A ) ) )
180179, 156eqtrd 2495 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  =  -u ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) )
181 csbnegg 9721 . . . . . . . . . . 11  |-  ( X  e.  S  ->  [_ X  /  x ]_ -u B  =  -u [_ X  /  x ]_ B )
18233, 181syl 16 . . . . . . . . . 10  |-  ( ph  ->  [_ X  /  x ]_ -u B  =  -u [_ X  /  x ]_ B )
183180, 182oveq12d 6221 . . . . . . . . 9  |-  ( ph  ->  ( ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X )  -  [_ X  /  x ]_ -u B
)  =  ( -u ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  -u [_ X  /  x ]_ B ) )
18495recnd 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( Y  -  ( |_ `  Y ) )  e.  CC )
18572recnd 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  CC )
186184, 185mulneg2d 9912 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Y  -  ( |_ `  Y ) )  x.  -u E
)  =  -u (
( Y  -  ( |_ `  Y ) )  x.  E ) )
18712recnd 9526 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  e.  CC )
18820recnd 9526 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  [_ Y  /  x ]_ A  e.  CC )
189187, 188neg2subd 9850 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  -u [_ Y  /  x ]_ A )  =  ( [_ Y  /  x ]_ A  -  sum_ k  e.  ( M ... ( |_ `  Y ) ) C ) )
19011recnd 9526 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( M ... ( |_
`  Y ) ) )  ->  C  e.  CC )
1912, 190fsumneg 13375 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  =  -u sum_ k  e.  ( M ... ( |_ `  Y ) ) C )
192191oveq1d 6218 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A )  =  ( -u sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  -u [_ Y  /  x ]_ A ) )
193187, 188negsubdi2d 9849 . . . . . . . . . . . . . . . 16  |-  ( ph  -> 
-u ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  =  ( [_ Y  /  x ]_ A  -  sum_ k  e.  ( M ... ( |_ `  Y ) ) C ) )
194189, 192, 1933eqtr4d 2505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A )  =  -u ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) )
195186, 194oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )  =  ( -u ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  -u ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
19696recnd 9526 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Y  -  ( |_ `  Y ) )  x.  E )  e.  CC )
197196, 57negdid 9846 . . . . . . . . . . . . . 14  |-  ( ph  -> 
-u ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  =  ( -u ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  -u ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
198195, 197eqtr4d 2498 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )  =  -u (
( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
19997renegcld 9889 . . . . . . . . . . . . 13  |-  ( ph  -> 
-u ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  e.  RR )
200198, 199eqeltrd 2542 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )  e.  RR )
201 nfcv 2616 . . . . . . . . . . . . . 14  |-  F/_ x
( ( Y  -  ( |_ `  Y ) )  x.  -u E
)
202 nfcv 2616 . . . . . . . . . . . . . . 15  |-  F/_ x sum_ k  e.  ( M ... ( |_ `  Y ) ) -u C
20315nfneg 9720 . . . . . . . . . . . . . . 15  |-  F/_ x -u
[_ Y  /  x ]_ A
204202, 24, 203nfov 6226 . . . . . . . . . . . . . 14  |-  F/_ x
( sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A )
205201, 164, 204nfov 6226 . . . . . . . . . . . . 13  |-  F/_ x
( ( ( Y  -  ( |_ `  Y ) )  x.  -u E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )
206 id 22 . . . . . . . . . . . . . . . 16  |-  ( x  =  Y  ->  x  =  Y )
207206, 26oveq12d 6221 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  (
x  -  ( |_
`  x ) )  =  ( Y  -  ( |_ `  Y ) ) )
20869negeqd 9718 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  -u B  =  -u E )
209207, 208oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( x  =  Y  ->  (
( x  -  ( |_ `  x ) )  x.  -u B )  =  ( ( Y  -  ( |_ `  Y ) )  x.  -u E
) )
21027sumeq1d 13299 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  sum_ k  e.  ( M ... ( |_ `  x ) )
-u C  =  sum_ k  e.  ( M ... ( |_ `  Y
) ) -u C
)
21117negeqd 9718 . . . . . . . . . . . . . . 15  |-  ( x  =  Y  ->  -u A  =  -u [_ Y  /  x ]_ A )
212210, 211oveq12d 6221 . . . . . . . . . . . . . 14  |-  ( x  =  Y  ->  ( sum_ k  e.  ( M ... ( |_ `  x ) ) -u C  -  -u A )  =  ( sum_ k  e.  ( M ... ( |_ `  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )
213209, 212oveq12d 6221 . . . . . . . . . . . . 13  |-  ( x  =  Y  ->  (
( ( x  -  ( |_ `  x ) )  x.  -u B
)  +  ( sum_ k  e.  ( M ... ( |_ `  x
) ) -u C  -  -u A ) )  =  ( ( ( Y  -  ( |_
`  Y ) )  x.  -u E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) ) )
21422, 205, 213, 138fvmptf 5902 . . . . . . . . . . . 12  |-  ( ( Y  e.  S  /\  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) )
-u C  -  -u [_ Y  /  x ]_ A ) )  e.  RR )  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  =  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E
)  +  ( sum_ k  e.  ( M ... ( |_ `  Y
) ) -u C  -  -u [_ Y  /  x ]_ A ) ) )
2151, 200, 214syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  =  ( ( ( Y  -  ( |_ `  Y ) )  x.  -u E
)  +  ( sum_ k  e.  ( M ... ( |_ `  Y
) ) -u C  -  -u [_ Y  /  x ]_ A ) ) )
216215, 198eqtrd 2495 . . . . . . . . . 10  |-  ( ph  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  =  -u ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
217208adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  =  Y )  ->  -u B  =  -u E )
2181, 217csbied 3425 . . . . . . . . . 10  |-  ( ph  ->  [_ Y  /  x ]_ -u B  =  -u E )
219216, 218oveq12d 6221 . . . . . . . . 9  |-  ( ph  ->  ( ( ( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  -  [_ Y  /  x ]_ -u B
)  =  ( -u ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  -u E
) )
220141, 183, 2193brtr3d 4432 . . . . . . . 8  |-  ( ph  ->  ( -u ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  -u [_ X  /  x ]_ B )  <_  ( -u (
( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  -u E
) )
22190recnd 9526 . . . . . . . . 9  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  e.  CC )
222221, 143neg2subd 9850 . . . . . . . 8  |-  ( ph  ->  ( -u ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  -u [_ X  /  x ]_ B )  =  ( [_ X  /  x ]_ B  -  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
22397recnd 9526 . . . . . . . . 9  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  e.  CC )
224223, 185neg2subd 9850 . . . . . . . 8  |-  ( ph  ->  ( -u ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  -u E
)  =  ( E  -  ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
225220, 222, 2243brtr3d 4432 . . . . . . 7  |-  ( ph  ->  ( [_ X  /  x ]_ B  -  (
( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )  <_  ( E  -  ( (
( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
226221, 143negsubdi2d 9849 . . . . . . 7  |-  ( ph  -> 
-u ( ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  =  ( [_ X  /  x ]_ B  -  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
227223, 185negsubdi2d 9849 . . . . . . 7  |-  ( ph  -> 
-u ( ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E )  =  ( E  -  ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) ) )
228225, 226, 2273brtr4d 4433 . . . . . 6  |-  ( ph  -> 
-u ( ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  <_  -u ( ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E ) )
22998, 91lenegd 10032 . . . . . 6  |-  ( ph  ->  ( ( ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E )  <_  ( ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  <->  -u ( ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  <_  -u ( ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E ) ) )
230228, 229mpbird 232 . . . . 5  |-  ( ph  ->  ( ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  -  E )  <_  ( ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B ) )
23173, 98, 91, 116, 230letrd 9642 . . . 4  |-  ( ph  ->  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  E )  <_ 
( ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B ) )
232 1red 9515 . . . . . . . 8  |-  ( ph  ->  1  e.  RR )
233 nfv 1674 . . . . . . . . . . 11  |-  F/ x  D  <_  X
234 nfcv 2616 . . . . . . . . . . . 12  |-  F/_ x
0
235 nfcv 2616 . . . . . . . . . . . 12  |-  F/_ x  <_
236234, 235, 161nfbr 4447 . . . . . . . . . . 11  |-  F/ x
0  <_  [_ X  /  x ]_ B
237233, 236nfim 1858 . . . . . . . . . 10  |-  F/ x
( D  <_  X  ->  0  <_  [_ X  /  x ]_ B )
238 breq2 4407 . . . . . . . . . . 11  |-  ( x  =  X  ->  ( D  <_  x  <->  D  <_  X ) )
239171breq2d 4415 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
0  <_  B  <->  0  <_  [_ X  /  x ]_ B ) )
240238, 239imbi12d 320 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( D  <_  x  ->  0  <_  B )  <->  ( D  <_  X  ->  0  <_  [_ X  /  x ]_ B ) ) )
241237, 240rspc 3173 . . . . . . . . 9  |-  ( X  e.  S  ->  ( A. x  e.  S  ( D  <_  x  -> 
0  <_  B )  ->  ( D  <_  X  ->  0  <_  [_ X  /  x ]_ B ) ) )
24233, 103, 105, 241syl3c 61 . . . . . . . 8  |-  ( ph  ->  0  <_  [_ X  /  x ]_ B )
243 fracle1 11773 . . . . . . . . 9  |-  ( X  e.  RR  ->  ( X  -  ( |_ `  X ) )  <_ 
1 )
24474, 243syl 16 . . . . . . . 8  |-  ( ph  ->  ( X  -  ( |_ `  X ) )  <_  1 )
24577, 232, 88, 242, 244lemul1ad 10386 . . . . . . 7  |-  ( ph  ->  ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  <_  ( 1  x. 
[_ X  /  x ]_ B ) )
246143mulid2d 9518 . . . . . . 7  |-  ( ph  ->  ( 1  x.  [_ X  /  x ]_ B
)  =  [_ X  /  x ]_ B )
247245, 246breqtrd 4427 . . . . . 6  |-  ( ph  ->  ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  <_  [_ X  /  x ]_ B )
24889, 88, 45, 247leadd1dd 10067 . . . . 5  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  <_  ( [_ X  /  x ]_ B  +  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) )
24990, 88, 45lesubadd2d 10052 . . . . 5  |-  ( ph  ->  ( ( ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  <_  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A )  <-> 
( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  <_  ( [_ X  /  x ]_ B  +  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
250248, 249mpbird 232 . . . 4  |-  ( ph  ->  ( ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  -  [_ X  /  x ]_ B )  <_  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) )
25173, 91, 45, 231, 250letrd 9642 . . 3  |-  ( ph  ->  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  E )  <_ 
( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )
25221, 72readdcld 9527 . . . 4  |-  ( ph  ->  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  +  E )  e.  RR )
253 fracge0 11774 . . . . . . 7  |-  ( X  e.  RR  ->  0  <_  ( X  -  ( |_ `  X ) ) )
25474, 253syl 16 . . . . . 6  |-  ( ph  ->  0  <_  ( X  -  ( |_ `  X ) ) )
25577, 88, 254, 242mulge0d 10030 . . . . 5  |-  ( ph  ->  0  <_  ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B ) )
25645, 89addge02d 10042 . . . . 5  |-  ( ph  ->  ( 0  <_  (
( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  <->  ( sum_ k  e.  ( M ... ( |_ `  X
) ) C  -  [_ X  /  x ]_ A )  <_  (
( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
257255, 256mpbid 210 . . . 4  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  <_  ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) )
258140simpld 459 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  S  |->  ( ( ( x  -  ( |_
`  x ) )  x.  -u B )  +  ( sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  Y )  <_  (
( x  e.  S  |->  ( ( ( x  -  ( |_ `  x ) )  x.  -u B )  +  (
sum_ k  e.  ( M ... ( |_
`  x ) )
-u C  -  -u A
) ) ) `  X ) )
259258, 216, 1803brtr3d 4432 . . . . . 6  |-  ( ph  -> 
-u ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  <_  -u ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) )
26090, 97lenegd 10032 . . . . . 6  |-  ( ph  ->  ( ( ( ( X  -  ( |_
`  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  <_  ( (
( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  <->  -u ( ( ( Y  -  ( |_
`  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  <_  -u ( ( ( X  -  ( |_ `  X ) )  x.  [_ X  /  x ]_ B )  +  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) ) ) )
261259, 260mpbird 232 . . . . 5  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  <_  ( (
( Y  -  ( |_ `  Y ) )  x.  E )  +  ( sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
262 fracle1 11773 . . . . . . . . . 10  |-  ( Y  e.  RR  ->  ( Y  -  ( |_ `  Y ) )  <_ 
1 )
26392, 262syl 16 . . . . . . . . 9  |-  ( ph  ->  ( Y  -  ( |_ `  Y ) )  <_  1 )
26495, 232, 72, 112, 263lemul1ad 10386 . . . . . . . 8  |-  ( ph  ->  ( ( Y  -  ( |_ `  Y ) )  x.  E )  <_  ( 1  x.  E ) )
265185mulid2d 9518 . . . . . . . 8  |-  ( ph  ->  ( 1  x.  E
)  =  E )
266264, 265breqtrd 4427 . . . . . . 7  |-  ( ph  ->  ( ( Y  -  ( |_ `  Y ) )  x.  E )  <_  E )
26796, 72, 21, 266leadd1dd 10067 . . . . . 6  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  <_  ( E  +  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )
268185, 57addcomd 9685 . . . . . 6  |-  ( ph  ->  ( E  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  =  ( (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A )  +  E ) )
269267, 268breqtrd 4427 . . . . 5  |-  ( ph  ->  ( ( ( Y  -  ( |_ `  Y ) )  x.  E )  +  (
sum_ k  e.  ( M ... ( |_
`  Y ) ) C  -  [_ Y  /  x ]_ A ) )  <_  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  +  E ) )
27090, 97, 252, 261, 269letrd 9642 . . . 4  |-  ( ph  ->  ( ( ( X  -  ( |_ `  X ) )  x. 
[_ X  /  x ]_ B )  +  (
sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A ) )  <_  ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  +  E ) )
27145, 90, 252, 257, 270letrd 9642 . . 3  |-  ( ph  ->  ( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  <_  ( ( sum_ k  e.  ( M ... ( |_ `  Y
) ) C  -  [_ Y  /  x ]_ A )  +  E
) )
27245, 21, 72absdifled 13042 . . 3  |-  ( ph  ->  ( ( abs `  (
( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )  <_  E  <->  ( ( ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A )  -  E )  <_ 
( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  /\  ( sum_ k  e.  ( M ... ( |_ `  X ) ) C  -  [_ X  /  x ]_ A )  <_  ( ( sum_ k  e.  ( M ... ( |_ `  Y
) ) C  -  [_ Y  /  x ]_ A )  +  E
) ) ) )
273251, 271, 272mpbir2and 913 . 2  |-  ( ph  ->  ( abs `  (
( sum_ k  e.  ( M ... ( |_
`  X ) ) C  -  [_ X  /  x ]_ A )  -  ( sum_ k  e.  ( M ... ( |_ `  Y ) ) C  -  [_ Y  /  x ]_ A ) ) )  <_  E
)
27460, 273eqbrtrd 4423 1  |-  ( ph  ->  ( abs `  (
( G `  Y
)  -  ( G `
 X ) ) )  <_  E )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1370    e. wcel 1758   A.wral 2799   [_csb 3398    C_ wss 3439   {cpr 3990   class class class wbr 4403    |-> cmpt 4461   ` cfv 5529  (class class class)co 6203   CCcc 9394   RRcr 9395   0cc0 9396   1c1 9397    + caddc 9399    x. cmul 9401   +oocpnf 9529   RR*cxr 9531    <_ cle 9533    - cmin 9709   -ucneg 9710   ZZcz 10760   ZZ>=cuz 10975   (,)cioo 11414   ...cfz 11557   |_cfl 11760   abscabs 12844   sum_csu 13284    _D cdv 21474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-inf2 7961  ax-cnex 9452  ax-resscn 9453  ax-1cn 9454  ax-icn 9455  ax-addcl 9456  ax-addrcl 9457  ax-mulcl 9458  ax-mulrcl 9459  ax-mulcom 9460  ax-addass 9461  ax-mulass 9462  ax-distr 9463  ax-i2m1 9464  ax-1ne0 9465  ax-1rid 9466  ax-rnegex 9467  ax-rrecex 9468  ax-cnre 9469  ax-pre-lttri 9470  ax-pre-lttrn 9471  ax-pre-ltadd 9472  ax-pre-mulgt0 9473  ax-pre-sup 9474  ax-addf 9475  ax-mulf 9476
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-iin 4285  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-of 6433  df-om 6590  df-1st 6690  df-2nd 6691  df-supp 6804  df-recs 6945  df-rdg 6979  df-1o 7033  df-2o 7034  df-oadd 7037  df-er 7214  df-map 7329  df-pm 7330  df-ixp 7377  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-fsupp 7735  df-fi 7775  df-sup 7805  df-oi 7838  df-card 8223  df-cda 8451  df-pnf 9534  df-mnf 9535  df-xr 9536  df-ltxr 9537  df-le 9538  df-sub 9711  df-neg 9712  df-div 10108  df-nn 10437  df-2 10494  df-3 10495  df-4 10496  df-5 10497  df-6 10498  df-7 10499  df-8 10500  df-9 10501  df-10 10502  df-n0 10694  df-z 10761  df-dec 10870  df-uz 10976  df-q 11068  df-rp 11106  df-xneg 11203  df-xadd 11204  df-xmul 11205  df-ioo 11418  df-ico 11420  df-icc 11421  df-fz 11558  df-fzo 11669  df-fl 11762  df-seq 11927  df-exp 11986  df-hash 12224  df-cj 12709  df-re 12710  df-im 12711  df-sqr 12845  df-abs 12846  df-clim 13087  df-sum 13285  df-struct 14297  df-ndx 14298  df-slot 14299  df-base 14300  df-sets 14301  df-ress 14302  df-plusg 14373  df-mulr 14374  df-starv 14375  df-sca 14376  df-vsca 14377  df-ip 14378  df-tset 14379  df-ple 14380  df-ds 14382  df-unif 14383  df-hom 14384  df-cco 14385  df-rest 14483  df-topn 14484  df-0g 14502  df-gsum 14503  df-topgen 14504  df-pt 14505  df-prds 14508  df-xrs 14562  df-qtop 14567  df-imas 14568  df-xps 14570  df-mre 14646  df-mrc 14647  df-acs 14649  df-mnd 15537  df-submnd 15587  df-mulg 15670  df-cntz 15957  df-cmn 16403  df-psmet 17937  df-xmet 17938  df-met 17939  df-bl 17940  df-mopn 17941  df-fbas 17942  df-fg 17943  df-cnfld 17947  df-top 18638  df-bases 18640  df-topon 18641  df-topsp 18642  df-cld 18758  df-ntr 18759  df-cls 18760  df-nei 18837  df-lp 18875  df-perf 18876  df-cn 18966  df-cnp 18967  df-haus 19054  df-cmp 19125  df-tx 19270  df-hmeo 19463  df-fil 19554  df-fm 19646  df-flim 19647  df-flf 19648  df-xms 20030  df-ms 20031  df-tms 20032  df-cncf 20589  df-limc 21477  df-dv 21478
This theorem is referenced by:  logfacbnd3  22698  log2sumbnd  22929
  Copyright terms: Public domain W3C validator