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

Theorem c1lip1 22567
Description: C1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Hypotheses
Ref Expression
c1lip1.a  |-  ( ph  ->  A  e.  RR )
c1lip1.b  |-  ( ph  ->  B  e.  RR )
c1lip1.f  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
c1lip1.dv  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR ) )
c1lip1.cn  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR ) )
Assertion
Ref Expression
c1lip1  |-  ( ph  ->  E. k  e.  RR  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) )
Distinct variable groups:    ph, x, y, k    x, A, y, k    x, B, y, k    x, F, y, k

Proof of Theorem c1lip1
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 9585 . . . 4  |-  0  e.  RR
21ne0ii 3790 . . 3  |-  RR  =/=  (/)
3 ral0 3922 . . . . 5  |-  A. x  e.  (/)  A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) )
4 c1lip1.a . . . . . . . . 9  |-  ( ph  ->  A  e.  RR )
54rexrd 9632 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
6 c1lip1.b . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
76rexrd 9632 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
8 icc0 11580 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A [,] B
)  =  (/)  <->  B  <  A ) )
95, 7, 8syl2anc 659 . . . . . . 7  |-  ( ph  ->  ( ( A [,] B )  =  (/)  <->  B  <  A ) )
109biimpar 483 . . . . . 6  |-  ( (
ph  /\  B  <  A )  ->  ( A [,] B )  =  (/) )
1110raleqdv 3057 . . . . 5  |-  ( (
ph  /\  B  <  A )  ->  ( A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) )  <->  A. x  e.  (/)  A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
123, 11mpbiri 233 . . . 4  |-  ( (
ph  /\  B  <  A )  ->  A. x  e.  ( A [,] B
) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )
1312ralrimivw 2869 . . 3  |-  ( (
ph  /\  B  <  A )  ->  A. k  e.  RR  A. x  e.  ( A [,] B
) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )
14 r19.2z 3906 . . 3  |-  ( ( RR  =/=  (/)  /\  A. k  e.  RR  A. x  e.  ( A [,] B
) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )  ->  E. k  e.  RR  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) )
152, 13, 14sylancr 661 . 2  |-  ( (
ph  /\  B  <  A )  ->  E. k  e.  RR  A. x  e.  ( A [,] B
) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )
164adantr 463 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  A  e.  RR )
176adantr 463 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  B  e.  RR )
18 simpr 459 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  A  <_  B )
19 c1lip1.f . . . . . 6  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
2019adantr 463 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  F  e.  ( CC  ^pm  RR ) )
21 c1lip1.dv . . . . . 6  |-  ( ph  ->  ( ( RR  _D  F )  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR ) )
2221adantr 463 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  ( ( RR  _D  F )  |`  ( A [,] B ) )  e.  ( ( A [,] B )
-cn-> RR ) )
23 c1lip1.cn . . . . . 6  |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR ) )
2423adantr 463 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  ( F  |`  ( A [,] B
) )  e.  ( ( A [,] B
) -cn-> RR ) )
25 eqid 2454 . . . . 5  |-  sup (
( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  =  sup (
( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )
2616, 17, 18, 20, 22, 24, 25c1liplem1 22566 . . . 4  |-  ( (
ph  /\  A  <_  B )  ->  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  e.  RR  /\  A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  x.  ( abs `  ( b  -  a
) ) ) ) ) )
27 oveq1 6277 . . . . . . . 8  |-  ( k  =  sup ( ( abs " ( ( RR  _D  F )
" ( A [,] B ) ) ) ,  RR ,  <  )  ->  ( k  x.  ( abs `  (
b  -  a ) ) )  =  ( sup ( ( abs " ( ( RR 
_D  F ) "
( A [,] B
) ) ) ,  RR ,  <  )  x.  ( abs `  (
b  -  a ) ) ) )
2827breq2d 4451 . . . . . . 7  |-  ( k  =  sup ( ( abs " ( ( RR  _D  F )
" ( A [,] B ) ) ) ,  RR ,  <  )  ->  ( ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  x.  ( abs `  ( b  -  a
) ) ) ) )
2928imbi2d 314 . . . . . 6  |-  ( k  =  sup ( ( abs " ( ( RR  _D  F )
" ( A [,] B ) ) ) ,  RR ,  <  )  ->  ( ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  <-> 
( a  <  b  ->  ( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  x.  ( abs `  ( b  -  a
) ) ) ) ) )
30292ralbidv 2898 . . . . 5  |-  ( k  =  sup ( ( abs " ( ( RR  _D  F )
" ( A [,] B ) ) ) ,  RR ,  <  )  ->  ( A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  <->  A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  x.  ( abs `  ( b  -  a
) ) ) ) ) )
3130rspcev 3207 . . . 4  |-  ( ( sup ( ( abs " ( ( RR 
_D  F ) "
( A [,] B
) ) ) ,  RR ,  <  )  e.  RR  /\  A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  ( sup ( ( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  x.  ( abs `  ( b  -  a
) ) ) ) )  ->  E. k  e.  RR  A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) ) )
3226, 31syl 16 . . 3  |-  ( (
ph  /\  A  <_  B )  ->  E. k  e.  RR  A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) ) )
33 breq1 4442 . . . . . . . . . 10  |-  ( a  =  x  ->  (
a  <  b  <->  x  <  b ) )
34 fveq2 5848 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  ( F `  a )  =  ( F `  x ) )
3534oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  x  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  x ) ) )
3635fveq2d 5852 . . . . . . . . . . 11  |-  ( a  =  x  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  x ) ) ) )
37 oveq2 6278 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  (
b  -  a )  =  ( b  -  x ) )
3837fveq2d 5852 . . . . . . . . . . . 12  |-  ( a  =  x  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  x ) ) )
3938oveq2d 6286 . . . . . . . . . . 11  |-  ( a  =  x  ->  (
k  x.  ( abs `  ( b  -  a
) ) )  =  ( k  x.  ( abs `  ( b  -  x ) ) ) )
4036, 39breq12d 4452 . . . . . . . . . 10  |-  ( a  =  x  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( k  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( b  -  x
) ) ) ) )
4133, 40imbi12d 318 . . . . . . . . 9  |-  ( a  =  x  ->  (
( a  <  b  ->  ( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( k  x.  ( abs `  (
b  -  a ) ) ) )  <->  ( x  <  b  ->  ( abs `  ( ( F `  b )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( b  -  x
) ) ) ) ) )
42 breq2 4443 . . . . . . . . . 10  |-  ( b  =  y  ->  (
x  <  b  <->  x  <  y ) )
43 fveq2 5848 . . . . . . . . . . . . 13  |-  ( b  =  y  ->  ( F `  b )  =  ( F `  y ) )
4443oveq1d 6285 . . . . . . . . . . . 12  |-  ( b  =  y  ->  (
( F `  b
)  -  ( F `
 x ) )  =  ( ( F `
 y )  -  ( F `  x ) ) )
4544fveq2d 5852 . . . . . . . . . . 11  |-  ( b  =  y  ->  ( abs `  ( ( F `
 b )  -  ( F `  x ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
46 oveq1 6277 . . . . . . . . . . . . 13  |-  ( b  =  y  ->  (
b  -  x )  =  ( y  -  x ) )
4746fveq2d 5852 . . . . . . . . . . . 12  |-  ( b  =  y  ->  ( abs `  ( b  -  x ) )  =  ( abs `  (
y  -  x ) ) )
4847oveq2d 6286 . . . . . . . . . . 11  |-  ( b  =  y  ->  (
k  x.  ( abs `  ( b  -  x
) ) )  =  ( k  x.  ( abs `  ( y  -  x ) ) ) )
4945, 48breq12d 4452 . . . . . . . . . 10  |-  ( b  =  y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
b  -  x ) ) )  <->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) )
5042, 49imbi12d 318 . . . . . . . . 9  |-  ( b  =  y  ->  (
( x  <  b  ->  ( abs `  (
( F `  b
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
b  -  x ) ) ) )  <->  ( x  <  y  ->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) ) )
5141, 50rspc2v 3216 . . . . . . . 8  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  -> 
( A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( x  < 
y  ->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) ) )
5251ad2antlr 724 . . . . . . 7  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  x  <  y )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( x  < 
y  ->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) ) )
53 pm2.27 39 . . . . . . . 8  |-  ( x  <  y  ->  (
( x  <  y  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )  -> 
( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
5453adantl 464 . . . . . . 7  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  x  <  y )  ->  (
( x  <  y  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )  -> 
( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
5552, 54syld 44 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  x  <  y )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
56 0le0 10621 . . . . . . . . . 10  |-  0  <_  0
57 fvres 5862 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  =  ( F `  x
) )
5857ad2antrl 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  =  ( F `  x
) )
59 cncff 21566 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR )  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR )
6023, 59syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR )
6160ad2antrr 723 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B
) --> RR )
62 simpl 455 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  ->  x  e.  ( A [,] B ) )
63 ffvelrn 6005 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR  /\  x  e.  ( A [,] B ) )  -> 
( ( F  |`  ( A [,] B ) ) `  x )  e.  RR )
6461, 62, 63syl2an 475 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  e.  RR )
6558, 64eqeltrrd 2543 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  x )  e.  RR )
6665recnd 9611 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  x )  e.  CC )
6766subidd 9910 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F `  x
)  -  ( F `
 x ) )  =  0 )
6867abs00bd 13209 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 x )  -  ( F `  x ) ) )  =  0 )
69 iccssre 11609 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
704, 6, 69syl2anc 659 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A [,] B
)  C_  RR )
7170ad3antrrr 727 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( A [,] B )  C_  RR )
72 simprl 754 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  ( A [,] B
) )
7371, 72sseldd 3490 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  RR )
7473recnd 9611 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  CC )
7574subidd 9910 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  -  x )  =  0 )
7675abs00bd 13209 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( x  -  x ) )  =  0 )
7776oveq2d 6286 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
k  x.  ( abs `  ( x  -  x
) ) )  =  ( k  x.  0 ) )
78 simplr 753 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  k  e.  RR )
7978recnd 9611 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  k  e.  CC )
8079mul01d 9768 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
k  x.  0 )  =  0 )
8177, 80eqtrd 2495 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
k  x.  ( abs `  ( x  -  x
) ) )  =  0 )
8268, 81breq12d 4452 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( abs `  (
( F `  x
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
x  -  x ) ) )  <->  0  <_  0 ) )
8356, 82mpbiri 233 . . . . . . . . 9  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 x )  -  ( F `  x ) ) )  <_  (
k  x.  ( abs `  ( x  -  x
) ) ) )
84 fveq2 5848 . . . . . . . . . . . 12  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
8584oveq1d 6285 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( F `  x
)  -  ( F `
 x ) )  =  ( ( F `
 y )  -  ( F `  x ) ) )
8685fveq2d 5852 . . . . . . . . . 10  |-  ( x  =  y  ->  ( abs `  ( ( F `
 x )  -  ( F `  x ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
87 oveq1 6277 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  -  x )  =  ( y  -  x ) )
8887fveq2d 5852 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( abs `  ( x  -  x ) )  =  ( abs `  (
y  -  x ) ) )
8988oveq2d 6286 . . . . . . . . . 10  |-  ( x  =  y  ->  (
k  x.  ( abs `  ( x  -  x
) ) )  =  ( k  x.  ( abs `  ( y  -  x ) ) ) )
9086, 89breq12d 4452 . . . . . . . . 9  |-  ( x  =  y  ->  (
( abs `  (
( F `  x
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
x  -  x ) ) )  <->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) )
9183, 90syl5ibcom 220 . . . . . . . 8  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  =  y  -> 
( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
9291imp 427 . . . . . . 7  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  x  =  y )  -> 
( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )
9392a1d 25 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  x  =  y )  -> 
( A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
94 breq1 4442 . . . . . . . . . . 11  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
95 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( a  =  y  ->  ( F `  a )  =  ( F `  y ) )
9695oveq2d 6286 . . . . . . . . . . . . 13  |-  ( a  =  y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  y ) ) )
9796fveq2d 5852 . . . . . . . . . . . 12  |-  ( a  =  y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  y ) ) ) )
98 oveq2 6278 . . . . . . . . . . . . . 14  |-  ( a  =  y  ->  (
b  -  a )  =  ( b  -  y ) )
9998fveq2d 5852 . . . . . . . . . . . . 13  |-  ( a  =  y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  y ) ) )
10099oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  y  ->  (
k  x.  ( abs `  ( b  -  a
) ) )  =  ( k  x.  ( abs `  ( b  -  y ) ) ) )
10197, 100breq12d 4452 . . . . . . . . . . 11  |-  ( a  =  y  ->  (
( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( k  x.  ( abs `  (
b  -  a ) ) )  <->  ( abs `  ( ( F `  b )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( b  -  y
) ) ) ) )
10294, 101imbi12d 318 . . . . . . . . . 10  |-  ( a  =  y  ->  (
( a  <  b  ->  ( abs `  (
( F `  b
)  -  ( F `
 a ) ) )  <_  ( k  x.  ( abs `  (
b  -  a ) ) ) )  <->  ( y  <  b  ->  ( abs `  ( ( F `  b )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( b  -  y
) ) ) ) ) )
103 breq2 4443 . . . . . . . . . . 11  |-  ( b  =  x  ->  (
y  <  b  <->  y  <  x ) )
104 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  ( F `  b )  =  ( F `  x ) )
105104oveq1d 6285 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
( F `  b
)  -  ( F `
 y ) )  =  ( ( F `
 x )  -  ( F `  y ) ) )
