Axiom ax-1cn 7638

Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7596. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	⊢ 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 7548	. 2 class 1
2		cc 7545	. 2 class ℂ
3	1, 2	wcel 1463	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  7682  1ex  7685  mulid1  7687  mulid2  7688  1cnd  7706  muladd11  7818  1p1times  7819  peano2cn  7820  peano2cnm  7951  0reALT  7982  pncan1  8058  npcan1  8059  kcnktkm1cn  8064  ine0  8075  mulm1  8081  mulsubfacd  8099  ixi  8263  inelr  8264  muleqadd  8342  recclap  8352  recap0  8358  recidap  8359  recidap2  8360  div1  8376  1div1e1  8377  diveqap1  8378  recdivap  8391  divdivap1  8396  divdivap2  8397  recdivap2  8398  conjmulap  8402  eqneg  8405  div2negap  8408  recreclt  8568  nn1m1nn  8648  nn1suc  8649  nnaddcl  8650  nnmulcl  8651  nnsub  8669  1m1e0  8699  neg1cn  8735  neg1ne0  8737  neg1ap0  8739  negneg1e1  8740  1pneg1e0  8741  1m0e1  8743  0p1e1  8744  1p0e1  8746  2m1e1  8748  3m1e2  8750  2p2e4  8751  1p2e3  8758  3p2e5  8765  3p3e6  8766  4p2e6  8767  4p3e7  8768  4p4e8  8769  5p2e7  8770  5p3e8  8771  5p4e9  8772  6p2e8  8773  6p3e9  8774  7p2e9  8775  1t1e1  8776  3t3e9  8781  neg1mulneg1e1  8836  1mhlfehlf  8842  8th4div3  8843  halfpm6th  8844  addltmul  8860  elnn0nn  8923  peano2z  8994  zlem1lt  9014  zltlem1  9015  nnaddm1cl  9019  elz2  9026  zextlt  9047  zeo  9060  peano5uzti  9063  numsuc  9099  numltc  9111  numsucc  9125  numaddc  9133  6p5lem  9155  5p5e10  9156  6p4e10  9157  7p3e10  9160  8p2e10  9165  10m1e9  9181  4t3lem  9182  7t4e28  9196  9t11e99  9215  decbin2  9226  uzp1  9261  peano2uzr  9282  uzaddcl  9283  qreccl  9336  iccf1o  9680  fz01en  9726  fztp  9751  fzsuc2  9752  fztpval  9756  fseq1m1p1  9768  elfzp1b  9770  fzoss2  9842  fzval3  9874  fzosplitsnm1  9879  fzo0to42pr  9890  fzosplitprm1  9904  fldiv4p1lem1div2  9971  flqdiv  9987  frecfzen2  10093  nn0ennn  10099  seq3m1  10134  monoord2  10143  ser3mono  10144  expcl  10204  m1expcl2  10208  expclzaplem  10210  expm1t  10214  1exp  10215  mulexpzap  10226  expadd  10228  expaddzap  10230  expmul  10231  expubnd  10243  neg1sqe1  10280  irec  10285  i4  10288  binom21  10297  bernneq  10305  bernneq2  10306  facndiv  10378  faclbnd6  10383  bcnp1n  10398  bcm1k  10399  bcp1nk  10401  bcn2  10403  bcp1m1  10404  bcpasc  10405  4bc3eq4  10412  hashfz  10460  hashfzo  10461  seq3coll  10478  rei  10564  imi  10565  caucvgrelemrec  10643  recan  10773  iserex  11000  serf0  11013  fsumm1  11077  fsump1  11081  telfsumo  11127  fsumparts  11131  hashiun  11139  binomlem  11144  binom  11145  binom1p  11146  binom11  11147  binom1dif  11148  bcxmas  11150  isumsplit  11152  isum1p  11153  arisum  11159  arisum2  11160  trireciplem  11161  geosergap  11167  geolim  11172  geolim2  11173  georeclim  11174  geo2sum  11175  geo2sum2  11176  0.999...  11182  geoihalfsum  11183  mertenslemi1  11196  mertenslem2  11197  mertensabs  11198  esum  11219  ege2le3  11228  efexp  11239  efzval  11240  eftlub  11247  effsumlt  11249  ef4p  11251  tanval3ap  11272  efi4p  11275  tan0  11289  efival  11290  tanaddap  11297  cos2t  11308  cos2tsin  11309  ef01bndlem  11314  cos1bnd  11317  cos2bnd  11318  demoivreALT  11330  eirraplem  11331  3dvdsdec  11410  3dvds2dec  11411  odd2np1lem  11417  odd2np1  11418  opoe  11440  omoe  11441  opeo  11442  omeo  11443  m1exp1  11446  n2dvdsm1  11458  flodddiv4  11479  gcdmultiple  11554  sqgcd  11563  nn0seqcvgd  11568  prmind2  11647  hashdvds  11742  phiprmpw  11743  phiprm  11744  expcncf  12578  dvid  12617  ex-fl  12630  trilpolemeq1  12925