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	⊢ ( 𝜑 → 𝐾 ⇝ ( 𝐴 𝐹 𝐵 ) )