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

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 → u F v ∈ ℂ
6 climcn2.5a ⊢ φ → G ⇝ A
7 climcn2.5b ⊢ φ → H ⇝ B
8 climcn2.6 ⊢ φ → K ∈ W
9 climcn2.7 ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < 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 ⁡ k F H ⁡ 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 ∈ ℤ ≥ j G ⁡ 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 ∈ ℤ ≥ j H ⁡ k − B < z
22 1 rexanuz2 ⊢ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ H ⁡ k − B < z ↔ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ ∃ j ∈ Z ∀ k ∈ ℤ ≥ j H ⁡ k − B < z
23 17 21 22 sylanbrc ⊢ φ ∧ y ∈ ℝ + ∧ z ∈ ℝ + → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ 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 → u F v = G ⁡ k F v
29 28 fvoveq1d ⊢ u = G ⁡ k → u F v − A F B = G ⁡ k F v − A F B
30 29 breq1d ⊢ u = G ⁡ k → u F v − A F B < x ↔ G ⁡ k F v − A F B < x
31 27 30 imbi12d ⊢ u = G ⁡ k → u − A < y ∧ v − B < z → u F v − A F B < x ↔ G ⁡ k − A < y ∧ v − B < z → G ⁡ k F v − A F B < 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 ⁡ k F v = G ⁡ k F H ⁡ k
36 35 fvoveq1d ⊢ v = H ⁡ k → G ⁡ k F v − A F B = G ⁡ k F H ⁡ k − A F B
37 36 breq1d ⊢ v = H ⁡ k → G ⁡ k F v − A F B < x ↔ G ⁡ k F H ⁡ k − A F B < x
38 34 37 imbi12d ⊢ v = H ⁡ k → G ⁡ k − A < y ∧ v − B < z → G ⁡ k F v − A F B < x ↔ G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
39 31 38 rspc2v ⊢ G ⁡ k ∈ C ∧ H ⁡ k ∈ D → ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
40 10 11 39 syl2anc ⊢ φ ∧ k ∈ Z → ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
41 40 imp ⊢ φ ∧ k ∈ Z ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
42 41 an32s ⊢ φ ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x ∧ k ∈ Z → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
43 24 42 sylan2 ⊢ φ ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
44 43 anassrs ⊢ φ ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x ∧ j ∈ Z ∧ k ∈ ℤ ≥ j → G ⁡ k − A < y ∧ H ⁡ k − B < z → G ⁡ k F H ⁡ k − A F B < x
45 44 ralimdva ⊢ φ ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x ∧ j ∈ Z → ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ H ⁡ k − B < z → ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
46 45 reximdva ⊢ φ ∧ ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ H ⁡ k − B < z → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
47 46 ex ⊢ φ → ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ H ⁡ k − B < z → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
48 47 adantr ⊢ φ ∧ y ∈ ℝ + ∧ z ∈ ℝ + → ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k − A < y ∧ H ⁡ k − B < z → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
49 23 48 mpid ⊢ φ ∧ y ∈ ℝ + ∧ z ∈ ℝ + → ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
50 49 rexlimdvva ⊢ φ → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
51 50 adantr ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∃ z ∈ ℝ + ∀ u ∈ C ∀ v ∈ D u − A < y ∧ v − B < z → u F v − A F B < x → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
52 9 51 mpd ⊢ φ ∧ x ∈ ℝ + → ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
53 52 ralrimiva ⊢ φ → ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
54 5 3 4 caovcld ⊢ φ → A F B ∈ ℂ
55 10 11 jca ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ C ∧ H ⁡ k ∈ D
56 5 ralrimivva ⊢ φ → ∀ u ∈ C ∀ v ∈ D u F v ∈ ℂ
57 56 adantr ⊢ φ ∧ k ∈ Z → ∀ u ∈ C ∀ v ∈ D u F v ∈ ℂ
58 28 eleq1d ⊢ u = G ⁡ k → u F v ∈ ℂ ↔ G ⁡ k F v ∈ ℂ
59 35 eleq1d ⊢ v = H ⁡ k → G ⁡ k F v ∈ ℂ ↔ G ⁡ k F H ⁡ k ∈ ℂ
60 58 59 rspc2v ⊢ G ⁡ k ∈ C ∧ H ⁡ k ∈ D → ∀ u ∈ C ∀ v ∈ D u F v ∈ ℂ → G ⁡ k F H ⁡ k ∈ ℂ
61 55 57 60 sylc ⊢ φ ∧ k ∈ Z → G ⁡ k F H ⁡ k ∈ ℂ
62 1 2 8 12 54 61 clim2c ⊢ φ → K ⇝ A F B ↔ ∀ x ∈ ℝ + ∃ j ∈ Z ∀ k ∈ ℤ ≥ j G ⁡ k F H ⁡ k − A F B < x
63 53 62 mpbird ⊢ φ → K ⇝ A F B