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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 6888 . 2 class 1
2 cc 6885 . 2 class
31, 2wcel 1393 1 wff 1 ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7017  1ex  7020  mulid1  7022  mulid2  7023  1cnd  7041  muladd11  7144  1p1times  7145  peano2cn  7146  peano2cnm  7275  0reALT  7306  pncan1  7373  npcan1  7374  kcnktkm1cn  7378  ine0  7389  mulm1  7395  mulsubfacd  7413  ixi  7572  inelr  7573  muleqadd  7647  recclap  7656  recap0  7662  recidap  7663  recidap2  7664  div1  7678  1div1e1  7679  diveqap1  7680  recdivap  7692  divdivap1  7697  divdivap2  7698  recdivap2  7699  conjmulap  7703  eqneg  7706  div2negap  7709  recreclt  7864  nn1m1nn  7930  nn1suc  7931  nnaddcl  7932  nnmulcl  7933  nnsub  7950  1m1e0  7982  neg1cn  8020  neg1ne0  8022  neg1ap0  8024  negneg1e1  8025  1pneg1e0  8026  1m0e1  8028  0p1e1  8029  1p0e1  8030  2m1e1  8032  3m1e2  8034  2p2e4  8035  1p2e3  8042  3p2e5  8050  3p3e6  8051  4p2e6  8052  4p3e7  8053  4p4e8  8054  5p2e7  8055  5p3e8  8056  5p4e9  8057  5p5e10  8058  6p2e8  8059  6p3e9  8060  6p4e10  8061  7p2e9  8062  7p3e10  8063  8p2e10  8064  1t1e1  8065  3t3e9  8070  neg1mulneg1e1  8135  1mhlfehlf  8141  8th4div3  8142  halfpm6th  8143  addltmul  8159  elnn0nn  8222  peano2z  8279  zlem1lt  8298  zltlem1  8299  nnaddm1cl  8303  elz2  8310  zextlt  8330  zeo  8341  peano5uzti  8344  numsuc  8377  numltc  8385  numsucc  8391  numaddc  8400  6p5lem  8414  4t3lem  8436  7t4e28  8449  decbin2  8469  uzp1  8504  peano2uzr  8526  uzaddcl  8527  qreccl  8574  iccf1o  8870  fz01en  8915  fztp  8938  fzsuc2  8939  fztpval  8943  fseq1m1p1  8955  elfzp1b  8957  fzoss2  9026  fzval3  9058  fzosplitsnm1  9063  fzo0to42pr  9074  fzosplitprm1  9088  fldiv4p1lem1div2  9145  frecfzen2  9178  nn0ennn  9183  iseqm1  9201  iseqshft2  9206  monoord2  9210  isermono  9211  expival  9231  expcl  9247  m1expcl2  9251  expclzaplem  9253  expm1t  9257  1exp  9258  mulexpzap  9269  expadd  9271  expaddzap  9273  expmul  9274  expubnd  9285  neg1sqe1  9322  irec  9326  i4  9329  binom21  9337  bernneq  9343  bernneq2  9344  rei  9473  imi  9474  caucvgrelemrec  9552  recan  9679  iiserex  9832  serif0  9844  nn0seqcvgd  9853  ex-fl  9868
  Copyright terms: Public domain W3C validator