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

Metamath Proof Explorer

Axiom ax-mulcl

Description: Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by Theorem axmulcl . Proofs should normally use mulcl instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cc class ℂ
2 0 1 wcel wff A ∈ ℂ
3 cB class B
4 3 1 wcel wff B ∈ ℂ
5 2 4 wa wff A ∈ ℂ ∧ B ∈ ℂ
6 cmul class ×
7 0 3 6 co class A ⁢ B
8 7 1 wcel wff A ⁢ B ∈ ℂ
9 5 8 wi wff A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