Step |
Hyp |
Ref |
Expression |
1 |
|
rlim2.1 |
|- ( ph -> A. z e. A B e. CC ) |
2 |
|
rlim2.2 |
|- ( ph -> A C_ RR ) |
3 |
|
rlim2.3 |
|- ( ph -> C e. CC ) |
4 |
1 2 3
|
rlim2 |
|- ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
5 |
|
simplr |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> y e. RR ) |
6 |
|
simpl |
|- ( ( A C_ RR /\ y e. RR ) -> A C_ RR ) |
7 |
6
|
sselda |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> z e. RR ) |
8 |
|
ltle |
|- ( ( y e. RR /\ z e. RR ) -> ( y < z -> y <_ z ) ) |
9 |
5 7 8
|
syl2anc |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y < z -> y <_ z ) ) |
10 |
9
|
imim1d |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
11 |
10
|
ralimdva |
|- ( ( A C_ RR /\ y e. RR ) -> ( A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
12 |
2 11
|
sylan |
|- ( ( ph /\ y e. RR ) -> ( A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
13 |
12
|
reximdva |
|- ( ph -> ( E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
14 |
13
|
ralimdv |
|- ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) -> A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
15 |
4 14
|
sylbid |
|- ( ph -> ( ( z e. A |-> B ) ~~>r C -> A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |
16 |
|
peano2re |
|- ( y e. RR -> ( y + 1 ) e. RR ) |
17 |
16
|
adantl |
|- ( ( ph /\ y e. RR ) -> ( y + 1 ) e. RR ) |
18 |
|
ltp1 |
|- ( y e. RR -> y < ( y + 1 ) ) |
19 |
18
|
ad2antlr |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> y < ( y + 1 ) ) |
20 |
16
|
ad2antlr |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( y + 1 ) e. RR ) |
21 |
|
ltletr |
|- ( ( y e. RR /\ ( y + 1 ) e. RR /\ z e. RR ) -> ( ( y < ( y + 1 ) /\ ( y + 1 ) <_ z ) -> y < z ) ) |
22 |
5 20 7 21
|
syl3anc |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y < ( y + 1 ) /\ ( y + 1 ) <_ z ) -> y < z ) ) |
23 |
19 22
|
mpand |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y + 1 ) <_ z -> y < z ) ) |
24 |
23
|
imim1d |
|- ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( ( y < z -> ( abs ` ( B - C ) ) < x ) -> ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
25 |
24
|
ralimdva |
|- ( ( A C_ RR /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
26 |
2 25
|
sylan |
|- ( ( ph /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
27 |
|
breq1 |
|- ( w = ( y + 1 ) -> ( w <_ z <-> ( y + 1 ) <_ z ) ) |
28 |
27
|
rspceaimv |
|- ( ( ( y + 1 ) e. RR /\ A. z e. A ( ( y + 1 ) <_ z -> ( abs ` ( B - C ) ) < x ) ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) |
29 |
17 26 28
|
syl6an |
|- ( ( ph /\ y e. RR ) -> ( A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
30 |
29
|
rexlimdva |
|- ( ph -> ( E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
31 |
30
|
ralimdv |
|- ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> A. x e. RR+ E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
32 |
1 2 3
|
rlim2 |
|- ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. w e. RR A. z e. A ( w <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
33 |
31 32
|
sylibrd |
|- ( ph -> ( A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) -> ( z e. A |-> B ) ~~>r C ) ) |
34 |
15 33
|
impbid |
|- ( ph -> ( ( z e. A |-> B ) ~~>r C <-> A. x e. RR+ E. y e. RR A. z e. A ( y < z -> ( abs ` ( B - C ) ) < x ) ) ) |