Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
|- 0 e. RR |
2 |
|
ral0 |
|- A. y e. (/) ( abs ` ( F ` y ) ) <_ 0 |
3 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> A e. RR ) |
4 |
3
|
rexrd |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> A e. RR* ) |
5 |
|
simp2 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> B e. RR ) |
6 |
5
|
rexrd |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> B e. RR* ) |
7 |
|
icc0 |
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) ) |
8 |
4 6 7
|
syl2anc |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( A [,] B ) = (/) <-> B < A ) ) |
9 |
8
|
biimpar |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> ( A [,] B ) = (/) ) |
10 |
9
|
raleqdv |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> ( A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 <-> A. y e. (/) ( abs ` ( F ` y ) ) <_ 0 ) ) |
11 |
2 10
|
mpbiri |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 ) |
12 |
|
brralrspcev |
|- ( ( 0 e. RR /\ A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ 0 ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
13 |
1 11 12
|
sylancr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ B < A ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
14 |
3
|
adantr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> A e. RR ) |
15 |
5
|
adantr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> B e. RR ) |
16 |
|
simpr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> A <_ B ) |
17 |
|
simp3 |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. ( ( A [,] B ) -cn-> CC ) ) |
18 |
|
abscncf |
|- abs e. ( CC -cn-> RR ) |
19 |
18
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> abs e. ( CC -cn-> RR ) ) |
20 |
17 19
|
cncfco |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) ) |
21 |
20
|
adantr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) ) |
22 |
14 15 16 21
|
evthicc |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> ( E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) /\ E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` z ) <_ ( ( abs o. F ) ` y ) ) ) |
23 |
22
|
simpld |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) ) |
24 |
|
cncff |
|- ( ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) -> ( abs o. F ) : ( A [,] B ) --> RR ) |
25 |
20 24
|
syl |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( abs o. F ) : ( A [,] B ) --> RR ) |
26 |
25
|
ffvelrnda |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( ( abs o. F ) ` z ) e. RR ) |
27 |
|
cncff |
|- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC ) |
28 |
17 27
|
syl |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F : ( A [,] B ) --> CC ) |
29 |
28
|
adantr |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> F : ( A [,] B ) --> CC ) |
30 |
|
fvco3 |
|- ( ( F : ( A [,] B ) --> CC /\ y e. ( A [,] B ) ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) ) |
31 |
29 30
|
sylan |
|- ( ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) ) |
32 |
31
|
breq1d |
|- ( ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) /\ y e. ( A [,] B ) ) -> ( ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) <-> ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) ) |
33 |
32
|
ralbidva |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) <-> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) ) |
34 |
33
|
biimpd |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) ) |
35 |
|
brralrspcev |
|- ( ( ( ( abs o. F ) ` z ) e. RR /\ A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( ( abs o. F ) ` z ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
36 |
26 34 35
|
syl6an |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ z e. ( A [,] B ) ) -> ( A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) ) |
37 |
36
|
rexlimdva |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> ( E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) ) |
38 |
37
|
imp |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ E. z e. ( A [,] B ) A. y e. ( A [,] B ) ( ( abs o. F ) ` y ) <_ ( ( abs o. F ) ` z ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
39 |
23 38
|
syldan |
|- ( ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) /\ A <_ B ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |
40 |
13 39 5 3
|
ltlecasei |
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ x ) |