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=ℤ≥M
climcn2.2 ⊢φ→M∈ℤ
climcn2.3a ⊢φ→A∈C
climcn2.3b ⊢φ→B∈D
climcn2.4 ⊢φ∧u∈C∧v∈D→uFv∈ℂ
climcn2.5a ⊢φ→G⇝A
climcn2.5b ⊢φ→H⇝B
climcn2.6 ⊢φ→K∈W
climcn2.7 ⊢φ∧x∈ℝ+→∃y∈ℝ+∃z∈ℝ+∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x
climcn2.8a ⊢φ∧k∈Z→G⁡k∈C
climcn2.8b ⊢φ∧k∈Z→H⁡k∈D
climcn2.9 ⊢φ∧k∈Z→K⁡k=G⁡kFH⁡k
Assertion climcn2 ⊢φ→K⇝AFB

Proof

Step Hyp Ref Expression
1 climcn2.1 ⊢Z=ℤ≥M
2 climcn2.2 ⊢φ→M∈ℤ
3 climcn2.3a ⊢φ→A∈C
4 climcn2.3b ⊢φ→B∈D
5 climcn2.4 ⊢φ∧u∈C∧v∈D→uFv∈ℂ
6 climcn2.5a ⊢φ→G⇝A
7 climcn2.5b ⊢φ→H⇝B
8 climcn2.6 ⊢φ→K∈W
9 climcn2.7 ⊢φ∧x∈ℝ+→∃y∈ℝ+∃z∈ℝ+∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x
10 climcn2.8a ⊢φ∧k∈Z→G⁡k∈C
11 climcn2.8b ⊢φ∧k∈Z→H⁡k∈D
12 climcn2.9 ⊢φ∧k∈Z→K⁡k=G⁡kFH⁡k
13 2 adantr ⊢φ∧y∈ℝ+∧z∈ℝ+→M∈ℤ
14 simprl ⊢φ∧y∈ℝ+∧z∈ℝ+→y∈ℝ+
15 eqidd ⊢φ∧y∈ℝ+∧z∈ℝ+∧k∈Z→G⁡k=G⁡k
16 6 adantr ⊢φ∧y∈ℝ+∧z∈ℝ+→G⇝A
17 1 13 14 15 16 climi2 ⊢φ∧y∈ℝ+∧z∈ℝ+→∃j∈Z∀k∈ℤ≥jG⁡k−A<y
18 simprr ⊢φ∧y∈ℝ+∧z∈ℝ+→z∈ℝ+
19 eqidd ⊢φ∧y∈ℝ+∧z∈ℝ+∧k∈Z→H⁡k=H⁡k
20 7 adantr ⊢φ∧y∈ℝ+∧z∈ℝ+→H⇝B
21 1 13 18 19 20 climi2 ⊢φ∧y∈ℝ+∧z∈ℝ+→∃j∈Z∀k∈ℤ≥jH⁡k−B<z
22 1 rexanuz2 ⊢∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z↔∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧∃j∈Z∀k∈ℤ≥jH⁡k−B<z
23 17 21 22 sylanbrc ⊢φ∧y∈ℝ+∧z∈ℝ+→∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z
24 1 uztrn2 ⊢j∈Z∧k∈ℤ≥j→k∈Z
25 fvoveq1 ⊢u=G⁡k→u−A=G⁡k−A
26 25 breq1d ⊢u=G⁡k→u−A<y↔G⁡k−A<y
27 26 anbi1d ⊢u=G⁡k→u−A<y∧v−B<z↔G⁡k−A<y∧v−B<z
28 oveq1 ⊢u=G⁡k→uFv=G⁡kFv
29 28 fvoveq1d ⊢u=G⁡k→uFv−AFB=G⁡kFv−AFB
30 29 breq1d ⊢u=G⁡k→uFv−AFB<x↔G⁡kFv−AFB<x
31 27 30 imbi12d ⊢u=G⁡k→u−A<y∧v−B<z→uFv−AFB<x↔G⁡k−A<y∧v−B<z→G⁡kFv−AFB<x
32 fvoveq1 ⊢v=H⁡k→v−B=H⁡k−B
33 32 breq1d ⊢v=H⁡k→v−B<z↔H⁡k−B<z
34 33 anbi2d ⊢v=H⁡k→G⁡k−A<y∧v−B<z↔G⁡k−A<y∧H⁡k−B<z
35 oveq2 ⊢v=H⁡k→G⁡kFv=G⁡kFH⁡k
36 35 fvoveq1d ⊢v=H⁡k→G⁡kFv−AFB=G⁡kFH⁡k−AFB
37 36 breq1d ⊢v=H⁡k→G⁡kFv−AFB<x↔G⁡kFH⁡k−AFB<x
38 34 37 imbi12d ⊢v=H⁡k→G⁡k−A<y∧v−B<z→G⁡kFv−AFB<x↔G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
39 31 38 rspc2v ⊢G⁡k∈C∧H⁡k∈D→∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
40 10 11 39 syl2anc ⊢φ∧k∈Z→∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
41 40 imp ⊢φ∧k∈Z∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
42 41 an32s ⊢φ∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x∧k∈Z→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
43 24 42 sylan2 ⊢φ∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x∧j∈Z∧k∈ℤ≥j→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
44 43 anassrs ⊢φ∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x∧j∈Z∧k∈ℤ≥j→G⁡k−A<y∧H⁡k−B<z→G⁡kFH⁡k−AFB<x
45 44 ralimdva ⊢φ∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x∧j∈Z→∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z→∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
46 45 reximdva ⊢φ∧∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
47 46 ex ⊢φ→∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
48 47 adantr ⊢φ∧y∈ℝ+∧z∈ℝ+→∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡k−A<y∧H⁡k−B<z→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
49 23 48 mpid ⊢φ∧y∈ℝ+∧z∈ℝ+→∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
50 49 rexlimdvva ⊢φ→∃y∈ℝ+∃z∈ℝ+∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
51 50 adantr ⊢φ∧x∈ℝ+→∃y∈ℝ+∃z∈ℝ+∀u∈C∀v∈Du−A<y∧v−B<z→uFv−AFB<x→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
52 9 51 mpd ⊢φ∧x∈ℝ+→∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
53 52 ralrimiva ⊢φ→∀x∈ℝ+∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
54 5 3 4 caovcld ⊢φ→AFB∈ℂ
55 10 11 jca ⊢φ∧k∈Z→G⁡k∈C∧H⁡k∈D
56 5 ralrimivva ⊢φ→∀u∈C∀v∈DuFv∈ℂ
57 56 adantr ⊢φ∧k∈Z→∀u∈C∀v∈DuFv∈ℂ
58 28 eleq1d ⊢u=G⁡k→uFv∈ℂ↔G⁡kFv∈ℂ
59 35 eleq1d ⊢v=H⁡k→G⁡kFv∈ℂ↔G⁡kFH⁡k∈ℂ
60 58 59 rspc2v ⊢G⁡k∈C∧H⁡k∈D→∀u∈C∀v∈DuFv∈ℂ→G⁡kFH⁡k∈ℂ
61 55 57 60 sylc ⊢φ∧k∈Z→G⁡kFH⁡k∈ℂ
62 1 2 8 12 54 61 clim2c ⊢φ→K⇝AFB↔∀x∈ℝ+∃j∈Z∀k∈ℤ≥jG⁡kFH⁡k−AFB<x
63 53 62 mpbird ⊢φ→K⇝AFB