Metamath Proof Explorer

Theorem climcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climcn1.1 
|- Z = ( ZZ>= ` M )
climcn1.2 
|- ( ph -> M e. ZZ )
climcn1.3 
|- ( ph -> A e. B )
climcn1.4 
|- ( ( ph /\ z e. B ) -> ( F ` z ) e. CC )
climcn1.5 
|- ( ph -> G ~~> A )
climcn1.6 
|- ( ph -> H e. W )
climcn1.7 
|- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
climcn1.8 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. B )
climcn1.9 
|- ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
Assertion climcn1 
|- ( ph -> H ~~> ( F ` A ) )

Proof

Step Hyp Ref Expression
1 climcn1.1 
 |-  Z = ( ZZ>= ` M )
2 climcn1.2 
 |-  ( ph -> M e. ZZ )
3 climcn1.3 
 |-  ( ph -> A e. B )
4 climcn1.4 
 |-  ( ( ph /\ z e. B ) -> ( F ` z ) e. CC )
5 climcn1.5 
 |-  ( ph -> G ~~> A )
6 climcn1.6 
 |-  ( ph -> H e. W )
7 climcn1.7 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
8 climcn1.8 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. B )
9 climcn1.9 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
10 2 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> M e. ZZ )
11 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
12 eqidd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
13 5 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> G ~~> A )
14 1 10 11 12 13 climi2 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y )
15 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
16 8 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) -> ( G ` k ) e. B )
17 fvoveq1 
 |-  ( z = ( G ` k ) -> ( abs ` ( z - A ) ) = ( abs ` ( ( G ` k ) - A ) ) )
18 17 breq1d 
 |-  ( z = ( G ` k ) -> ( ( abs ` ( z - A ) ) < y <-> ( abs ` ( ( G ` k ) - A ) ) < y ) )
19 18 imbrov2fvoveq 
 |-  ( z = ( G ` k ) -> ( ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) <-> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) ) )
20 19 rspcva 
 |-  ( ( ( G ` k ) e. B /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) -> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
21 16 20 sylan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ k e. Z ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) -> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
22 21 an32s 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) /\ k e. Z ) -> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
23 15 22 sylan2 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
24 23 anassrs 
 |-  ( ( ( ( ( ph /\ y e. RR+ ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( G ` k ) - A ) ) < y -> ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
25 24 ralimdva 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
26 25 reximdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
27 26 ex 
 |-  ( ( ph /\ y e. RR+ ) -> ( A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) ) )
28 14 27 mpid 
 |-  ( ( ph /\ y e. RR+ ) -> ( A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
29 28 rexlimdva 
 |-  ( ph -> ( E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
30 29 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. RR+ A. z e. B ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
31 7 30 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x )
32 31 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x )
33 fveq2 
 |-  ( z = A -> ( F ` z ) = ( F ` A ) )
34 33 eleq1d 
 |-  ( z = A -> ( ( F ` z ) e. CC <-> ( F ` A ) e. CC ) )
35 4 ralrimiva 
 |-  ( ph -> A. z e. B ( F ` z ) e. CC )
36 34 35 3 rspcdva 
 |-  ( ph -> ( F ` A ) e. CC )
37 fveq2 
 |-  ( z = ( G ` k ) -> ( F ` z ) = ( F ` ( G ` k ) ) )
38 37 eleq1d 
 |-  ( z = ( G ` k ) -> ( ( F ` z ) e. CC <-> ( F ` ( G ` k ) ) e. CC ) )
39 35 adantr 
 |-  ( ( ph /\ k e. Z ) -> A. z e. B ( F ` z ) e. CC )
40 38 39 8 rspcdva 
 |-  ( ( ph /\ k e. Z ) -> ( F ` ( G ` k ) ) e. CC )
41 1 2 6 9 36 40 clim2c 
 |-  ( ph -> ( H ~~> ( F ` A ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` ( G ` k ) ) - ( F ` A ) ) ) < x ) )
42 32 41 mpbird 
 |-  ( ph -> H ~~> ( F ` A ) )