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 ) ) ) ) |