Metamath Proof Explorer

Theorem divccnOLD

Description: Obsolete version of divccn as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis expcnOLD.j ⊢ J = TopOpen ⁡ ℂ fld
Assertion divccnOLD ⊢ A ∈ ℂ ∧ A ≠ 0 → x ∈ ℂ ⟼ x A ∈ J Cn J

Proof

Step Hyp Ref Expression
1 expcnOLD.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