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

Theorem c1lip1 22997
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 9668 . . . 4  |-  0  e.  RR
21ne0ii 3749 . . 3  |-  RR  =/=  (/)
3 ral0 3885 . . . . 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 9715 . . . . . . . 8  |-  ( ph  ->  A  e.  RR* )
6 c1lip1.b . . . . . . . . 9  |-  ( ph  ->  B  e.  RR )
76rexrd 9715 . . . . . . . 8  |-  ( ph  ->  B  e.  RR* )
8 icc0 11712 . . . . . . . 8  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  (
( A [,] B
)  =  (/)  <->  B  <  A ) )
95, 7, 8syl2anc 671 . . . . . . 7  |-  ( ph  ->  ( ( A [,] B )  =  (/)  <->  B  <  A ) )
109biimpar 492 . . . . . 6  |-  ( (
ph  /\  B  <  A )  ->  ( A [,] B )  =  (/) )
1110raleqdv 3004 . . . . 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 241 . . . 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 2814 . . 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 3869 . . 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 674 . 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 471 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  A  e.  RR )
176adantr 471 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  B  e.  RR )
18 simpr 467 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  A  <_  B )
19 c1lip1.f . . . . . 6  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
2019adantr 471 . . . . 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 471 . . . . 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 471 . . . . 5  |-  ( (
ph  /\  A  <_  B )  ->  ( F  |`  ( A [,] B
) )  e.  ( ( A [,] B
) -cn-> RR ) )
25 eqid 2461 . . . . 5  |-  sup (
( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )  =  sup (
( abs " (
( RR  _D  F
) " ( A [,] B ) ) ) ,  RR ,  <  )
2616, 17, 18, 20, 22, 24, 25c1liplem1 22996 . . . 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 6321 . . . . . . . 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 4427 . . . . . . 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 322 . . . . . 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 2843 . . . . 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 3161 . . . 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 17 . . 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 4418 . . . . . . . . . 10  |-  ( a  =  x  ->  (
a  <  b  <->  x  <  b ) )
34 fveq2 5887 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  ( F `  a )  =  ( F `  x ) )
3534oveq2d 6330 . . . . . . . . . . . 12  |-  ( a  =  x  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  x ) ) )
3635fveq2d 5891 . . . . . . . . . . 11  |-  ( a  =  x  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  x ) ) ) )
37 oveq2 6322 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  (
b  -  a )  =  ( b  -  x ) )
3837fveq2d 5891 . . . . . . . . . . . 12  |-  ( a  =  x  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  x ) ) )
3938oveq2d 6330 . . . . . . . . . . 11  |-  ( a  =  x  ->  (
k  x.  ( abs `  ( b  -  a
) ) )  =  ( k  x.  ( abs `  ( b  -  x ) ) ) )
4036, 39breq12d 4428 . . . . . . . . . 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 326 . . . . . . . . 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 4419 . . . . . . . . . 10  |-  ( b  =  y  ->  (
x  <  b  <->  x  <  y ) )
43 fveq2 5887 . . . . . . . . . . . . 13  |-  ( b  =  y  ->  ( F `  b )  =  ( F `  y ) )
4443oveq1d 6329 . . . . . . . . . . . 12  |-  ( b  =  y  ->  (
( F `  b
)  -  ( F `
 x ) )  =  ( ( F `
 y )  -  ( F `  x ) ) )
4544fveq2d 5891 . . . . . . . . . . 11  |-  ( b  =  y  ->  ( abs `  ( ( F `
 b )  -  ( F `  x ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
46 oveq1 6321 . . . . . . . . . . . . 13  |-  ( b  =  y  ->  (
b  -  x )  =  ( y  -  x ) )
4746fveq2d 5891 . . . . . . . . . . . 12  |-  ( b  =  y  ->  ( abs `  ( b  -  x ) )  =  ( abs `  (
y  -  x ) ) )
4847oveq2d 6330 . . . . . . . . . . 11  |-  ( b  =  y  ->  (
k  x.  ( abs `  ( b  -  x
) ) )  =  ( k  x.  ( abs `  ( y  -  x ) ) ) )
4945, 48breq12d 4428 . . . . . . . . . 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 326 . . . . . . . . 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 3170 . . . . . . . 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 738 . . . . . . 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 40 . . . . . . . 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 472 . . . . . . 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 45 . . . . . 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 10726 . . . . . . . . . 10  |-  0  <_  0
57 fvres 5901 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( A [,] B )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  =  ( F `  x
) )
5857ad2antrl 739 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  =  ( F `  x
) )
59 cncff 21973 . . . . . . . . . . . . . . . . . 18  |-  ( ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> RR )  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR )
6023, 59syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR )
6160ad2antrr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  ( F  |`  ( A [,] B ) ) : ( A [,] B
) --> RR )
62 simpl 463 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  ->  x  e.  ( A [,] B ) )
63 ffvelrn 6042 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR  /\  x  e.  ( A [,] B ) )  -> 
( ( F  |`  ( A [,] B ) ) `  x )  e.  RR )
6461, 62, 63syl2an 484 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 x )  e.  RR )
6558, 64eqeltrrd 2540 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  x )  e.  RR )
6665recnd 9694 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  x )  e.  CC )
6766subidd 9999 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F `  x
)  -  ( F `
 x ) )  =  0 )
6867abs00bd 13402 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( ( F `
 x )  -  ( F `  x ) ) )  =  0 )
69 iccssre 11744 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A [,] B
)  C_  RR )
704, 6, 69syl2anc 671 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A [,] B
)  C_  RR )
7170ad3antrrr 741 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( A [,] B )  C_  RR )
72 simprl 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  ( A [,] B
) )
7371, 72sseldd 3444 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  RR )
7473recnd 9694 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  x  e.  CC )
7574subidd 9999 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  -  x )  =  0 )
7675abs00bd 13402 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( x  -  x ) )  =  0 )
7776oveq2d 6330 . . . . . . . . . . . 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 767 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  k  e.  RR )
7978recnd 9694 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  k  e.  CC )
8079mul01d 9857 . . . . . . . . . . . 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 4428 . . . . . . . . . 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 241 . . . . . . . . 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 5887 . . . . . . . . . . . 12  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
8584oveq1d 6329 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( F `  x
)  -  ( F `
 x ) )  =  ( ( F `
 y )  -  ( F `  x ) ) )
8685fveq2d 5891 . . . . . . . . . 10  |-  ( x  =  y  ->  ( abs `  ( ( F `
 x )  -  ( F `  x ) ) )  =  ( abs `  ( ( F `  y )  -  ( F `  x ) ) ) )
87 oveq1 6321 . . . . . . . . . . . 12  |-  ( x  =  y  ->  (
x  -  x )  =  ( y  -  x ) )
8887fveq2d 5891 . . . . . . . . . . 11  |-  ( x  =  y  ->  ( abs `  ( x  -  x ) )  =  ( abs `  (
y  -  x ) ) )
8988oveq2d 6330 . . . . . . . . . 10  |-  ( x  =  y  ->  (
k  x.  ( abs `  ( x  -  x
) ) )  =  ( k  x.  ( abs `  ( y  -  x ) ) ) )
9086, 89breq12d 4428 . . . . . . . . 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 228 . . . . . . . 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 435 . . . . . . 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 26 . . . . . 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 4418 . . . . . . . . . . 11  |-  ( a  =  y  ->  (
a  <  b  <->  y  <  b ) )
95 fveq2 5887 . . . . . . . . . . . . . 14  |-  ( a  =  y  ->  ( F `  a )  =  ( F `  y ) )
9695oveq2d 6330 . . . . . . . . . . . . 13  |-  ( a  =  y  ->  (
( F `  b
)  -  ( F `
 a ) )  =  ( ( F `
 b )  -  ( F `  y ) ) )
9796fveq2d 5891 . . . . . . . . . . . 12  |-  ( a  =  y  ->  ( abs `  ( ( F `
 b )  -  ( F `  a ) ) )  =  ( abs `  ( ( F `  b )  -  ( F `  y ) ) ) )
98 oveq2 6322 . . . . . . . . . . . . . 14  |-  ( a  =  y  ->  (
b  -  a )  =  ( b  -  y ) )
9998fveq2d 5891 . . . . . . . . . . . . 13  |-  ( a  =  y  ->  ( abs `  ( b  -  a ) )  =  ( abs `  (
b  -  y ) ) )
10099oveq2d 6330 . . . . . . . . . . . 12  |-  ( a  =  y  ->  (
k  x.  ( abs `  ( b  -  a
) ) )  =  ( k  x.  ( abs `  ( b  -  y ) ) ) )
10197, 100breq12d 4428 . . . . . . . . . . 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 326 . . . . . . . . . 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 4419 . . . . . . . . . . 11  |-  ( b  =  x  ->  (
y  <  b  <->  y  <  x ) )
104 fveq2 5887 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  ( F `  b )  =  ( F `  x ) )
105104oveq1d 6329 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  (
( F `  b
)  -  ( F `
 y ) )  =  ( ( F `
 x )  -  ( F `  y ) ) )
106105fveq2d 5891 . . . . . . . . . . . 12  |-  ( b  =  x  ->  ( abs `  ( ( F `
 b )  -  ( F `  y ) ) )  =  ( abs `  ( ( F `  x )  -  ( F `  y ) ) ) )
107 oveq1 6321 . . . . . . . . . . . . . 14  |-  ( b  =  x  ->  (
b  -  y )  =  ( x  -  y ) )
108107fveq2d 5891 . . . . . . . . . . . . 13  |-  ( b  =  x  ->  ( abs `  ( b  -  y ) )  =  ( abs `  (
x  -  y ) ) )
109108oveq2d 6330 . . . . . . . . . . . 12  |-  ( b  =  x  ->  (
k  x.  ( abs `  ( b  -  y
) ) )  =  ( k  x.  ( abs `  ( x  -  y ) ) ) )
110106, 109breq12d 4428 . . . . . . . . . . 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 326 . . . . . . . . . 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 3170 . . . . . . . . 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 459 . . . . . . . 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 738 . . . . . . 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 467 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  y  <  x )
116 fvres 5901 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( A [,] B )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  =  ( F `  y
) )
117116ad2antll 740 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  =  ( F `  y
) )
118 simpr 467 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  -> 
y  e.  ( A [,] B ) )
119 ffvelrn 6042 . . . . . . . . . . . . . . 15  |-  ( ( ( F  |`  ( A [,] B ) ) : ( A [,] B ) --> RR  /\  y  e.  ( A [,] B ) )  -> 
( ( F  |`  ( A [,] B ) ) `  y )  e.  RR )
12061, 118, 119syl2an 484 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
( F  |`  ( A [,] B ) ) `
 y )  e.  RR )
