MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-addf Structured version   Visualization version   GIF version

Axiom ax-addf 11231
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 11234 should be used. Note that uses of ax-addf 11231 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 11182. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)

Assertion
Ref Expression
ax-addf + :(ℂ × ℂ)⟶ℂ

Detailed syntax breakdown of Axiom ax-addf
StepHypRef Expression
1 cc 11150 . . 3 class
21, 1cxp 5686 . 2 class (ℂ × ℂ)
3 caddc 11155 . 2 class +
42, 1, 3wf 6558 1 wff + :(ℂ × ℂ)⟶ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  addex  13028  cnfldadd  21387  dfcnfldOLD  21397  cnfldplusf  21426  addcn  24900  itg1addlem4  25747  itg1addlem4OLD  25748  cnaddabloOLD  30609  cnidOLD  30610  cncvcOLD  30611  cnnv  30705  cnnvba  30707  cncph  30847  raddcn  33889  addcomgi  44451
  Copyright terms: Public domain W3C validator