Metamath Proof Explorer

Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014)

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 mulcn ⊢ × ∈ J × t J Cn J
12 11 a1i ⊢ A ∈ ℂ ∧ A ≠ 0 → × ∈ J × t J Cn J
13 7 8 10 12 cnmpt12f ⊢ A ∈ ℂ ∧ A ≠ 0 → x ∈ ℂ ⟼ x ⁢ 1 A ∈ J Cn J
14 5 13 eqeltrd ⊢ A ∈ ℂ ∧ A ≠ 0 → x ∈ ℂ ⟼ x A ∈ J Cn J