Metamath Proof Explorer

Theorem climcn2

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

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

Proof

Step Hyp Ref Expression
1 climcn2.1 
 |-  Z = ( ZZ>= ` M )
2 climcn2.2 
 |-  ( ph -> M e. ZZ )
3 climcn2.3a 
 |-  ( ph -> A e. C )
4 climcn2.3b 
 |-  ( ph -> B e. D )
5 climcn2.4 
 |-  ( ( ph /\ ( u e. C /\ v e. D ) ) -> ( u F v ) e. CC )
6 climcn2.5a 
 |-  ( ph -> G ~~> A )
7 climcn2.5b 
 |-  ( ph -> H ~~> B )
8 climcn2.6 
 |-  ( ph -> K e. W )
9 climcn2.7 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ E. z e. RR+ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) )
10 climcn2.8a 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. C )
11 climcn2.8b 
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) e. D )
12 climcn2.9 
 |-  ( ( ph /\ k e. Z ) -> ( K ` k ) = ( ( G ` k ) F ( H ` k ) ) )
13 2 adantr 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> M e. ZZ )
14 simprl 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> y e. RR+ )
15 eqidd 
 |-  ( ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) /\ k e. Z ) -> ( G ` k ) = ( G ` k ) )
16 6 adantr 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> G ~~> A )
17 1 13 14 15 16 climi2 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y )
18 simprr 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> z e. RR+ )
19 eqidd 
 |-  ( ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) /\ k e. Z ) -> ( H ` k ) = ( H ` k ) )
20 7 adantr 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> H ~~> B )
21 1 13 18 19 20 climi2 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( H ` k ) - B ) ) < z )
22 1 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( G ` k ) - A ) ) < y /\ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( H ` k ) - B ) ) < z ) )
23 17 21 22 sylanbrc 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) )
24 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
25 fvoveq1 
 |-  ( u = ( G ` k ) -> ( abs ` ( u - A ) ) = ( abs ` ( ( G ` k ) - A ) ) )
26 25 breq1d 
 |-  ( u = ( G ` k ) -> ( ( abs ` ( u - A ) ) < y <-> ( abs ` ( ( G ` k ) - A ) ) < y ) )
27 26 anbi1d 
 |-  ( u = ( G ` k ) -> ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) <-> ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) ) )
28 oveq1 
 |-  ( u = ( G ` k ) -> ( u F v ) = ( ( G ` k ) F v ) )
29 28 fvoveq1d 
 |-  ( u = ( G ` k ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) = ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) )
30 29 breq1d 
 |-  ( u = ( G ` k ) -> ( ( abs ` ( ( u F v ) - ( A F B ) ) ) < x <-> ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) < x ) )
31 27 30 imbi12d 
 |-  ( u = ( G ` k ) -> ( ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) <-> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) < x ) ) )
32 fvoveq1 
 |-  ( v = ( H ` k ) -> ( abs ` ( v - B ) ) = ( abs ` ( ( H ` k ) - B ) ) )
33 32 breq1d 
 |-  ( v = ( H ` k ) -> ( ( abs ` ( v - B ) ) < z <-> ( abs ` ( ( H ` k ) - B ) ) < z ) )
34 33 anbi2d 
 |-  ( v = ( H ` k ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) <-> ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) ) )
35 oveq2 
 |-  ( v = ( H ` k ) -> ( ( G ` k ) F v ) = ( ( G ` k ) F ( H ` k ) ) )
36 35 fvoveq1d 
 |-  ( v = ( H ` k ) -> ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) = ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) )
37 36 breq1d 
 |-  ( v = ( H ` k ) -> ( ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) < x <-> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
38 34 37 imbi12d 
 |-  ( v = ( H ` k ) -> ( ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F v ) - ( A F B ) ) ) < x ) <-> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) ) )
39 31 38 rspc2v 
 |-  ( ( ( G ` k ) e. C /\ ( H ` k ) e. D ) -> ( A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) ) )
40 10 11 39 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> ( A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) ) )
41 40 imp 
 |-  ( ( ( ph /\ k e. Z ) /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
42 41 an32s 
 |-  ( ( ( ph /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) /\ k e. Z ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
43 24 42 sylan2 
 |-  ( ( ( ph /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
44 43 anassrs 
 |-  ( ( ( ( ph /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
45 44 ralimdva 
 |-  ( ( ( ph /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
46 45 reximdva 
 |-  ( ( ph /\ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
47 46 ex 
 |-  ( ph -> ( A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) ) )
48 47 adantr 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( abs ` ( ( G ` k ) - A ) ) < y /\ ( abs ` ( ( H ` k ) - B ) ) < z ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) ) )
49 23 48 mpid 
 |-  ( ( ph /\ ( y e. RR+ /\ z e. RR+ ) ) -> ( A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
50 49 rexlimdvva 
 |-  ( ph -> ( E. y e. RR+ E. z e. RR+ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
51 50 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. RR+ E. z e. RR+ A. u e. C A. v e. D ( ( ( abs ` ( u - A ) ) < y /\ ( abs ` ( v - B ) ) < z ) -> ( abs ` ( ( u F v ) - ( A F B ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
52 9 51 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x )
53 52 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x )
54 5 3 4 caovcld 
 |-  ( ph -> ( A F B ) e. CC )
55 10 11 jca 
 |-  ( ( ph /\ k e. Z ) -> ( ( G ` k ) e. C /\ ( H ` k ) e. D ) )
56 5 ralrimivva 
 |-  ( ph -> A. u e. C A. v e. D ( u F v ) e. CC )
57 56 adantr 
 |-  ( ( ph /\ k e. Z ) -> A. u e. C A. v e. D ( u F v ) e. CC )
58 28 eleq1d 
 |-  ( u = ( G ` k ) -> ( ( u F v ) e. CC <-> ( ( G ` k ) F v ) e. CC ) )
59 35 eleq1d 
 |-  ( v = ( H ` k ) -> ( ( ( G ` k ) F v ) e. CC <-> ( ( G ` k ) F ( H ` k ) ) e. CC ) )
60 58 59 rspc2v 
 |-  ( ( ( G ` k ) e. C /\ ( H ` k ) e. D ) -> ( A. u e. C A. v e. D ( u F v ) e. CC -> ( ( G ` k ) F ( H ` k ) ) e. CC ) )
61 55 57 60 sylc 
 |-  ( ( ph /\ k e. Z ) -> ( ( G ` k ) F ( H ` k ) ) e. CC )
62 1 2 8 12 54 61 clim2c 
 |-  ( ph -> ( K ~~> ( A F B ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( G ` k ) F ( H ` k ) ) - ( A F B ) ) ) < x ) )
63 53 62 mpbird 
 |-  ( ph -> K ~~> ( A F B ) )