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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 6692 . 2 class 1
2 cc 6689 . 2 class
31, 2wcel 1390 1 wff 1
Colors of variables: wff set class
This axiom is referenced by:  0cn  6797  1ex  6800  mulid1  6802  mulid2  6803  1cnd  6821  muladd11  6923  1p1times  6924  peano2cn  6925  peano2cnm  7053  0reALT  7084  pncan1  7151  npcan1  7152  kcnktkm1cn  7156  ine0  7167  mulm1  7173  mulsubfacd  7191  ixi  7347  inelr  7348  muleqadd  7411  recclap  7420  recap0  7426  recidap  7427  recidap2  7428  div1  7442  1div1e1  7443  diveqap1  7444  recdivap  7456  divdivap1  7461  divdivap2  7462  recdivap2  7463  conjmulap  7467  eqneg  7470  div2negap  7473  recreclt  7627  nn1m1nn  7693  nn1suc  7694  nnaddcl  7695  nnmulcl  7696  nnsub  7713  1m1e0  7744  neg1cn  7780  neg1ne0  7782  neg1ap0  7784  negneg1e1  7785  1pneg1e0  7786  1m0e1  7788  0p1e1  7789  1p0e1  7790  2m1e1  7792  3m1e2  7794  2p2e4  7795  1p2e3  7802  3p2e5  7810  3p3e6  7811  4p2e6  7812  4p3e7  7813  4p4e8  7814  5p2e7  7815  5p3e8  7816  5p4e9  7817  5p5e10  7818  6p2e8  7819  6p3e9  7820  6p4e10  7821  7p2e9  7822  7p3e10  7823  8p2e10  7824  1t1e1  7825  3t3e9  7830  neg1mulneg1e1  7895  1mhlfehlf  7900  8th4div3  7901  halfpm6th  7902  addltmul  7918  elnn0nn  7980  peano2z  8037  zlem1lt  8056  zltlem1  8057  nnaddm1cl  8061  elz2  8068  zextlt  8088  zeo  8099  peano5uzti  8102  numsuc  8135  numltc  8143  numsucc  8149  numaddc  8158  6p5lem  8172  4t3lem  8194  7t4e28  8207  decbin2  8227  uzp1  8262  peano2uzr  8284  uzaddcl  8285  qreccl  8331  iccf1o  8622  fz01en  8667  fztp  8690  fzsuc2  8691  fztpval  8695  fseq1m1p1  8707  elfzp1b  8709  fzoss2  8778  fzval3  8810  fzosplitsnm1  8815  fzo0to42pr  8826  fzosplitprm1  8840  frecfzen2  8865  nn0ennn  8870  expival  8891  expcl  8907  m1expcl2  8911  expclzaplem  8913  expm1t  8917  1exp  8918  mulexpzap  8929  expadd  8931  expaddzap  8933  expmul  8934  expubnd  8945  neg1sqe1  8981  irec  8985  i4  8988  binom21  8996  bernneq  9002  bernneq2  9003  rei  9107  imi  9108
  Copyright terms: Public domain W3C validator