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

Metamath Proof Explorer

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→ ℂ ) )