Metamath Proof Explorer

Theorem c1lip2

Description: C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses c1lip2.a 
|- ( ph -> A e. RR )
c1lip2.b 
|- ( ph -> B e. RR )
c1lip2.f 
|- ( ph -> F e. ( ( C^n ` RR ) ` 1 ) )
c1lip2.rn 
|- ( ph -> ran F C_ RR )
c1lip2.dm 
|- ( ph -> ( A [,] B ) C_ dom F )
Assertion c1lip2 
|- ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 c1lip2.a 
 |-  ( ph -> A e. RR )
2 c1lip2.b 
 |-  ( ph -> B e. RR )
3 c1lip2.f 
 |-  ( ph -> F e. ( ( C^n ` RR ) ` 1 ) )
4 c1lip2.rn 
 |-  ( ph -> ran F C_ RR )
5 c1lip2.dm 
 |-  ( ph -> ( A [,] B ) C_ dom F )
6 ax-resscn 
 |-  RR C_ CC
7 1nn0 
 |-  1 e. NN0
8 elcpn 
 |-  ( ( RR C_ CC /\ 1 e. NN0 ) -> ( F e. ( ( C^n ` RR ) ` 1 ) <-> ( F e. ( CC ^pm RR ) /\ ( ( RR Dn F ) ` 1 ) e. ( dom F -cn-> CC ) ) ) )
9 6 7 8 mp2an 
 |-  ( F e. ( ( C^n ` RR ) ` 1 ) <-> ( F e. ( CC ^pm RR ) /\ ( ( RR Dn F ) ` 1 ) e. ( dom F -cn-> CC ) ) )
10 9 simplbi 
 |-  ( F e. ( ( C^n ` RR ) ` 1 ) -> F e. ( CC ^pm RR ) )
11 3 10 syl 
 |-  ( ph -> F e. ( CC ^pm RR ) )
12 pmfun 
 |-  ( F e. ( CC ^pm RR ) -> Fun F )
13 11 12 syl 
 |-  ( ph -> Fun F )
14 13 funfnd 
 |-  ( ph -> F Fn dom F )
15 df-f 
 |-  ( F : dom F --> RR <-> ( F Fn dom F /\ ran F C_ RR ) )
16 14 4 15 sylanbrc 
 |-  ( ph -> F : dom F --> RR )
17 cnex 
 |-  CC e. _V
18 reex 
 |-  RR e. _V
19 17 18 elpm2 
 |-  ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
20 19 simprbi 
 |-  ( F e. ( CC ^pm RR ) -> dom F C_ RR )
21 11 20 syl 
 |-  ( ph -> dom F C_ RR )
22 dvfre 
 |-  ( ( F : dom F --> RR /\ dom F C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
23 16 21 22 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
24 0p1e1 
 |-  ( 0 + 1 ) = 1
25 24 fveq2i 
 |-  ( ( RR Dn F ) ` ( 0 + 1 ) ) = ( ( RR Dn F ) ` 1 )
26 0nn0 
 |-  0 e. NN0
27 dvnp1 
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) /\ 0 e. NN0 ) -> ( ( RR Dn F ) ` ( 0 + 1 ) ) = ( RR _D ( ( RR Dn F ) ` 0 ) ) )
28 6 26 27 mp3an13 
 |-  ( F e. ( CC ^pm RR ) -> ( ( RR Dn F ) ` ( 0 + 1 ) ) = ( RR _D ( ( RR Dn F ) ` 0 ) ) )
29 11 28 syl 
 |-  ( ph -> ( ( RR Dn F ) ` ( 0 + 1 ) ) = ( RR _D ( ( RR Dn F ) ` 0 ) ) )
30 25 29 syl5eqr 
 |-  ( ph -> ( ( RR Dn F ) ` 1 ) = ( RR _D ( ( RR Dn F ) ` 0 ) ) )
31 dvn0 
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) ) -> ( ( RR Dn F ) ` 0 ) = F )
32 6 11 31 sylancr 
 |-  ( ph -> ( ( RR Dn F ) ` 0 ) = F )
33 32 oveq2d 
 |-  ( ph -> ( RR _D ( ( RR Dn F ) ` 0 ) ) = ( RR _D F ) )
34 30 33 eqtrd 
 |-  ( ph -> ( ( RR Dn F ) ` 1 ) = ( RR _D F ) )
35 9 simprbi 
 |-  ( F e. ( ( C^n ` RR ) ` 1 ) -> ( ( RR Dn F ) ` 1 ) e. ( dom F -cn-> CC ) )
36 3 35 syl 
 |-  ( ph -> ( ( RR Dn F ) ` 1 ) e. ( dom F -cn-> CC ) )
37 34 36 eqeltrrd 
 |-  ( ph -> ( RR _D F ) e. ( dom F -cn-> CC ) )
38 cncff 
 |-  ( ( RR _D F ) e. ( dom F -cn-> CC ) -> ( RR _D F ) : dom F --> CC )
39 fdm 
 |-  ( ( RR _D F ) : dom F --> CC -> dom ( RR _D F ) = dom F )
40 37 38 39 3syl 
 |-  ( ph -> dom ( RR _D F ) = dom F )
41 40 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom F --> RR ) )
42 23 41 mpbid 
 |-  ( ph -> ( RR _D F ) : dom F --> RR )
43 cncffvrn 
 |-  ( ( RR C_ CC /\ ( RR _D F ) e. ( dom F -cn-> CC ) ) -> ( ( RR _D F ) e. ( dom F -cn-> RR ) <-> ( RR _D F ) : dom F --> RR ) )
44 6 37 43 sylancr 
 |-  ( ph -> ( ( RR _D F ) e. ( dom F -cn-> RR ) <-> ( RR _D F ) : dom F --> RR ) )
45 42 44 mpbird 
 |-  ( ph -> ( RR _D F ) e. ( dom F -cn-> RR ) )
46 rescncf 
 |-  ( ( A [,] B ) C_ dom F -> ( ( RR _D F ) e. ( dom F -cn-> RR ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) ) )
47 5 45 46 sylc 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
48 18 prid1 
 |-  RR e. { RR , CC }
49 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
50 cpnord 
 |-  ( ( RR e. { RR , CC } /\ 0 e. NN0 /\ 1 e. ( ZZ>= ` 0 ) ) -> ( ( C^n ` RR ) ` 1 ) C_ ( ( C^n ` RR ) ` 0 ) )
51 48 26 49 50 mp3an 
 |-  ( ( C^n ` RR ) ` 1 ) C_ ( ( C^n ` RR ) ` 0 )
52 51 3 sseldi 
 |-  ( ph -> F e. ( ( C^n ` RR ) ` 0 ) )
53 elcpn 
 |-  ( ( RR C_ CC /\ 0 e. NN0 ) -> ( F e. ( ( C^n ` RR ) ` 0 ) <-> ( F e. ( CC ^pm RR ) /\ ( ( RR Dn F ) ` 0 ) e. ( dom F -cn-> CC ) ) ) )
54 6 26 53 mp2an 
 |-  ( F e. ( ( C^n ` RR ) ` 0 ) <-> ( F e. ( CC ^pm RR ) /\ ( ( RR Dn F ) ` 0 ) e. ( dom F -cn-> CC ) ) )
55 54 simprbi 
 |-  ( F e. ( ( C^n ` RR ) ` 0 ) -> ( ( RR Dn F ) ` 0 ) e. ( dom F -cn-> CC ) )
56 52 55 syl 
 |-  ( ph -> ( ( RR Dn F ) ` 0 ) e. ( dom F -cn-> CC ) )
57 32 56 eqeltrrd 
 |-  ( ph -> F e. ( dom F -cn-> CC ) )
58 cncffvrn 
 |-  ( ( RR C_ CC /\ F e. ( dom F -cn-> CC ) ) -> ( F e. ( dom F -cn-> RR ) <-> F : dom F --> RR ) )
59 6 57 58 sylancr 
 |-  ( ph -> ( F e. ( dom F -cn-> RR ) <-> F : dom F --> RR ) )
60 16 59 mpbird 
 |-  ( ph -> F e. ( dom F -cn-> RR ) )
61 rescncf 
 |-  ( ( A [,] B ) C_ dom F -> ( F e. ( dom F -cn-> RR ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) ) )
62 5 60 61 sylc 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
63 1 2 11 47 62 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 ) ) ) )