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

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 
|- ( ph -> A e. CC )
add1cncf.f 
|- F = ( x e. CC |-> ( x + A ) )
Assertion add1cncf 
|- ( ph -> F e. ( CC -cn-> CC ) )

Proof

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