**Description: **Multiplication is an
operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ax-mulcl 9877 should be used. Note that uses of ax-mulf 9895
can be eliminated by using the defined operation
(𝑥
∈ ℂ, 𝑦 ∈
ℂ ↦ (𝑥 ·
𝑦)) in place of
·, from which
this axiom (with the defined operation in place of ·) follows as a
theorem.
This axiom is justified by theorem axmulf 9846. (New usage is discouraged.)
(Contributed by NM, 19-Oct-2004.) |