Description: The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008) (Revised by Mario Carneiro, 25-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | negfcncf.1 | |
|
Assertion | negfcncf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | negfcncf.1 | |
|
2 | cncff | |
|
3 | 2 | ffvelcdmda | |
4 | 2 | feqmptd | |
5 | eqidd | |
|
6 | negeq | |
|
7 | 3 4 5 6 | fmptco | |
8 | 7 1 | eqtr4di | |
9 | id | |
|
10 | ssid | |
|
11 | eqid | |
|
12 | 11 | negcncf | |
13 | 10 12 | mp1i | |
14 | 9 13 | cncfco | |
15 | 8 14 | eqeltrrd | |