Axiom ax-1cn 7972

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7928. (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 7880	. 2 class 1
2		cc 7877	. 2 class ℂ
3	1, 2	wcel 2167	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  8018  1ex  8021  mulrid  8023  mullid  8024  1cnd  8042  muladd11  8159  1p1times  8160  peano2cn  8161  peano2cnm  8292  0reALT  8323  pncan1  8403  npcan1  8404  kcnktkm1cn  8409  ine0  8420  mulm1  8426  mulsubfacd  8445  ixi  8610  inelr  8611  muleqadd  8695  recclap  8706  recap0  8712  recidap  8713  recidap2  8714  div1  8730  1div1e1  8731  diveqap1  8732  recdivap  8745  divdivap1  8750  divdivap2  8751  recdivap2  8752  conjmulap  8756  eqneg  8759  div2negap  8762  recreclt  8927  ofnegsub  8989  nn1m1nn  9008  nn1suc  9009  nnaddcl  9010  nnmulcl  9011  nnsub  9029  1m1e0  9059  neg1cn  9095  neg1ne0  9097  neg1ap0  9099  negneg1e1  9100  1pneg1e0  9101  1m0e1  9103  0p1e1  9104  1p0e1  9106  2m1e1  9108  3m1e2  9110  4m1e3  9111  5m1e4  9112  6m1e5  9113  7m1e6  9114  8m1e7  9115  9m1e8  9116  2p2e4  9117  1p2e3  9125  3p2e5  9132  3p3e6  9133  4p2e6  9134  4p3e7  9135  4p4e8  9136  5p2e7  9137  5p3e8  9138  5p4e9  9139  6p2e8  9140  6p3e9  9141  7p2e9  9142  1t1e1  9143  3t3e9  9148  neg1mulneg1e1  9203  1mhlfehlf  9209  8th4div3  9210  halfpm6th  9211  addltmul  9228  elnn0nn  9291  peano2z  9362  zlem1lt  9382  zltlem1  9383  nnaddm1cl  9387  elz2  9397  zextlt  9418  zeo  9431  peano5uzti  9434  numsuc  9470  numltc  9482  numsucc  9496  numaddc  9504  6p5lem  9526  5p5e10  9527  6p4e10  9528  7p3e10  9531  8p2e10  9536  10m1e9  9552  4t3lem  9553  7t4e28  9567  9t11e99  9586  decbin2  9597  halfthird  9599  5recm6rec  9600  uzp1  9635  peano2uzr  9659  uzaddcl  9660  qreccl  9716  iccf1o  10079  fz01en  10128  fztp  10153  fzsuc2  10154  fztpval  10158  fseq1m1p1  10170  elfzp1b  10172  fz0to4untppr  10199  fzoss2  10248  fzval3  10280  fzosplitsnm1  10285  fzo0to42pr  10296  fzosplitprm1  10310  fldiv4p1lem1div2  10395  flqdiv  10413  frecfzen2  10519  nn0ennn  10525  xnn0nnen  10529  seq3m1  10565  seqshft2g  10574  monoord2  10578  ser3mono  10579  seqf1oglem1  10611  seqf1oglem2  10612  expcl  10649  m1expcl2  10653  expclzaplem  10655  expm1t  10659  1exp  10660  mulexpzap  10671  expadd  10673  expaddzap  10675  expmul  10676  expubnd  10688  neg1sqe1  10726  irec  10731  i4  10734  binom21  10744  bernneq  10752  bernneq2  10753  facndiv  10831  faclbnd6  10836  bcnp1n  10851  bcm1k  10852  bcp1nk  10854  bcn2  10856  bcp1m1  10857  bcpasc  10858  4bc3eq4  10865  hashfz  10913  hashfzo  10914  seq3coll  10934  rei  11064  imi  11065  caucvgrelemrec  11144  recan  11274  iserex  11504  serf0  11517  fsumm1  11581  fsump1  11585  telfsumo  11631  fsumparts  11635  hashiun  11643  binomlem  11648  binom  11649  binom1p  11650  binom11  11651  binom1dif  11652  bcxmas  11654  isumsplit  11656  isum1p  11657  arisum  11663  arisum2  11664  trireciplem  11665  geosergap  11671  geolim  11676  geolim2  11677  georeclim  11678  geo2sum  11679  geo2sum2  11680  0.999...  11686  geoihalfsum  11687  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodf1  11707  prodfclim1  11709  prodrbdclem  11736  fproddccvg  11737  prodmodclem2a  11741  fprodntrivap  11749  prodssdc  11754  fprodssdc  11755  esum  11827  ege2le3  11836  efexp  11847  efzval  11848  eftlub  11855  effsumlt  11857  ef4p  11859  tanval3ap  11879  efi4p  11882  tan0  11896  efival  11897  tanaddap  11904  cos2t  11915  cos2tsin  11916  ef01bndlem  11921  cos1bnd  11924  cos2bnd  11925  demoivreALT  11939  eirraplem  11942  3dvds  12029  3dvdsdec  12030  3dvds2dec  12031  odd2np1lem  12037  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  m1exp1  12066  n2dvdsm1  12078  flodddiv4  12101  bitsfzo  12119  gcdmultiple  12187  sqgcd  12196  nn0seqcvgd  12209  prmind2  12288  hashdvds  12389  phiprmpw  12390  phiprm  12391  eulerthlemth  12400  sumhashdc  12516  fldivp1  12517  prmpwdvds  12524  pockthlem  12525  pockthi  12527  4sqlem11  12570  4sqlem19  12578  dec5nprm  12583  mulgnndir  13281  mulgneg2  13286  cnfld1  14128  zsssubrg  14141  mulgrhm2  14166  expcncf  14845  divcncfap  14850  hovercncf  14882  dvid  14931  dvidre  14933  dvexp  14947  dvexp2  14948  dveflem  14962  plyaddlem1  14983  plymullem1  14984  dvply1  15001  reeff1olem  15007  eulerid  15038  cos2pi  15040  sincosq3sgn  15064  sincosq4sgn  15065  cosq23lt0  15069  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  pigt3  15080  abssinper  15082  coskpi  15084  cosq34lt1  15086  logdivlti  15117  rpcxpp1  15142  rpcxpsqrt  15158  rprelogbdiv  15193  binom4  15215  wilthlem1  15216  0sgm  15221  1sgmprm  15230  1sgm2ppw  15231  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  zabsle1  15240  lgslem1  15241  lgslem2  15242  lgsfcl2  15247  lgsvalmod  15260  lgsneg  15265  lgsdilem  15268  lgsdir2lem1  15269  lgsdir2lem2  15270  lgsdir2lem3  15271  lgsdir2lem5  15273  lgsne0  15279  lgseisenlem1  15311  lgseisenlem2  15312  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2  15324  m1lgs  15326  2lgslem3c  15336  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  2sqlem10  15366  ex-fl  15371  trilpolemeq1  15684