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

Metamath Proof Explorer

Theorem sub1cncfd

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

Ref Expression
Hypotheses sub1cncfd.1 
|- ( ph -> A e. CC )
sub1cncfd.2 
|- F = ( x e. CC |-> ( x - A ) )
Assertion sub1cncfd 
|- ( ph -> F e. ( CC -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 sub1cncfd.1 
 |-  ( ph -> A e. CC )
2 sub1cncfd.2 
 |-  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 3 a1i 
 |-  ( ph -> CC C_ CC )
8 cncfmptc 
 |-  ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
9 1 7 7 8 syl3anc 
 |-  ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
10 6 9 subcncf 
 |-  ( ph -> ( x e. CC |-> ( x - A ) ) e. ( CC -cn-> CC ) )
11 2 10 eqeltrid 
 |-  ( ph -> F e. ( CC -cn-> CC ) )