This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climcn2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climcn2.3a ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
climcn2.3b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
climcn2.4 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 𝐹 𝑣 ) ∈ ℂ )
climcn2.5a ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
climcn2.5b ⊢ ( 𝜑 → 𝐻 ⇝ 𝐵 )
climcn2.6 ⊢ ( 𝜑 → 𝐾 ∈ 𝑊 )
climcn2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
climcn2.8a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐶 )
climcn2.8b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝐷 )
climcn2.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) )
Assertion climcn2 ( 𝜑 → 𝐾 ⇝ ( 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 climcn2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climcn2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climcn2.3a ⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
4 climcn2.3b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
5 climcn2.4 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐶 ∧ 𝑣 ∈ 𝐷 ) ) → ( 𝑢 𝐹 𝑣 ) ∈ ℂ )
6 climcn2.5a ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
7 climcn2.5b ⊢ ( 𝜑 → 𝐻 ⇝ 𝐵 )
8 climcn2.6 ⊢ ( 𝜑 → 𝐾 ∈ 𝑊 )
9 climcn2.7 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
10 climcn2.8a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐶 )
11 climcn2.8b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝐷 )
12 climcn2.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐾 ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑀 ∈ ℤ )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ+ )
15 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
16 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝐺 ⇝ 𝐴 )
17 1 13 14 15 16 climi2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑧 ∈ ℝ+ )
19 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐻 ‘ 𝑘 ) )
20 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → 𝐻 ⇝ 𝐵 )
21 1 13 18 19 20 climi2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 )
22 1 rexanuz2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) ↔ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) )
23 17 21 22 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) )
24 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
25 fvoveq1 ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( abs ‘ ( 𝑢 − 𝐴 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) )
26 25 breq1d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
27 26 anbi1d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) ) )
28 oveq1 ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( 𝑢 𝐹 𝑣 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) )
29 28 fvoveq1d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) = ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) )
30 29 breq1d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
31 27 30 imbi12d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ↔ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
32 fvoveq1 ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( abs ‘ ( 𝑣 − 𝐵 ) ) = ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) )
33 32 breq1d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ↔ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) )
34 33 anbi2d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) ) )
35 oveq2 ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) = ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) )
36 35 fvoveq1d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) = ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) )
37 36 breq1d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
38 34 37 imbi12d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ↔ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
39 31 38 rspc2v ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐶 ∧ ( 𝐻 ‘ 𝑘 ) ∈ 𝐷 ) → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
40 10 11 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
41 40 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
42 41 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
43 24 42 sylan2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
44 43 anassrs ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
45 44 ralimdva ⊢ ( ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
46 45 reximdva ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
47 46 ex ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( ( 𝐻 ‘ 𝑘 ) − 𝐵 ) ) < 𝑧 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) ) )
49 23 48 mpid ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
50 49 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( ( ( abs ‘ ( 𝑢 − 𝐴 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐵 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
52 9 51 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 )
53 52 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 )
54 5 3 4 caovcld ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ ℂ )
55 10 11 jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐶 ∧ ( 𝐻 ‘ 𝑘 ) ∈ 𝐷 ) )
56 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( 𝑢 𝐹 𝑣 ) ∈ ℂ )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( 𝑢 𝐹 𝑣 ) ∈ ℂ )
58 28 eleq1d ⊢ ( 𝑢 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑢 𝐹 𝑣 ) ∈ ℂ ↔ ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) ∈ ℂ ) )
59 35 eleq1d ⊢ ( 𝑣 = ( 𝐻 ‘ 𝑘 ) → ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 𝑣 ) ∈ ℂ ↔ ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) ∈ ℂ ) )
60 58 59 rspc2v ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐶 ∧ ( 𝐻 ‘ 𝑘 ) ∈ 𝐷 ) → ( ∀ 𝑢 ∈ 𝐶 ∀ 𝑣 ∈ 𝐷 ( 𝑢 𝐹 𝑣 ) ∈ ℂ → ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) ∈ ℂ ) )
61 55 57 60 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) ∈ ℂ )
62 1 2 8 12 54 61 clim2c ⊢ ( 𝜑 → ( 𝐾 ⇝ ( 𝐴 𝐹 𝐵 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( ( 𝐺 ‘ 𝑘 ) 𝐹 ( 𝐻 ‘ 𝑘 ) ) − ( 𝐴 𝐹 𝐵 ) ) ) < 𝑥 ) )
63 53 62 mpbird ⊢ ( 𝜑 → 𝐾 ⇝ ( 𝐴 𝐹 𝐵 ) )