Metamath Proof Explorer


Theorem addccncf2

Description: Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 addccncf2.1 F = x A B + x
2 simpl A B A
3 simpr A B B
4 ssidd A B
5 2 3 4 constcncfg A B x A B : A cn
6 ssid
7 cncfmptid A x A x : A cn
8 6 7 mpan2 A x A x : A cn
9 8 adantr A B x A x : A cn
10 5 9 addcncf A B x A B + x : A cn
11 1 10 eqeltrid A B F : A cn