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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 7295 . 2  class  1
2 cc 7292 . 2  class  CC
31, 2wcel 1436 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  7424  1ex  7427  mulid1  7429  mulid2  7430  1cnd  7448  muladd11  7559  1p1times  7560  peano2cn  7561  peano2cnm  7692  0reALT  7723  pncan1  7799  npcan1  7800  kcnktkm1cn  7805  ine0  7816  mulm1  7822  mulsubfacd  7840  ixi  8001  inelr  8002  muleqadd  8076  recclap  8085  recap0  8091  recidap  8092  recidap2  8093  div1  8109  1div1e1  8110  diveqap1  8111  recdivap  8124  divdivap1  8129  divdivap2  8130  recdivap2  8131  conjmulap  8135  eqneg  8138  div2negap  8141  recreclt  8296  nn1m1nn  8375  nn1suc  8376  nnaddcl  8377  nnmulcl  8378  nnsub  8395  1m1e0  8426  neg1cn  8462  neg1ne0  8464  neg1ap0  8466  negneg1e1  8467  1pneg1e0  8468  1m0e1  8470  0p1e1  8471  1p0e1  8472  2m1e1  8474  3m1e2  8476  2p2e4  8477  1p2e3  8484  3p2e5  8491  3p3e6  8492  4p2e6  8493  4p3e7  8494  4p4e8  8495  5p2e7  8496  5p3e8  8497  5p4e9  8498  6p2e8  8499  6p3e9  8500  7p2e9  8501  1t1e1  8502  3t3e9  8507  neg1mulneg1e1  8561  1mhlfehlf  8567  8th4div3  8568  halfpm6th  8569  addltmul  8585  elnn0nn  8648  peano2z  8719  zlem1lt  8739  zltlem1  8740  nnaddm1cl  8744  elz2  8751  zextlt  8771  zeo  8784  peano5uzti  8787  numsuc  8822  numltc  8834  numsucc  8848  numaddc  8856  6p5lem  8878  5p5e10  8879  6p4e10  8880  7p3e10  8883  8p2e10  8888  10m1e9  8904  4t3lem  8905  7t4e28  8919  9t11e99  8938  decbin2  8949  uzp1  8984  peano2uzr  9005  uzaddcl  9006  qreccl  9059  iccf1o  9353  fz01en  9399  fztp  9422  fzsuc2  9423  fztpval  9427  fseq1m1p1  9439  elfzp1b  9441  fzoss2  9511  fzval3  9543  fzosplitsnm1  9548  fzo0to42pr  9559  fzosplitprm1  9573  fldiv4p1lem1div2  9640  flqdiv  9656  frecfzen2  9762  nn0ennn  9768  iseqm1  9802  iseqshft2  9807  monoord2  9811  isermono  9812  expival  9856  expcl  9872  m1expcl2  9876  expclzaplem  9878  expm1t  9882  1exp  9883  mulexpzap  9894  expadd  9896  expaddzap  9898  expmul  9899  expubnd  9911  neg1sqe1  9948  irec  9952  i4  9955  binom21  9964  bernneq  9971  bernneq2  9972  facndiv  10044  faclbnd6  10049  bcnp1n  10064  bcm1k  10065  bcp1nk  10067  bcn2  10069  bcp1m1  10070  bcpasc  10071  4bc3eq4  10078  hashfz  10126  hashfzo  10127  iseqcoll  10144  rei  10229  imi  10230  caucvgrelemrec  10308  recan  10438  iiserex  10621  serif0  10633  3dvdsdec  10747  3dvds2dec  10748  odd2np1lem  10754  odd2np1  10755  opoe  10777  omoe  10778  opeo  10779  omeo  10780  m1exp1  10783  n2dvdsm1  10795  flodddiv4  10816  gcdmultiple  10891  sqgcd  10900  nn0seqcvgd  10905  prmind2  10984  hashdvds  11079  phiprmpw  11080  phiprm  11081  ex-fl  11098
  Copyright terms: Public domain W3C validator