Metamath Proof Explorer


Theorem add1cncf

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

Ref Expression
Hypotheses add1cncf.a φA
add1cncf.f F=xx+A
Assertion add1cncf φF:cn

Proof

Step Hyp Ref Expression
1 add1cncf.a φA
2 add1cncf.f F=xx+A
3 ssid
4 cncfmptid xx:cn
5 3 3 4 mp2an xx:cn
6 5 a1i φxx:cn
7 id AA
8 3 a1i A
9 cncfmptc AxA:cn
10 7 8 8 9 syl3anc AxA:cn
11 1 10 syl φxA:cn
12 6 11 addcncf φxx+A:cn
13 2 12 eqeltrid φF:cn