Theorem recn2

Description: The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Assertion	recn2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐴 ) ) ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ref	⊢ ℜ : ℂ ⟶ ℝ
2		ax-resscn	⊢ ℝ ⊆ ℂ
3		fss	⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℜ : ℂ ⟶ ℂ )
4	1 2 3	mp2an	⊢ ℜ : ℂ ⟶ ℂ
5		resub	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℜ ‘ ( 𝑧 − 𝐴 ) ) = ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐴 ) ) )
6	5	fveq2d	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ℜ ‘ ( 𝑧 − 𝐴 ) ) ) = ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐴 ) ) ) )
7		subcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑧 − 𝐴 ) ∈ ℂ )
8		absrele	⊢ ( ( 𝑧 − 𝐴 ) ∈ ℂ → ( abs ‘ ( ℜ ‘ ( 𝑧 − 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) )
9	7 8	syl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ℜ ‘ ( 𝑧 − 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) )
10	6 9	eqbrtrrd	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) )
11	4 10	cn1lem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ℜ ‘ 𝑧 ) − ( ℜ ‘ 𝐴 ) ) ) < 𝑥 ) )