Metamath Proof Explorer


Theorem rlimre

Description: Limit of the real part of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimabs.1 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑉 )
rlimabs.2 ( 𝜑 → ( 𝑘𝐴𝐵 ) ⇝𝑟 𝐶 )
Assertion rlimre ( 𝜑 → ( 𝑘𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ⇝𝑟 ( ℜ ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rlimabs.1 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑉 )
2 rlimabs.2 ( 𝜑 → ( 𝑘𝐴𝐵 ) ⇝𝑟 𝐶 )
3 1 2 rlimmptrcl ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
4 rlimcl ( ( 𝑘𝐴𝐵 ) ⇝𝑟 𝐶𝐶 ∈ ℂ )
5 2 4 syl ( 𝜑𝐶 ∈ ℂ )
6 ref ℜ : ℂ ⟶ ℝ
7 ax-resscn ℝ ⊆ ℂ
8 fss ( ( ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℜ : ℂ ⟶ ℂ )
9 6 7 8 mp2an ℜ : ℂ ⟶ ℂ
10 9 a1i ( 𝜑 → ℜ : ℂ ⟶ ℂ )
11 recn2 ( ( 𝐶 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐶 ) ) ) < 𝑥 ) )
12 5 11 sylan ( ( 𝜑𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧𝐶 ) ) < 𝑦 → ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐶 ) ) ) < 𝑥 ) )
13 3 5 2 10 12 rlimcn1b ( 𝜑 → ( 𝑘𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ⇝𝑟 ( ℜ ‘ 𝐶 ) )