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