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

Metamath Proof Explorer

Theorem sub2cncfd

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

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

Proof

Step Hyp Ref Expression
1 sub2cncfd.1 
 |-  ( ph -> A e. CC )
2 sub2cncfd.2 
 |-  F = ( x e. CC |-> ( A - x ) )
3 ssid 
 |-  CC C_ CC
4 3 a1i 
 |-  ( ph -> CC C_ CC )
5 cncfmptc 
 |-  ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
6 1 4 4 5 syl3anc 
 |-  ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
7 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
8 3 3 7 mp2an 
 |-  ( x e. CC |-> x ) e. ( CC -cn-> CC )
9 8 a1i 
 |-  ( ph -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
10 6 9 subcncf 
 |-  ( ph -> ( x e. CC |-> ( A - x ) ) e. ( CC -cn-> CC ) )
11 2 10 eqeltrid 
 |-  ( ph -> F e. ( CC -cn-> CC ) )