Metamath Proof Explorer


Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis expcn.j J = TopOpen fld
Assertion divccn A A 0 x x A J Cn J

Proof

Step Hyp Ref Expression
1 expcn.j J = TopOpen fld
2 divrec x A A 0 x A = x 1 A
3 2 3expb x A A 0 x A = x 1 A
4 3 ancoms A A 0 x x A = x 1 A
5 4 mpteq2dva A A 0 x x A = x x 1 A
6 1 cnfldtopon J TopOn
7 6 a1i A A 0 J TopOn
8 7 cnmptid A A 0 x x J Cn J
9 reccl A A 0 1 A
10 7 7 9 cnmptc A A 0 x 1 A J Cn J
11 1 mpomulcn u , v u v J × t J Cn J
12 11 a1i A A 0 u , v u v J × t J Cn J
13 oveq12 u = x v = 1 A u v = x 1 A
14 7 8 10 7 7 12 13 cnmpt12 A A 0 x x 1 A J Cn J
15 5 14 eqeltrd A A 0 x x A J Cn J