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

Axiom ax-1cn 7034
Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6994. (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 6947 . 2  class  1
2 cc 6944 . 2  class  CC
31, 2wcel 1409 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  7076  1ex  7079  mulid1  7081  mulid2  7082  1cnd  7100  muladd11  7206  1p1times  7207  peano2cn  7208  peano2cnm  7339  0reALT  7370  pncan1  7446  npcan1  7447  kcnktkm1cn  7451  ine0  7462  mulm1  7468  mulsubfacd  7486  ixi  7647  inelr  7648  muleqadd  7722  recclap  7731  recap0  7737  recidap  7738  recidap2  7739  div1  7753  1div1e1  7754  diveqap1  7755  recdivap  7768  divdivap1  7773  divdivap2  7774  recdivap2  7775  conjmulap  7779  eqneg  7782  div2negap  7785  recreclt  7940  nn1m1nn  8007  nn1suc  8008  nnaddcl  8009  nnmulcl  8010  nnsub  8027  1m1e0  8058  neg1cn  8094  neg1ne0  8096  neg1ap0  8098  negneg1e1  8099  1pneg1e0  8100  1m0e1  8102  0p1e1  8103  1p0e1  8104  2m1e1  8106  3m1e2  8108  2p2e4  8109  1p2e3  8116  3p2e5  8123  3p3e6  8124  4p2e6  8125  4p3e7  8126  4p4e8  8127  5p2e7  8128  5p3e8  8129  5p4e9  8130  6p2e8  8131  6p3e9  8132  7p2e9  8133  1t1e1  8134  3t3e9  8139  neg1mulneg1e1  8193  1mhlfehlf  8199  8th4div3  8200  halfpm6th  8201  addltmul  8217  elnn0nn  8280  peano2z  8337  zlem1lt  8357  zltlem1  8358  nnaddm1cl  8362  elz2  8369  zextlt  8389  zeo  8401  peano5uzti  8404  numsuc  8439  numltc  8451  numsucc  8465  numaddc  8473  6p5lem  8495  5p5e10  8496  6p4e10  8497  7p3e10  8500  8p2e10  8505  10m1e9  8521  4t3lem  8522  7t4e28  8536  9t11e99  8555  decbin2  8566  uzp1  8601  peano2uzr  8623  uzaddcl  8624  qreccl  8673  iccf1o  8972  fz01en  9018  fztp  9041  fzsuc2  9042  fztpval  9046  fseq1m1p1  9058  elfzp1b  9060  fzoss2  9129  fzval3  9161  fzosplitsnm1  9166  fzo0to42pr  9177  fzosplitprm1  9191  fldiv4p1lem1div2  9254  flqdiv  9270  frecfzen2  9367  nn0ennn  9372  iseqm1  9390  iseqshft2  9395  monoord2  9399  isermono  9400  expival  9421  expcl  9437  m1expcl2  9441  expclzaplem  9443  expm1t  9447  1exp  9448  mulexpzap  9459  expadd  9461  expaddzap  9463  expmul  9464  expubnd  9476  neg1sqe1  9513  irec  9517  i4  9520  binom21  9529  bernneq  9536  bernneq2  9537  facndiv  9606  faclbnd6  9611  bcnp1n  9626  bcm1k  9627  bcp1nk  9629  bcn2  9631  bcp1m1  9632  bcpasc  9633  4bc3eq4  9640  rei  9726  imi  9727  caucvgrelemrec  9805  recan  9935  iiserex  10089  serif0  10101  3dvdsdec  10175  3dvds2dec  10176  odd2np1lem  10182  odd2np1  10183  opoe  10206  omoe  10207  opeo  10208  omeo  10209  m1exp1  10212  n2dvdsm1  10224  nn0seqcvgd  10242  ex-fl  10258
  Copyright terms: Public domain W3C validator