Metamath Proof Explorer

Theorem rlimclim1

Description: Forward direction of rlimclim . (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Hypotheses rlimclim1.1 
|- Z = ( ZZ>= ` M )
rlimclim1.2 
|- ( ph -> M e. ZZ )
rlimclim1.3 
|- ( ph -> F ~~>r A )
rlimclim1.4 
|- ( ph -> Z C_ dom F )
Assertion rlimclim1 
|- ( ph -> F ~~> A )

Proof

Step Hyp Ref Expression
1 rlimclim1.1 
 |-  Z = ( ZZ>= ` M )
2 rlimclim1.2 
 |-  ( ph -> M e. ZZ )
3 rlimclim1.3 
 |-  ( ph -> F ~~>r A )
4 rlimclim1.4 
 |-  ( ph -> Z C_ dom F )
5 fvex 
 |-  ( F ` w ) e. _V
6 5 rgenw 
 |-  A. w e. dom F ( F ` w ) e. _V
7 6 a1i 
 |-  ( ( ph /\ y e. RR+ ) -> A. w e. dom F ( F ` w ) e. _V )
8 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
9 rlimf 
 |-  ( F ~~>r A -> F : dom F --> CC )
10 3 9 syl 
 |-  ( ph -> F : dom F --> CC )
11 10 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F : dom F --> CC )
12 11 feqmptd 
 |-  ( ( ph /\ y e. RR+ ) -> F = ( w e. dom F |-> ( F ` w ) ) )
13 3 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F ~~>r A )
14 12 13 eqbrtrrd 
 |-  ( ( ph /\ y e. RR+ ) -> ( w e. dom F |-> ( F ` w ) ) ~~>r A )
15 7 8 14 rlimi 
 |-  ( ( ph /\ y e. RR+ ) -> E. z e. RR A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
16 2 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> M e. ZZ )
17 flcl 
 |-  ( z e. RR -> ( |_ ` z ) e. ZZ )
18 17 peano2zd 
 |-  ( z e. RR -> ( ( |_ ` z ) + 1 ) e. ZZ )
19 18 ad2antrl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> ( ( |_ ` z ) + 1 ) e. ZZ )
20 19 16 ifcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. ZZ )
21 16 zred 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> M e. RR )
22 19 zred 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> ( ( |_ ` z ) + 1 ) e. RR )
23 max1 
 |-  ( ( M e. RR /\ ( ( |_ ` z ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) )
24 21 22 23 syl2anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> M <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) )
25 eluz2 
 |-  ( if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. ZZ /\ M <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) )
26 16 20 24 25 syl3anbrc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. ( ZZ>= ` M ) )
27 26 1 eleqtrrdi 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. Z )
28 simplrl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> z e. RR )
29 18 zred 
 |-  ( z e. RR -> ( ( |_ ` z ) + 1 ) e. RR )
30 28 29 syl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> ( ( |_ ` z ) + 1 ) e. RR )
31 21 adantr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> M e. RR )
32 30 31 ifcld 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. RR )
33 eluzelre 
 |-  ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) -> k e. RR )
34 33 adantl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> k e. RR )
35 fllep1 
 |-  ( z e. RR -> z <_ ( ( |_ ` z ) + 1 ) )
36 28 35 syl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> z <_ ( ( |_ ` z ) + 1 ) )
37 max2 
 |-  ( ( M e. RR /\ ( ( |_ ` z ) + 1 ) e. RR ) -> ( ( |_ ` z ) + 1 ) <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) )
38 31 30 37 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> ( ( |_ ` z ) + 1 ) <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) )
39 28 30 32 36 38 letrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> z <_ if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) )
40 eluzle 
 |-  ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) <_ k )
41 40 adantl 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) <_ k )
42 28 32 34 39 41 letrd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> z <_ k )
43 breq2 
 |-  ( w = k -> ( z <_ w <-> z <_ k ) )
44 43 imbrov2fvoveq 
 |-  ( w = k -> ( ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) <-> ( z <_ k -> ( abs ` ( ( F ` k ) - A ) ) < y ) ) )
45 simplrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) )
46 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> Z C_ dom F )
47 1 uztrn2 
 |-  ( ( if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. Z /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> k e. Z )
48 27 47 sylan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> k e. Z )
49 46 48 sseldd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> k e. dom F )
50 44 45 49 rspcdva 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> ( z <_ k -> ( abs ` ( ( F ` k ) - A ) ) < y ) )
51 42 50 mpd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ) -> ( abs ` ( ( F ` k ) - A ) ) < y )
52 51 ralrimiva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ( abs ` ( ( F ` k ) - A ) ) < y )
53 fveq2 
 |-  ( j = if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) -> ( ZZ>= ` j ) = ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) )
54 53 raleqdv 
 |-  ( j = if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y <-> A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ( abs ` ( ( F ` k ) - A ) ) < y ) )
55 54 rspcev 
 |-  ( ( if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) e. Z /\ A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` z ) + 1 ) , ( ( |_ ` z ) + 1 ) , M ) ) ( abs ` ( ( F ` k ) - A ) ) < y ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y )
56 27 52 55 syl2anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( z e. RR /\ A. w e. dom F ( z <_ w -> ( abs ` ( ( F ` w ) - A ) ) < y ) ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y )
57 15 56 rexlimddv 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y )
58 57 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y )
59 rlimpm 
 |-  ( F ~~>r A -> F e. ( CC ^pm RR ) )
60 3 59 syl 
 |-  ( ph -> F e. ( CC ^pm RR ) )
61 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
62 rlimcl 
 |-  ( F ~~>r A -> A e. CC )
63 3 62 syl 
 |-  ( ph -> A e. CC )
64 4 sselda 
 |-  ( ( ph /\ k e. Z ) -> k e. dom F )
65 10 ffvelrnda 
 |-  ( ( ph /\ k e. dom F ) -> ( F ` k ) e. CC )
66 64 65 syldan 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
67 1 2 60 61 63 66 clim2c 
 |-  ( ph -> ( F ~~> A <-> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < y ) )
68 58 67 mpbird 
 |-  ( ph -> F ~~> A )