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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 6712 . 2  1
2 cc 6709 . 2  CC
31, 2wcel 1390 1  1  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  6817  1ex  6820  mulid1  6822  mulid2  6823  1cnd  6841  muladd11  6943  1p1times  6944  peano2cn  6945  peano2cnm  7073  0reALT  7104  pncan1  7171  npcan1  7172  kcnktkm1cn  7176  ine0  7187  mulm1  7193  mulsubfacd  7211  ixi  7367  inelr  7368  muleqadd  7431  recclap  7440  recap0  7446  recidap  7447  recidap2  7448  div1  7462  1div1e1  7463  diveqap1  7464  recdivap  7476  divdivap1  7481  divdivap2  7482  recdivap2  7483  conjmulap  7487  eqneg  7490  div2negap  7493  recreclt  7647  nn1m1nn  7713  nn1suc  7714  nnaddcl  7715  nnmulcl  7716  nnsub  7733  1m1e0  7764  neg1cn  7800  neg1ne0  7802  neg1ap0  7804  negneg1e1  7805  1pneg1e0  7806  1m0e1  7808  0p1e1  7809  1p0e1  7810  2m1e1  7812  3m1e2  7814  2p2e4  7815  1p2e3  7822  3p2e5  7830  3p3e6  7831  4p2e6  7832  4p3e7  7833  4p4e8  7834  5p2e7  7835  5p3e8  7836  5p4e9  7837  5p5e10  7838  6p2e8  7839  6p3e9  7840  6p4e10  7841  7p2e9  7842  7p3e10  7843  8p2e10  7844  1t1e1  7845  3t3e9  7850  neg1mulneg1e1  7915  1mhlfehlf  7920  8th4div3  7921  halfpm6th  7922  addltmul  7938  elnn0nn  8000  peano2z  8057  zlem1lt  8076  zltlem1  8077  nnaddm1cl  8081  elz2  8088  zextlt  8108  zeo  8119  peano5uzti  8122  numsuc  8155  numltc  8163  numsucc  8169  numaddc  8178  6p5lem  8192  4t3lem  8214  7t4e28  8227  decbin2  8247  uzp1  8282  peano2uzr  8304  uzaddcl  8305  qreccl  8351  iccf1o  8642  fz01en  8687  fztp  8710  fzsuc2  8711  fztpval  8715  fseq1m1p1  8727  elfzp1b  8729  fzoss2  8798  fzval3  8830  fzosplitsnm1  8835  fzo0to42pr  8846  fzosplitprm1  8860  frecfzen2  8885  nn0ennn  8890  expival  8911  expcl  8927  m1expcl2  8931  expclzaplem  8933  expm1t  8937  1exp  8938  mulexpzap  8949  expadd  8951  expaddzap  8953  expmul  8954  expubnd  8965  neg1sqe1  9001  irec  9005  i4  9008  binom21  9016  bernneq  9022  bernneq2  9023  rei  9127  imi  9128
  Copyright terms: Public domain W3C validator