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

Metamath Proof Explorer

Theorem add2cncf

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

Ref Expression
Hypotheses add2cncf.a 
|- ( ph -> A e. CC )
add2cncf.f 
|- F = ( x e. CC |-> ( A + x ) )
Assertion add2cncf 
|- ( ph -> F e. ( CC -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 add2cncf.a 
 |-  ( ph -> A e. CC )
2 add2cncf.f 
 |-  F = ( x e. CC |-> ( A + x ) )
3 ssid 
 |-  CC C_ CC
4 3 a1i 
 |-  ( A e. CC -> CC C_ CC )
5 cncfmptc 
 |-  ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
6 4 4 5 mpd3an23 
 |-  ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
7 1 6 syl 
 |-  ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
8 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
9 3 3 8 mp2an 
 |-  ( x e. CC |-> x ) e. ( CC -cn-> CC )
10 9 a1i 
 |-  ( ph -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
11 7 10 addcncf 
 |-  ( ph -> ( x e. CC |-> ( A + x ) ) e. ( CC -cn-> CC ) )
12 2 11 eqeltrid 
 |-  ( ph -> F e. ( CC -cn-> CC ) )