Theorem climcn1

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

	Ref	Expression
Hypotheses	climcn1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climcn1.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climcn1.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	climcn1.4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
	climcn1.5	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
	climcn1.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
	climcn1.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
	climcn1.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐵 )
	climcn1.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
Assertion	climcn1	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climcn1.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climcn1.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climcn1.3	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
4		climcn1.4	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
5		climcn1.5	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )
6		climcn1.6	⊢ ( 𝜑 → 𝐻 ∈ 𝑊 )
7		climcn1.7	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
8		climcn1.8	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐵 )
9		climcn1.9	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
12		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
13	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝐺 ⇝ 𝐴 )
14	1 10 11 12 13	climi2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 )
15	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
16	8	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝐵 )
17		fvoveq1	⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) )
18	17	breq1d	⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 ) )
19	18	imbrov2fvoveq	⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ↔ ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) )
20	19	rspcva	⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
21	16 20	sylan	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
22	21	an32s	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
23	15 22	sylan2	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
24	23	anassrs	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
25	24	ralimdva	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
26	25	reximdva	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
27	26	ex	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑦 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) )
28	14 27	mpid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
29	28	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
30	29	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝐵 ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
31	7 30	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 )
32	31	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 )
33		fveq2	⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) )
34	33	eleq1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℂ ) )
35	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
36	34 35 3	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
37		fveq2	⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
38	37	eleq1d	⊢ ( 𝑧 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ ) )
39	35	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∀ 𝑧 ∈ 𝐵 ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
40	38 39 8	rspcdva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
41	1 2 6 9 36 40	clim2c	⊢ ( 𝜑 → ( 𝐻 ⇝ ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )
42	32 41	mpbird	⊢ ( 𝜑 → 𝐻 ⇝ ( 𝐹 ‘ 𝐴 ) )