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 ) )