Step |
Hyp |
Ref |
Expression |
1 |
|
rlimuni.1 |
|- ( ph -> F : A --> CC ) |
2 |
|
rlimuni.2 |
|- ( ph -> sup ( A , RR* , < ) = +oo ) |
3 |
|
rlimuni.3 |
|- ( ph -> F ~~>r B ) |
4 |
|
rlimuni.4 |
|- ( ph -> F ~~>r C ) |
5 |
|
rlimcl |
|- ( F ~~>r B -> B e. CC ) |
6 |
3 5
|
syl |
|- ( ph -> B e. CC ) |
7 |
6
|
ad2antrr |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> B e. CC ) |
8 |
|
rlimcl |
|- ( F ~~>r C -> C e. CC ) |
9 |
4 8
|
syl |
|- ( ph -> C e. CC ) |
10 |
9
|
ad2antrr |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> C e. CC ) |
11 |
7 10
|
subcld |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( B - C ) e. CC ) |
12 |
11
|
abscld |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( abs ` ( B - C ) ) e. RR ) |
13 |
12
|
ltnrd |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> -. ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) |
14 |
1
|
ffvelrnda |
|- ( ( ph /\ k e. A ) -> ( F ` k ) e. CC ) |
15 |
14
|
adantlr |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( F ` k ) e. CC ) |
16 |
15 7
|
abssubd |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( abs ` ( ( F ` k ) - B ) ) = ( abs ` ( B - ( F ` k ) ) ) ) |
17 |
16
|
breq1d |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) <-> ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) |
18 |
17
|
anbi1d |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) <-> ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) |
19 |
|
abs3lem |
|- ( ( ( B e. CC /\ C e. CC ) /\ ( ( F ` k ) e. CC /\ ( abs ` ( B - C ) ) e. RR ) ) -> ( ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) |
20 |
7 10 15 12 19
|
syl22anc |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( B - ( F ` k ) ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) |
21 |
18 20
|
sylbid |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) |
22 |
21
|
imim2d |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> ( j <_ k -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) ) |
23 |
22
|
impcomd |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> ( abs ` ( B - C ) ) < ( abs ` ( B - C ) ) ) ) |
24 |
13 23
|
mtod |
|- ( ( ( ph /\ j e. RR ) /\ k e. A ) -> -. ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
25 |
24
|
nrexdv |
|- ( ( ph /\ j e. RR ) -> -. E. k e. A ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
26 |
|
r19.29r |
|- ( ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> E. k e. A ( j <_ k /\ ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
27 |
25 26
|
nsyl |
|- ( ( ph /\ j e. RR ) -> -. ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
28 |
27
|
nrexdv |
|- ( ph -> -. E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
29 |
1
|
fdmd |
|- ( ph -> dom F = A ) |
30 |
|
rlimss |
|- ( F ~~>r B -> dom F C_ RR ) |
31 |
3 30
|
syl |
|- ( ph -> dom F C_ RR ) |
32 |
29 31
|
eqsstrrd |
|- ( ph -> A C_ RR ) |
33 |
|
ressxr |
|- RR C_ RR* |
34 |
32 33
|
sstrdi |
|- ( ph -> A C_ RR* ) |
35 |
|
supxrunb1 |
|- ( A C_ RR* -> ( A. j e. RR E. k e. A j <_ k <-> sup ( A , RR* , < ) = +oo ) ) |
36 |
34 35
|
syl |
|- ( ph -> ( A. j e. RR E. k e. A j <_ k <-> sup ( A , RR* , < ) = +oo ) ) |
37 |
2 36
|
mpbird |
|- ( ph -> A. j e. RR E. k e. A j <_ k ) |
38 |
|
r19.29 |
|- ( ( A. j e. RR E. k e. A j <_ k /\ E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
39 |
38
|
ex |
|- ( A. j e. RR E. k e. A j <_ k -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) ) |
40 |
37 39
|
syl |
|- ( ph -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> E. j e. RR ( E. k e. A j <_ k /\ A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) ) |
41 |
28 40
|
mtod |
|- ( ph -> -. E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) |
42 |
1
|
adantr |
|- ( ( ph /\ B =/= C ) -> F : A --> CC ) |
43 |
|
ffvelrn |
|- ( ( F : A --> CC /\ k e. A ) -> ( F ` k ) e. CC ) |
44 |
43
|
ralrimiva |
|- ( F : A --> CC -> A. k e. A ( F ` k ) e. CC ) |
45 |
42 44
|
syl |
|- ( ( ph /\ B =/= C ) -> A. k e. A ( F ` k ) e. CC ) |
46 |
6
|
adantr |
|- ( ( ph /\ B =/= C ) -> B e. CC ) |
47 |
9
|
adantr |
|- ( ( ph /\ B =/= C ) -> C e. CC ) |
48 |
46 47
|
subcld |
|- ( ( ph /\ B =/= C ) -> ( B - C ) e. CC ) |
49 |
|
simpr |
|- ( ( ph /\ B =/= C ) -> B =/= C ) |
50 |
46 47 49
|
subne0d |
|- ( ( ph /\ B =/= C ) -> ( B - C ) =/= 0 ) |
51 |
48 50
|
absrpcld |
|- ( ( ph /\ B =/= C ) -> ( abs ` ( B - C ) ) e. RR+ ) |
52 |
51
|
rphalfcld |
|- ( ( ph /\ B =/= C ) -> ( ( abs ` ( B - C ) ) / 2 ) e. RR+ ) |
53 |
42
|
feqmptd |
|- ( ( ph /\ B =/= C ) -> F = ( k e. A |-> ( F ` k ) ) ) |
54 |
3
|
adantr |
|- ( ( ph /\ B =/= C ) -> F ~~>r B ) |
55 |
53 54
|
eqbrtrrd |
|- ( ( ph /\ B =/= C ) -> ( k e. A |-> ( F ` k ) ) ~~>r B ) |
56 |
45 52 55
|
rlimi |
|- ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) |
57 |
4
|
adantr |
|- ( ( ph /\ B =/= C ) -> F ~~>r C ) |
58 |
53 57
|
eqbrtrrd |
|- ( ( ph /\ B =/= C ) -> ( k e. A |-> ( F ` k ) ) ~~>r C ) |
59 |
45 52 58
|
rlimi |
|- ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) |
60 |
32
|
adantr |
|- ( ( ph /\ B =/= C ) -> A C_ RR ) |
61 |
|
rexanre |
|- ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) /\ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
62 |
60 61
|
syl |
|- ( ( ph /\ B =/= C ) -> ( E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) /\ E. j e. RR A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
63 |
56 59 62
|
mpbir2and |
|- ( ( ph /\ B =/= C ) -> E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) |
64 |
63
|
ex |
|- ( ph -> ( B =/= C -> E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) ) ) |
65 |
64
|
necon1bd |
|- ( ph -> ( -. E. j e. RR A. k e. A ( j <_ k -> ( ( abs ` ( ( F ` k ) - B ) ) < ( ( abs ` ( B - C ) ) / 2 ) /\ ( abs ` ( ( F ` k ) - C ) ) < ( ( abs ` ( B - C ) ) / 2 ) ) ) -> B = C ) ) |
66 |
41 65
|
mpd |
|- ( ph -> B = C ) |