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 ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„‚ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA โŠข ๐ด
1 cc โŠข โ„‚
2 0 1 wcel โŠข ๐ด โˆˆ โ„‚
3 cB โŠข ๐ต
4 3 1 wcel โŠข ๐ต โˆˆ โ„‚
5 2 4 wa โŠข ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ )
6 cmul โŠข ยท
7 0 3 6 co โŠข ( ๐ด ยท ๐ต )
8 7 1 wcel โŠข ( ๐ด ยท ๐ต ) โˆˆ โ„‚
9 5 8 wi โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„‚ )