Axiom ax-1cn 8125

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

This axiom is referenced by:  0cn  8171  1ex  8174  mulrid  8176  mullid  8177  1cnd  8195  muladd11  8312  1p1times  8313  peano2cn  8314  peano2cnm  8445  0reALT  8476  pncan1  8556  npcan1  8557  kcnktkm1cn  8562  ine0  8573  mulm1  8579  mulsubfacd  8598  ixi  8763  inelr  8764  muleqadd  8848  recclap  8859  recap0  8865  recidap  8866  recidap2  8867  div1  8883  1div1e1  8884  diveqap1  8885  recdivap  8898  divdivap1  8903  divdivap2  8904  recdivap2  8905  conjmulap  8909  eqneg  8912  div2negap  8915  recreclt  9080  ofnegsub  9142  nn1m1nn  9161  nn1suc  9162  nnaddcl  9163  nnmulcl  9164  nnsub  9182  1m1e0  9212  neg1cn  9248  neg1ne0  9250  neg1ap0  9252  negneg1e1  9253  1pneg1e0  9254  1m0e1  9256  0p1e1  9257  1p0e1  9259  2m1e1  9261  3m1e2  9263  4m1e3  9264  5m1e4  9265  6m1e5  9266  7m1e6  9267  8m1e7  9268  9m1e8  9269  2p2e4  9270  1p2e3  9278  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  1t1e1  9296  3t3e9  9301  neg1mulneg1e1  9356  1mhlfehlf  9362  8th4div3  9363  halfpm6th  9364  addltmul  9381  elnn0nn  9444  peano2z  9515  zlem1lt  9536  zltlem1  9537  nnaddm1cl  9541  elz2  9551  zextlt  9572  zeo  9585  peano5uzti  9588  numsuc  9624  numltc  9636  numsucc  9650  numaddc  9658  6p5lem  9680  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  10m1e9  9706  4t3lem  9707  7t4e28  9721  9t11e99  9740  decbin2  9751  halfthird  9753  5recm6rec  9754  uzp1  9790  peano2uzr  9819  uzaddcl  9820  qreccl  9876  iccf1o  10239  fz01en  10288  fztp  10313  fzsuc2  10314  fztpval  10318  fseq1m1p1  10330  elfzp1b  10332  fz0to4untppr  10359  fzoss2  10409  fzval3  10450  fzosplitsnm1  10455  fzo0to42pr  10466  fzosplitprm1  10481  fldiv4p1lem1div2  10566  flqdiv  10584  frecfzen2  10690  nn0ennn  10696  xnn0nnen  10700  seq3m1  10736  seqshft2g  10745  monoord2  10749  ser3mono  10750  seqf1oglem1  10782  seqf1oglem2  10783  expcl  10820  m1expcl2  10824  expclzaplem  10826  expm1t  10830  1exp  10831  mulexpzap  10842  expadd  10844  expaddzap  10846  expmul  10847  expubnd  10859  neg1sqe1  10897  irec  10902  i4  10905  binom21  10915  bernneq  10923  bernneq2  10924  facndiv  11002  faclbnd6  11007  bcnp1n  11022  bcm1k  11023  bcp1nk  11025  bcn2  11027  bcp1m1  11028  bcpasc  11029  4bc3eq4  11036  hashfz  11086  hashfzo  11087  seq3coll  11107  swrds1  11253  swrdlsw  11254  wrdind  11307  wrd2ind  11308  rei  11477  imi  11478  caucvgrelemrec  11557  recan  11687  iserex  11917  serf0  11930  fsumm1  11995  fsump1  11999  telfsumo  12045  fsumparts  12049  hashiun  12057  binomlem  12062  binom  12063  binom1p  12064  binom11  12065  binom1dif  12066  bcxmas  12068  isumsplit  12070  isum1p  12071  arisum  12077  arisum2  12078  trireciplem  12079  geosergap  12085  geolim  12090  geolim2  12091  georeclim  12092  geo2sum  12093  geo2sum2  12094  0.999...  12100  geoihalfsum  12101  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodf1  12121  prodfclim1  12123  prodrbdclem  12150  fproddccvg  12151  prodmodclem2a  12155  fprodntrivap  12163  prodssdc  12168  fprodssdc  12169  esum  12241  ege2le3  12250  efexp  12261  efzval  12262  eftlub  12269  effsumlt  12271  ef4p  12273  tanval3ap  12293  efi4p  12296  tan0  12310  efival  12311  tanaddap  12318  cos2t  12329  cos2tsin  12330  ef01bndlem  12335  cos1bnd  12338  cos2bnd  12339  demoivreALT  12353  eirraplem  12356  3dvds  12443  3dvdsdec  12444  3dvds2dec  12445  odd2np1lem  12451  odd2np1  12452  opoe  12474  omoe  12475  opeo  12476  omeo  12477  m1exp1  12480  n2dvdsm1  12492  flodddiv4  12515  bitsfzo  12534  gcdmultiple  12609  sqgcd  12618  nn0seqcvgd  12631  prmind2  12710  hashdvds  12811  phiprmpw  12812  phiprm  12813  eulerthlemth  12822  sumhashdc  12938  fldivp1  12939  prmpwdvds  12946  pockthlem  12947  pockthi  12949  4sqlem11  12992  4sqlem19  13000  dec5nprm  13005  mulgnndir  13756  mulgneg2  13761  cnfld1  14605  zsssubrg  14618  mulgrhm2  14643  expcncf  15352  divcncfap  15357  hovercncf  15389  dvid  15438  dvidre  15440  dvexp  15454  dvexp2  15455  dveflem  15469  plyaddlem1  15490  plymullem1  15491  dvply1  15508  reeff1olem  15514  eulerid  15545  cos2pi  15547  sincosq3sgn  15571  sincosq4sgn  15572  cosq23lt0  15576  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  pigt3  15587  abssinper  15589  coskpi  15591  cosq34lt1  15593  logdivlti  15624  rpcxpp1  15649  rpcxpsqrt  15665  rprelogbdiv  15700  binom4  15722  wilthlem1  15723  0sgm  15728  1sgmprm  15737  1sgm2ppw  15738  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  zabsle1  15747  lgslem1  15748  lgslem2  15749  lgsfcl2  15754  lgsvalmod  15767  lgsneg  15772  lgsdilem  15775  lgsdir2lem1  15776  lgsdir2lem2  15777  lgsdir2lem3  15778  lgsdir2lem5  15780  lgsne0  15786  lgseisenlem1  15818  lgseisenlem2  15819  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2  15831  m1lgs  15833  2lgslem3c  15843  2lgsoddprmlem3c  15857  2lgsoddprmlem3d  15858  2sqlem10  15873  clwwlknonex2lem2  16308  ex-fl  16368  trilpolemeq1  16695