Description: Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | add1cncf.a | |
|
add1cncf.f | |
||
Assertion | add1cncf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | add1cncf.a | |
|
2 | add1cncf.f | |
|
3 | ssid | |
|
4 | cncfmptid | |
|
5 | 3 3 4 | mp2an | |
6 | 5 | a1i | |
7 | id | |
|
8 | 3 | a1i | |
9 | cncfmptc | |
|
10 | 7 8 8 9 | syl3anc | |
11 | 1 10 | syl | |
12 | 6 11 | addcncf | |
13 | 2 12 | eqeltrid | |