Axiom ax-1cn 8025

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

This axiom is referenced by:  0cn  8071  1ex  8074  mulrid  8076  mullid  8077  1cnd  8095  muladd11  8212  1p1times  8213  peano2cn  8214  peano2cnm  8345  0reALT  8376  pncan1  8456  npcan1  8457  kcnktkm1cn  8462  ine0  8473  mulm1  8479  mulsubfacd  8498  ixi  8663  inelr  8664  muleqadd  8748  recclap  8759  recap0  8765  recidap  8766  recidap2  8767  div1  8783  1div1e1  8784  diveqap1  8785  recdivap  8798  divdivap1  8803  divdivap2  8804  recdivap2  8805  conjmulap  8809  eqneg  8812  div2negap  8815  recreclt  8980  ofnegsub  9042  nn1m1nn  9061  nn1suc  9062  nnaddcl  9063  nnmulcl  9064  nnsub  9082  1m1e0  9112  neg1cn  9148  neg1ne0  9150  neg1ap0  9152  negneg1e1  9153  1pneg1e0  9154  1m0e1  9156  0p1e1  9157  1p0e1  9159  2m1e1  9161  3m1e2  9163  4m1e3  9164  5m1e4  9165  6m1e5  9166  7m1e6  9167  8m1e7  9168  9m1e8  9169  2p2e4  9170  1p2e3  9178  3p2e5  9185  3p3e6  9186  4p2e6  9187  4p3e7  9188  4p4e8  9189  5p2e7  9190  5p3e8  9191  5p4e9  9192  6p2e8  9193  6p3e9  9194  7p2e9  9195  1t1e1  9196  3t3e9  9201  neg1mulneg1e1  9256  1mhlfehlf  9262  8th4div3  9263  halfpm6th  9264  addltmul  9281  elnn0nn  9344  peano2z  9415  zlem1lt  9436  zltlem1  9437  nnaddm1cl  9441  elz2  9451  zextlt  9472  zeo  9485  peano5uzti  9488  numsuc  9524  numltc  9536  numsucc  9550  numaddc  9558  6p5lem  9580  5p5e10  9581  6p4e10  9582  7p3e10  9585  8p2e10  9590  10m1e9  9606  4t3lem  9607  7t4e28  9621  9t11e99  9640  decbin2  9651  halfthird  9653  5recm6rec  9654  uzp1  9689  peano2uzr  9713  uzaddcl  9714  qreccl  9770  iccf1o  10133  fz01en  10182  fztp  10207  fzsuc2  10208  fztpval  10212  fseq1m1p1  10224  elfzp1b  10226  fz0to4untppr  10253  fzoss2  10303  fzval3  10340  fzosplitsnm1  10345  fzo0to42pr  10356  fzosplitprm1  10370  fldiv4p1lem1div2  10455  flqdiv  10473  frecfzen2  10579  nn0ennn  10585  xnn0nnen  10589  seq3m1  10625  seqshft2g  10634  monoord2  10638  ser3mono  10639  seqf1oglem1  10671  seqf1oglem2  10672  expcl  10709  m1expcl2  10713  expclzaplem  10715  expm1t  10719  1exp  10720  mulexpzap  10731  expadd  10733  expaddzap  10735  expmul  10736  expubnd  10748  neg1sqe1  10786  irec  10791  i4  10794  binom21  10804  bernneq  10812  bernneq2  10813  facndiv  10891  faclbnd6  10896  bcnp1n  10911  bcm1k  10912  bcp1nk  10914  bcn2  10916  bcp1m1  10917  bcpasc  10918  4bc3eq4  10925  hashfz  10973  hashfzo  10974  seq3coll  10994  swrds1  11129  swrdlsw  11130  rei  11254  imi  11255  caucvgrelemrec  11334  recan  11464  iserex  11694  serf0  11707  fsumm1  11771  fsump1  11775  telfsumo  11821  fsumparts  11825  hashiun  11833  binomlem  11838  binom  11839  binom1p  11840  binom11  11841  binom1dif  11842  bcxmas  11844  isumsplit  11846  isum1p  11847  arisum  11853  arisum2  11854  trireciplem  11855  geosergap  11861  geolim  11866  geolim2  11867  georeclim  11868  geo2sum  11869  geo2sum2  11870  0.999...  11876  geoihalfsum  11877  mertenslemi1  11890  mertenslem2  11891  mertensabs  11892  prodf1  11897  prodfclim1  11899  prodrbdclem  11926  fproddccvg  11927  prodmodclem2a  11931  fprodntrivap  11939  prodssdc  11944  fprodssdc  11945  esum  12017  ege2le3  12026  efexp  12037  efzval  12038  eftlub  12045  effsumlt  12047  ef4p  12049  tanval3ap  12069  efi4p  12072  tan0  12086  efival  12087  tanaddap  12094  cos2t  12105  cos2tsin  12106  ef01bndlem  12111  cos1bnd  12114  cos2bnd  12115  demoivreALT  12129  eirraplem  12132  3dvds  12219  3dvdsdec  12220  3dvds2dec  12221  odd2np1lem  12227  odd2np1  12228  opoe  12250  omoe  12251  opeo  12252  omeo  12253  m1exp1  12256  n2dvdsm1  12268  flodddiv4  12291  bitsfzo  12310  gcdmultiple  12385  sqgcd  12394  nn0seqcvgd  12407  prmind2  12486  hashdvds  12587  phiprmpw  12588  phiprm  12589  eulerthlemth  12598  sumhashdc  12714  fldivp1  12715  prmpwdvds  12722  pockthlem  12723  pockthi  12725  4sqlem11  12768  4sqlem19  12776  dec5nprm  12781  mulgnndir  13531  mulgneg2  13536  cnfld1  14378  zsssubrg  14391  mulgrhm2  14416  expcncf  15125  divcncfap  15130  hovercncf  15162  dvid  15211  dvidre  15213  dvexp  15227  dvexp2  15228  dveflem  15242  plyaddlem1  15263  plymullem1  15264  dvply1  15281  reeff1olem  15287  eulerid  15318  cos2pi  15320  sincosq3sgn  15344  sincosq4sgn  15345  cosq23lt0  15349  tangtx  15354  sincos4thpi  15356  sincos6thpi  15358  pigt3  15360  abssinper  15362  coskpi  15364  cosq34lt1  15366  logdivlti  15397  rpcxpp1  15422  rpcxpsqrt  15438  rprelogbdiv  15473  binom4  15495  wilthlem1  15496  0sgm  15501  1sgmprm  15510  1sgm2ppw  15511  mersenne  15513  perfect1  15514  perfectlem1  15515  perfectlem2  15516  perfect  15517  zabsle1  15520  lgslem1  15521  lgslem2  15522  lgsfcl2  15527  lgsvalmod  15540  lgsneg  15545  lgsdilem  15548  lgsdir2lem1  15549  lgsdir2lem2  15550  lgsdir2lem3  15551  lgsdir2lem5  15553  lgsne0  15559  lgseisenlem1  15591  lgseisenlem2  15592  lgseisen  15595  lgsquadlem1  15598  lgsquadlem2  15599  lgsquad2lem1  15602  lgsquad2  15604  m1lgs  15606  2lgslem3c  15616  2lgsoddprmlem3c  15630  2lgsoddprmlem3d  15631  2sqlem10  15646  ex-fl  15735  trilpolemeq1  16053