Metamath Proof Explorer


Theorem addccncf

Description: Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis addccncf.1 F = x x + A
Assertion addccncf A F : cn

Proof

Step Hyp Ref Expression
1 addccncf.1 F = x x + A
2 eqid TopOpen fld = TopOpen fld
3 2 addcn + TopOpen fld × t TopOpen fld Cn TopOpen fld
4 3 a1i A + TopOpen fld × t TopOpen fld Cn TopOpen fld
5 ssid
6 cncfmptid x x : cn
7 5 5 6 mp2an x x : cn
8 7 a1i A x x : cn
9 cncfmptc A x A : cn
10 5 5 9 mp3an23 A x A : cn
11 2 4 8 10 cncfmpt2f A x x + A : cn
12 1 11 eqeltrid A F : cn