106105fveq2d 5852 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( abs `  ( ( F `
 b )  -  ( F `  y ) ) )  =  ( abs `  ( ( F `  x )  -  ( F `  y ) ) ) )
107 oveq1 6277 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
b  -  y )  =  ( x  -  y ) )
108107fveq2d 5852 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  ( abs `  ( b  -  y ) )  =  ( abs `  (
x  -  y ) ) )
109108oveq2d 6286 . . . . . . . . . . . 12  |-  ( b  =  x  ->  (
k  x.  ( abs `  ( b  -  y
) ) )  =  ( k  x.  ( abs `  ( x  -  y ) ) ) )
110106, 109breq12d 4452 . . . . . . . . . . 11  |-  ( b  =  x  ->  (
( abs `  (
( F `  b
)  -  ( F `
 y ) ) )  <_  ( k  x.  ( abs `  (
b  -  y ) ) )  <->  ( abs `  ( ( F `  x )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( x  -  y
) ) ) ) )
111103, 110imbi12d 318 . . . . . . . . . 10  |-  ( b  =  x  ->  (
( y  <  b  ->  ( abs `  (
( F `  b
)  -  ( F `
 y ) ) )  <_  ( k  x.  ( abs `  (
b  -  y ) ) ) )  <->  ( y  <  x  ->  ( abs `  ( ( F `  x )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( x  -  y
) ) ) ) ) )
112102, 111rspc2v 3216 . . . . . . . . 9  |-  ( ( y  e.  ( A [,] B )  /\  x  e.  ( A [,] B ) )  -> 
( A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( y  < 
x  ->  ( abs `  ( ( F `  x )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( x  -  y
) ) ) ) ) )
113112ancoms 451 . . . . . . . 8  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  -> 
( A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( y  < 
x  ->  ( abs `  ( ( F `  x )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( x  -  y
) ) ) ) ) )
114113ad2antlr 724 . . . . . . 7  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( y  < 
x  ->  ( abs `  ( ( F `  x )  -  ( F `  y )
) )  <_  (
k  x.  ( abs `  ( x  -  y
) ) ) ) ) )
115 simpr 459 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  y  <  x )
116 fvres 5862 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( A [,] B )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  =  ( F `  y
) )
117116ad2antll 726 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  =  ( F `  y
) )
118 simpr 459 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  -> 
y  e.  ( A [,] B ) )
119 ffvelrn 6005 . . . . . . . . . . . . . . 15  |-  ( ( ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR  /\  y  e.  ( A [,] B ) )  -> 
( ( F  |`  ( A [,] B ) ) `  y )  e.  RR )
12061, 118, 119syl2an 475 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  e.  RR )
121117, 120eqeltrrd 2543 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  y )  e.  RR )
122121recnd 9611 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  y )  e.  CC )
12366, 122abssubd 13369 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 x )  -  ( F `  y ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
124123adantr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  ( abs `  ( ( F `
 x )  -  ( F `  y ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
12570ad2antrr 723 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  ( A [,] B )  C_  RR )
126125sseld 3488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
x  e.  ( A [,] B )  ->  x  e.  RR )
)
127125sseld 3488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
y  e.  ( A [,] B )  -> 
y  e.  RR ) )
128126, 127anim12d 561 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  ->  ( x  e.  RR  /\  y  e.  RR ) ) )
129128imp 427 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  e.  RR  /\  y  e.  RR )
)
130 recn 9571 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  x  e.  CC )
131 recn 9571 . . . . . . . . . . . . . 14  |-  ( y  e.  RR  ->  y  e.  CC )
132 abssub 13244 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( abs `  (
x  -  y ) )  =  ( abs `  ( y  -  x
) ) )
133130, 131, 132syl2an 475 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( abs `  (
x  -  y ) )  =  ( abs `  ( y  -  x
) ) )
134129, 133syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( x  -  y ) )  =  ( abs `  (
y  -  x ) ) )
135134adantr 463 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  ( abs `  ( x  -  y ) )  =  ( abs `  (
y  -  x ) ) )
136135oveq2d 6286 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  (
k  x.  ( abs `  ( x  -  y
) ) )  =  ( k  x.  ( abs `  ( y  -  x ) ) ) )
137124, 136breq12d 4452 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  (
( abs `  (
( F `  x
)  -  ( F `
 y ) ) )  <_  ( k  x.  ( abs `  (
x  -  y ) ) )  <->  ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) )
138137biimpd 207 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  (
( abs `  (
( F `  x
)  -  ( F `
 y ) ) )  <_  ( k  x.  ( abs `  (
x  -  y ) ) )  ->  ( abs `  ( ( F `
 y )  -  ( F `  x ) ) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) )
139115, 138embantd 54 . . . . . . 7  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  (
( y  <  x  ->  ( abs `  (
( F `  x
)  -  ( F `
 y ) ) )  <_  ( k  x.  ( abs `  (
x  -  y ) ) ) )  -> 
( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
140114, 139syld 44 . . . . . 6  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
141 lttri4 9658 . . . . . . 7  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  <  y  \/  x  =  y  \/  y  <  x ) )
142129, 141syl 16 . . . . . 6  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  <  y  \/  x  =  y  \/  y  <  x ) )
14355, 93, 140, 142mpjao3dan 1293 . . . . 5  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
144143ralrimdvva 2878 . . . 4  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  ( A. a  e.  ( A [,] B ) A. b  e.  ( A [,] B ) ( a  <  b  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) ) )
145144reximdva 2929 . . 3  |-  ( (
ph  /\  A  <_  B )  ->  ( E. k  e.  RR  A. a  e.  ( A [,] B
) A. b  e.  ( A [,] B
) ( a  < 
b  ->  ( abs `  ( ( F `  b )  -  ( F `  a )
) )  <_  (
k  x.  ( abs `  ( b  -  a
) ) ) )  ->  E. k  e.  RR  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) ) )
14632, 145mpd 15 . 2  |-  ( (
ph  /\  A  <_  B )  ->  E. k  e.  RR  A. x  e.  ( A [,] B
) A. y  e.  ( A [,] B
) ( abs `  (
( F `  y
)  -  ( F `
 x ) ) )  <_  ( k  x.  ( abs `  (
y  -  x ) ) ) )
14715, 146, 6, 4ltlecasei 9681 1  |-  ( ph  ->  E. k  e.  RR  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( abs `  ( ( F `  y )  -  ( F `  x )
) )  <_  (
k  x.  ( abs `  ( y  -  x
) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    \/ w3o 970    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805    C_ wss 3461   (/)c0 3783   class class class wbr 4439    |` cres 4990   "cima 4991   -->wf 5566   ` cfv 5570  (class class class)co 6270    ^pm cpm 7413   supcsup 7892   CCcc 9479   RRcr 9480   0cc0 9481    x. cmul 9486   RR*cxr 9616    < clt 9617    <_ cle 9618    - cmin 9796   [,]cicc 11535   abscabs 13152   -cn->ccncf 21549    _D cdv 22436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559  ax-addf 9560  ax-mulf 9561
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-iin 4318  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-of 6513  df-om 6674  df-1st 6773  df-2nd 6774  df-supp 6892  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7463  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fsupp 7822  df-fi 7863  df-sup 7893  df-oi 7927  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-q 11184  df-rp 11222  df-xneg 11321  df-xadd 11322  df-xmul 11323  df-ioo 11536  df-ico 11538  df-icc 11539  df-fz 11676  df-fzo 11800  df-seq 12093  df-exp 12152  df-hash 12391  df-cj 13017  df-re 13018  df-im 13019  df-sqrt 13153  df-abs 13154  df-struct 14721  df-ndx 14722  df-slot 14723  df-base 14724  df-sets 14725  df-ress 14726  df-plusg 14800  df-mulr 14801  df-starv 14802  df-sca 14803  df-vsca 14804  df-ip 14805  df-tset 14806  df-ple 14807  df-ds 14809  df-unif 14810  df-hom 14811  df-cco 14812  df-rest 14915  df-topn 14916  df-0g 14934  df-gsum 14935  df-topgen 14936  df-pt 14937  df-prds 14940  df-xrs 14994  df-qtop 14999  df-imas 15000  df-xps 15002  df-mre 15078  df-mrc 15079  df-acs 15081  df-mgm 16074  df-sgrp 16113  df-mnd 16123  df-submnd 16169  df-mulg 16262  df-cntz 16557  df-cmn 17002  df-psmet 18609  df-xmet 18610  df-met 18611  df-bl 18612  df-mopn 18613  df-fbas 18614  df-fg 18615  df-cnfld 18619  df-top 19569  df-bases 19571  df-topon 19572  df-topsp 19573  df-cld 19690  df-ntr 19691  df-cls 19692  df-nei 19769  df-lp 19807  df-perf 19808  df-cn 19898  df-cnp 19899  df-haus 19986  df-cmp 20057  df-tx 20232  df-hmeo 20425  df-fil 20516  df-fm 20608  df-flim 20609  df-flf 20610  df-xms 20992  df-ms 20993  df-tms 20994  df-cncf 21551  df-limc 22439  df-dv 22440
This theorem is referenced by:  c1lip2  22568
  Copyright terms: Public domain W3C validator