Step |
Hyp |
Ref |
Expression |
1 |
|
ovolfs.1 |
|- G = ( ( abs o. - ) o. F ) |
2 |
|
absf |
|- abs : CC --> RR |
3 |
|
subf |
|- - : ( CC X. CC ) --> CC |
4 |
|
fco |
|- ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR ) |
5 |
2 3 4
|
mp2an |
|- ( abs o. - ) : ( CC X. CC ) --> RR |
6 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
7 |
|
ax-resscn |
|- RR C_ CC |
8 |
|
xpss12 |
|- ( ( RR C_ CC /\ RR C_ CC ) -> ( RR X. RR ) C_ ( CC X. CC ) ) |
9 |
7 7 8
|
mp2an |
|- ( RR X. RR ) C_ ( CC X. CC ) |
10 |
6 9
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( CC X. CC ) |
11 |
|
fss |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( CC X. CC ) ) -> F : NN --> ( CC X. CC ) ) |
12 |
10 11
|
mpan2 |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F : NN --> ( CC X. CC ) ) |
13 |
|
fco |
|- ( ( ( abs o. - ) : ( CC X. CC ) --> RR /\ F : NN --> ( CC X. CC ) ) -> ( ( abs o. - ) o. F ) : NN --> RR ) |
14 |
5 12 13
|
sylancr |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. F ) : NN --> RR ) |
15 |
1
|
feq1i |
|- ( G : NN --> RR <-> ( ( abs o. - ) o. F ) : NN --> RR ) |
16 |
14 15
|
sylibr |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> RR ) |
17 |
16
|
ffnd |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G Fn NN ) |
18 |
16
|
ffvelrnda |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) e. RR ) |
19 |
|
ovolfcl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) ) |
20 |
|
subge0 |
|- ( ( ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) e. RR ) -> ( 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) <-> ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) ) |
21 |
20
|
ancoms |
|- ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR ) -> ( 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) <-> ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) ) |
22 |
21
|
biimp3ar |
|- ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) -> 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) ) |
23 |
19 22
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> 0 <_ ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) ) |
24 |
1
|
ovolfsval |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) ) |
25 |
23 24
|
breqtrrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> 0 <_ ( G ` x ) ) |
26 |
|
elrege0 |
|- ( ( G ` x ) e. ( 0 [,) +oo ) <-> ( ( G ` x ) e. RR /\ 0 <_ ( G ` x ) ) ) |
27 |
18 25 26
|
sylanbrc |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( G ` x ) e. ( 0 [,) +oo ) ) |
28 |
27
|
ralrimiva |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. x e. NN ( G ` x ) e. ( 0 [,) +oo ) ) |
29 |
|
ffnfv |
|- ( G : NN --> ( 0 [,) +oo ) <-> ( G Fn NN /\ A. x e. NN ( G ` x ) e. ( 0 [,) +oo ) ) ) |
30 |
17 28 29
|
sylanbrc |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> G : NN --> ( 0 [,) +oo ) ) |