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 ⊢ φ ∧ k ∈ A → B ∈ V
rlimabs.2 ⊢ φ → k ∈ A ⟼ B ⇝ℝ C
Assertion rlimre ⊢ φ → k ∈ A ⟼ ℜ ⁡ B ⇝ℝ ℜ ⁡ C

Proof

Step Hyp Ref Expression
1 rlimabs.1 ⊢ φ ∧ k ∈ A → B ∈ V
2 rlimabs.2 ⊢ φ → k ∈ A ⟼ B ⇝ℝ C
3 1 2 rlimmptrcl ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 rlimcl ⊢ k ∈ A ⟼ B ⇝ℝ C → C ∈ ℂ
5 2 4 syl ⊢ φ → C ∈ ℂ
6 ref ⊢ ℜ : ℂ ⟶ ℝ
7 ax-resscn ⊢ ℝ ⊆ ℂ
8 fss ⊢ ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ → ℜ : ℂ ⟶ ℂ
9 6 7 8 mp2an ⊢ ℜ : ℂ ⟶ ℂ
10 9 a1i ⊢ φ → ℜ : ℂ ⟶ ℂ
11 recn2 ⊢ C ∈ ℂ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − C < y → ℜ ⁡ z − ℜ ⁡ C < x
12 5 11 sylan ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − C < y → ℜ ⁡ z − ℜ ⁡ C < x
13 3 5 2 10 12 rlimcn1b ⊢ φ → k ∈ A ⟼ ℜ ⁡ B ⇝ℝ ℜ ⁡ C