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

Metamath Proof Explorer

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