121117, 120eqeltrrd 2540 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  y )  e.  RR )
122121recnd 9694 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( F `  y )  e.  CC )
12366, 122abssubd 13563 . . . . . . . . . . 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 471 . . . . . . . . . 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 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  ( A [,] B )  C_  RR )
126125sseld 3442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
x  e.  ( A [,] B )  ->  x  e.  RR )
)
127125sseld 3442 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
y  e.  ( A [,] B )  -> 
y  e.  RR ) )
128126, 127anim12d 570 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  ->  (
( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) )  ->  ( x  e.  RR  /\  y  e.  RR ) ) )
129128imp 435 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  (
x  e.  RR  /\  y  e.  RR )
)
130 recn 9654 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  ->  x  e.  CC )
131 recn 9654 . . . . . . . . . . . . . 14  |-  ( y  e.  RR  ->  y  e.  CC )
132 abssub 13437 . . . . . . . . . . . . . 14  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( abs `  (
x  -  y ) )  =  ( abs `  ( y  -  x
) ) )
133130, 131, 132syl2an 484 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( abs `  (
x  -  y ) )  =  ( abs `  ( y  -  x
) ) )
134129, 133syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B )  /\  y  e.  ( A [,] B ) ) )  ->  ( abs `  ( x  -  y ) )  =  ( abs `  (
y  -  x ) ) )
135134adantr 471 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  A  <_  B )  /\  k  e.  RR )  /\  ( x  e.  ( A [,] B
)  /\  y  e.  ( A [,] B ) ) )  /\  y  <  x )  ->  ( abs `  ( x  -  y ) )  =  ( abs `  (
y  -  x ) ) )
136135oveq2d 6330 . . . . . . . . . 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 4428 . . . . . . . . 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 212 . . . . . . . 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 56 . . . . . . 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 45 . . . . . 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 9743 . . . . . . 7  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  <  y  \/  x  =  y  \/  y  <  x ) )
142129, 141syl 17 . . . . . 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 1344 . . . . 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 2823 . . . 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 2873 . . 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 9767 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 189    /\ wa 375    \/ w3o 990    = wceq 1454    e. wcel 1897    =/= wne 2632   A.wral 2748   E.wrex 2749    C_ wss 3415   (/)c0 3742   class class class wbr 4415    |` cres 4854   "cima 4855   -->wf 5596   ` cfv 5600  (class class class)co 6314    ^pm cpm 7498   supcsup 7979   CCcc 9562   RRcr 9563   0cc0 9564    x. cmul 9569   RR*cxr 9699    < clt 9700    <_ cle 9701    - cmin 9885   [,]cicc 11666   abscabs 13345   -cn->ccncf 21956    _D cdv 22866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-inf2 8171  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642  ax-addf 9643  ax-mulf 9644
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-iin 4294  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-of 6557  df-om 6719  df-1st 6819  df-2nd 6820  df-supp 6941  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-2o 7208  df-oadd 7211  df-er 7388  df-map 7499  df-pm 7500  df-ixp 7548  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-fsupp 7909  df-fi 7950  df-sup 7981  df-inf 7982  df-oi 8050  df-card 8398  df-cda 8623  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-4 10697  df-5 10698  df-6 10699  df-7 10700  df-8 10701  df-9 10702  df-10 10703  df-n0 10898  df-z 10966  df-dec 11080  df-uz 11188  df-q 11293  df-rp 11331  df-xneg 11437  df-xadd 11438  df-xmul 11439  df-ioo 11667  df-ico 11669  df-icc 11670  df-fz 11813  df-fzo 11946  df-seq 12245  df-exp 12304  df-hash 12547  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-struct 15171  df-ndx 15172  df-slot 15173  df-base 15174  df-sets 15175  df-ress 15176  df-plusg 15251  df-mulr 15252  df-starv 15253  df-sca 15254  df-vsca 15255  df-ip 15256  df-tset 15257  df-ple 15258  df-ds 15260  df-unif 15261  df-hom 15262  df-cco 15263  df-rest 15369  df-topn 15370  df-0g 15388  df-gsum 15389  df-topgen 15390  df-pt 15391  df-prds 15394  df-xrs 15448  df-qtop 15454  df-imas 15455  df-xps 15458  df-mre 15540  df-mrc 15541  df-acs 15543  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-submnd 16631  df-mulg 16724  df-cntz 17019  df-cmn 17480  df-psmet 19010  df-xmet 19011  df-met 19012  df-bl 19013  df-mopn 19014  df-fbas 19015  df-fg 19016  df-cnfld 19019  df-top 19969  df-bases 19970  df-topon 19971  df-topsp 19972  df-cld 20082  df-ntr 20083  df-cls 20084  df-nei 20162  df-lp 20200  df-perf 20201  df-cn 20291  df-cnp 20292  df-haus 20379  df-cmp 20450  df-tx 20625  df-hmeo 20818  df-fil 20909  df-fm 21001  df-flim 21002  df-flf 21003  df-xms 21383  df-ms 21384  df-tms 21385  df-cncf 21958  df-limc 22869  df-dv 22870
This theorem is referenced by:  c1lip2  22998
  Copyright terms: Public domain W3C validator