ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1cn Structured version   GIF version

Axiom ax-1cn 6736
Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6707. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn 1

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 6672 . 2 class 1
2 cc 6669 . 2 class
31, 2wcel 1390 1 wff 1
Colors of variables: wff set class
This axiom is referenced by:  0cn  6777  1ex  6780  mulid1  6782  mulid2  6783  1cnd  6801  muladd11  6903  1p1times  6904  peano2cn  6905  peano2cnm  7033  0reALT  7064  pncan1  7131  npcan1  7132  kcnktkm1cn  7136  ine0  7147  mulm1  7153  mulsubfacd  7171  ixi  7327  inelr  7328  muleqadd  7391  recclap  7400  recap0  7406  recidap  7407  recidap2  7408  div1  7422  1div1e1  7423  diveqap1  7424  recdivap  7436  divdivap1  7441  divdivap2  7442  recdivap2  7443  conjmulap  7447  eqneg  7450  div2negap  7453  recreclt  7607  nn1m1nn  7673  nn1suc  7674  nnaddcl  7675  nnmulcl  7676  nnsub  7693  1m1e0  7724  neg1cn  7760  neg1ne0  7762  neg1ap0  7764  negneg1e1  7765  1pneg1e0  7766  1m0e1  7768  0p1e1  7769  1p0e1  7770  2m1e1  7772  3m1e2  7774  2p2e4  7775  1p2e3  7782  3p2e5  7790  3p3e6  7791  4p2e6  7792  4p3e7  7793  4p4e8  7794  5p2e7  7795  5p3e8  7796  5p4e9  7797  5p5e10  7798  6p2e8  7799  6p3e9  7800  6p4e10  7801  7p2e9  7802  7p3e10  7803  8p2e10  7804  1t1e1  7805  3t3e9  7810  neg1mulneg1e1  7875  1mhlfehlf  7880  8th4div3  7881  halfpm6th  7882  addltmul  7898  elnn0nn  7960  peano2z  8017  zlem1lt  8036  zltlem1  8037  nnaddm1cl  8041  elz2  8048  zextlt  8068  zeo  8079  peano5uzti  8082  numsuc  8115  numltc  8123  numsucc  8129  numaddc  8138  6p5lem  8152  4t3lem  8174  7t4e28  8187  decbin2  8207  uzp1  8242  peano2uzr  8264  uzaddcl  8265  qreccl  8311  iccf1o  8602  fz01en  8647  fztp  8670  fzsuc2  8671  fztpval  8675  fseq1m1p1  8687  elfzp1b  8689  fzoss2  8758  fzval3  8790  fzosplitsnm1  8795  fzo0to42pr  8806  fzosplitprm1  8820  frecfzen2  8845  nn0ennn  8850  expival  8871  expcl  8887  m1expcl2  8891  expclzaplem  8893  expm1t  8897  1exp  8898  mulexpzap  8909  expadd  8911  expaddzap  8913  expmul  8914  expubnd  8925  neg1sqe1  8961  irec  8965  i4  8968  binom21  8976  bernneq  8982  bernneq2  8983  rei  9087  imi  9088
  Copyright terms: Public domain W3C validator