| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ax-mulf | Structured version Visualization version GIF version | ||
| Description: Multiplication is an
operation on the complex numbers. This axiom tells
us that · is defined only on complex
numbers which is analogous to
the way that other operations are defined, for example see subf 11510
or
eff 16117. However, while Metamath can handle this
axiom, if we wish to work
with weaker complex number axioms, we can avoid it by using the less
specific mulcl 11239. Note that uses of ax-mulf 11235 can be eliminated by using
the defined operation (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) in place of
·, as seen in mpomulf 11250.
This axiom is justified by Theorem axmulf 11186. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
| Ref | Expression |
|---|---|
| ax-mulf | ⊢ · :(ℂ × ℂ)⟶ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cc 11153 | . . 3 class ℂ | |
| 2 | 1, 1 | cxp 5683 | . 2 class (ℂ × ℂ) |
| 3 | cmul 11160 | . 2 class · | |
| 4 | 2, 1, 3 | wf 6557 | 1 wff · :(ℂ × ℂ)⟶ℂ |
| Colors of variables: wff setvar class |
| This axiom is referenced by: mulnzcnf 11909 mulex 13033 cnfldmul 21372 dfcnfldOLD 21380 mulcn 24889 iimulcnOLD 24968 dvdsmulf1o 27239 fsumdvdsmulOLD 27240 cncvcOLD 30602 xrge0pluscn 33939 |
| Copyright terms: Public domain | W3C validator |