Metamath Proof Explorer


Theorem negcncf

Description: The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis negcncf.1 F = x A x
Assertion negcncf A F : A cn

Proof

Step Hyp Ref Expression
1 negcncf.1 F = x A x
2 neg1cn 1
3 ssel2 A x A x
4 ovmpot 1 x -1 a , b a b x = -1 x
5 4 eqcomd 1 x -1 x = -1 a , b a b x
6 2 3 5 sylancr A x A -1 x = -1 a , b a b x
7 3 mulm1d A x A -1 x = x
8 6 7 eqtr3d A x A -1 a , b a b x = x
9 8 mpteq2dva A x A -1 a , b a b x = x A x
10 9 1 eqtr4di A x A -1 a , b a b x = F
11 eqid TopOpen fld = TopOpen fld
12 11 mpomulcn a , b a b TopOpen fld × t TopOpen fld Cn TopOpen fld
13 12 a1i A a , b a b TopOpen fld × t TopOpen fld Cn TopOpen fld
14 ssid
15 cncfmptc 1 A x A 1 : A cn
16 2 14 15 mp3an13 A x A 1 : A cn
17 cncfmptid A x A x : A cn
18 14 17 mpan2 A x A x : A cn
19 11 13 16 18 cncfmpt2f A x A -1 a , b a b x : A cn
20 10 19 eqeltrrd A F : A cn