Theorem sub2cncfd

Description: Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	sub2cncfd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	sub2cncfd.2	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 − 𝑥 ) )
Assertion	sub2cncfd	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		sub2cncfd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		sub2cncfd.2	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 − 𝑥 ) )
3		ssid	⊢ ℂ ⊆ ℂ
4	3	a1i	⊢ ( 𝜑 → ℂ ⊆ ℂ )
5		cncfmptc	⊢ ( ( 𝐴 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
6	1 4 4 5	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
7		cncfmptid	⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
8	3 3 7	mp2an	⊢ ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ )
9	8	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
10	6 9	subcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝐴 − 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
11	2 10	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )