![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax-addf | Structured version Visualization version GIF version |
Description: Addition 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-order or second-order statement (see
https://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 addcl 11222 should be used. Note that uses of ax-addf 11219 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 axaddf 11170. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
Ref | Expression |
---|---|
ax-addf | ⊢ + :(ℂ × ℂ)⟶ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cc 11138 | . . 3 class ℂ | |
2 | 1, 1 | cxp 5676 | . 2 class (ℂ × ℂ) |
3 | caddc 11143 | . 2 class + | |
4 | 2, 1, 3 | wf 6545 | 1 wff + :(ℂ × ℂ)⟶ℂ |
Colors of variables: wff setvar class |
This axiom is referenced by: addex 13006 rlimaddOLD 15624 cnfldadd 21302 dfcnfldOLD 21312 cnfldplusf 21341 addcn 24825 itg1addlem4 25672 itg1addlem4OLD 25673 cnaddabloOLD 30463 cnidOLD 30464 cncvcOLD 30465 cnnv 30559 cnnvba 30561 cncph 30701 raddcn 33661 addcomgi 44035 |
Copyright terms: Public domain | W3C validator |