This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion divccnOLD ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 expcnOLD.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 divrec ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
3 2 3expb ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
4 3 ancoms ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
5 4 mpteq2dva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( 1 / 𝐴 ) ) ) )
6 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
7 6 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
8 7 cnmptid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
9 reccl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
10 7 7 9 cnmptc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 1 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
11 1 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
12 11 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
13 7 8 10 12 cnmpt12f ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( 1 / 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
14 5 13 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )