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

Axiom ax-addf 9592
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- 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 addcl 9595 should be used. Note that uses of ax-addf 9592 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 9543. (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 9511 . . 3
21, 1cxp 5002 . 2
3 caddc 9516 . 2
42, 1, 3wf 5589 1
Colors of variables: wff setvar class
This axiom is referenced by:  addex  11247  rlimadd  13465  cnfldplusf  18445  addcn  21369  itg1addlem4  22106  cnaddablo  25352  cnid  25353  addinv  25354  readdsubgo  25355  zaddsubgo  25356  efghgrpOLD  25375  cnrngo  25405  cncvc  25476  cnnv  25582  cnnvba  25584  cncph  25734  raddcn  27911  addcomgi  31365
  Copyright terms: Public domain W3C validator