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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 6948 . 2 class 1
2 cc 6945 . 2 class
31, 2wcel 1409 1 wff 1 ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7077  1ex  7080  mulid1  7082  mulid2  7083  1cnd  7101  muladd11  7207  1p1times  7208  peano2cn  7209  peano2cnm  7340  0reALT  7371  pncan1  7447  npcan1  7448  kcnktkm1cn  7452  ine0  7463  mulm1  7469  mulsubfacd  7487  ixi  7648  inelr  7649  muleqadd  7723  recclap  7732  recap0  7738  recidap  7739  recidap2  7740  div1  7754  1div1e1  7755  diveqap1  7756  recdivap  7769  divdivap1  7774  divdivap2  7775  recdivap2  7776  conjmulap  7780  eqneg  7783  div2negap  7786  recreclt  7941  nn1m1nn  8008  nn1suc  8009  nnaddcl  8010  nnmulcl  8011  nnsub  8028  1m1e0  8059  neg1cn  8095  neg1ne0  8097  neg1ap0  8099  negneg1e1  8100  1pneg1e0  8101  1m0e1  8103  0p1e1  8104  1p0e1  8105  2m1e1  8107  3m1e2  8109  2p2e4  8110  1p2e3  8117  3p2e5  8124  3p3e6  8125  4p2e6  8126  4p3e7  8127  4p4e8  8128  5p2e7  8129  5p3e8  8130  5p4e9  8131  6p2e8  8132  6p3e9  8133  7p2e9  8134  1t1e1  8135  3t3e9  8140  neg1mulneg1e1  8194  1mhlfehlf  8200  8th4div3  8201  halfpm6th  8202  addltmul  8218  elnn0nn  8281  peano2z  8338  zlem1lt  8358  zltlem1  8359  nnaddm1cl  8363  elz2  8370  zextlt  8390  zeo  8402  peano5uzti  8405  numsuc  8440  numltc  8452  numsucc  8466  numaddc  8474  6p5lem  8496  5p5e10  8497  6p4e10  8498  7p3e10  8501  8p2e10  8506  10m1e9  8522  4t3lem  8523  7t4e28  8537  9t11e99  8556  decbin2  8567  uzp1  8602  peano2uzr  8624  uzaddcl  8625  qreccl  8674  iccf1o  8973  fz01en  9019  fztp  9042  fzsuc2  9043  fztpval  9047  fseq1m1p1  9059  elfzp1b  9061  fzoss2  9130  fzval3  9162  fzosplitsnm1  9167  fzo0to42pr  9178  fzosplitprm1  9192  fldiv4p1lem1div2  9255  flqdiv  9271  frecfzen2  9368  nn0ennn  9373  iseqm1  9391  iseqshft2  9396  monoord2  9400  isermono  9401  expival  9422  expcl  9438  m1expcl2  9442  expclzaplem  9444  expm1t  9448  1exp  9449  mulexpzap  9460  expadd  9462  expaddzap  9464  expmul  9465  expubnd  9477  neg1sqe1  9514  irec  9518  i4  9521  binom21  9530  bernneq  9537  bernneq2  9538  facndiv  9607  faclbnd6  9612  bcnp1n  9627  bcm1k  9628  bcp1nk  9630  bcn2  9632  bcp1m1  9633  bcpasc  9634  4bc3eq4  9641  rei  9727  imi  9728  caucvgrelemrec  9806  recan  9936  iiserex  10090  serif0  10102  3dvdsdec  10176  3dvds2dec  10177  odd2np1lem  10183  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210  m1exp1  10213  n2dvdsm1  10225  flodddiv4  10246  nn0seqcvgd  10263  ex-fl  10279
  Copyright terms: Public domain W3C validator