Axiom ax-1cn 8113

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

This axiom is referenced by:  0cn  8159  1ex  8162  mulrid  8164  mullid  8165  1cnd  8183  muladd11  8300  1p1times  8301  peano2cn  8302  peano2cnm  8433  0reALT  8464  pncan1  8544  npcan1  8545  kcnktkm1cn  8550  ine0  8561  mulm1  8567  mulsubfacd  8586  ixi  8751  inelr  8752  muleqadd  8836  recclap  8847  recap0  8853  recidap  8854  recidap2  8855  div1  8871  1div1e1  8872  diveqap1  8873  recdivap  8886  divdivap1  8891  divdivap2  8892  recdivap2  8893  conjmulap  8897  eqneg  8900  div2negap  8903  recreclt  9068  ofnegsub  9130  nn1m1nn  9149  nn1suc  9150  nnaddcl  9151  nnmulcl  9152  nnsub  9170  1m1e0  9200  neg1cn  9236  neg1ne0  9238  neg1ap0  9240  negneg1e1  9241  1pneg1e0  9242  1m0e1  9244  0p1e1  9245  1p0e1  9247  2m1e1  9249  3m1e2  9251  4m1e3  9252  5m1e4  9253  6m1e5  9254  7m1e6  9255  8m1e7  9256  9m1e8  9257  2p2e4  9258  1p2e3  9266  3p2e5  9273  3p3e6  9274  4p2e6  9275  4p3e7  9276  4p4e8  9277  5p2e7  9278  5p3e8  9279  5p4e9  9280  6p2e8  9281  6p3e9  9282  7p2e9  9283  1t1e1  9284  3t3e9  9289  neg1mulneg1e1  9344  1mhlfehlf  9350  8th4div3  9351  halfpm6th  9352  addltmul  9369  elnn0nn  9432  peano2z  9503  zlem1lt  9524  zltlem1  9525  nnaddm1cl  9529  elz2  9539  zextlt  9560  zeo  9573  peano5uzti  9576  numsuc  9612  numltc  9624  numsucc  9638  numaddc  9646  6p5lem  9668  5p5e10  9669  6p4e10  9670  7p3e10  9673  8p2e10  9678  10m1e9  9694  4t3lem  9695  7t4e28  9709  9t11e99  9728  decbin2  9739  halfthird  9741  5recm6rec  9742  uzp1  9778  peano2uzr  9807  uzaddcl  9808  qreccl  9864  iccf1o  10227  fz01en  10276  fztp  10301  fzsuc2  10302  fztpval  10306  fseq1m1p1  10318  elfzp1b  10320  fz0to4untppr  10347  fzoss2  10397  fzval3  10437  fzosplitsnm1  10442  fzo0to42pr  10453  fzosplitprm1  10468  fldiv4p1lem1div2  10553  flqdiv  10571  frecfzen2  10677  nn0ennn  10683  xnn0nnen  10687  seq3m1  10723  seqshft2g  10732  monoord2  10736  ser3mono  10737  seqf1oglem1  10769  seqf1oglem2  10770  expcl  10807  m1expcl2  10811  expclzaplem  10813  expm1t  10817  1exp  10818  mulexpzap  10829  expadd  10831  expaddzap  10833  expmul  10834  expubnd  10846  neg1sqe1  10884  irec  10889  i4  10892  binom21  10902  bernneq  10910  bernneq2  10911  facndiv  10989  faclbnd6  10994  bcnp1n  11009  bcm1k  11010  bcp1nk  11012  bcn2  11014  bcp1m1  11015  bcpasc  11016  4bc3eq4  11023  hashfz  11072  hashfzo  11073  seq3coll  11093  swrds1  11236  swrdlsw  11237  wrdind  11290  wrd2ind  11291  rei  11447  imi  11448  caucvgrelemrec  11527  recan  11657  iserex  11887  serf0  11900  fsumm1  11964  fsump1  11968  telfsumo  12014  fsumparts  12018  hashiun  12026  binomlem  12031  binom  12032  binom1p  12033  binom11  12034  binom1dif  12035  bcxmas  12037  isumsplit  12039  isum1p  12040  arisum  12046  arisum2  12047  trireciplem  12048  geosergap  12054  geolim  12059  geolim2  12060  georeclim  12061  geo2sum  12062  geo2sum2  12063  0.999...  12069  geoihalfsum  12070  mertenslemi1  12083  mertenslem2  12084  mertensabs  12085  prodf1  12090  prodfclim1  12092  prodrbdclem  12119  fproddccvg  12120  prodmodclem2a  12124  fprodntrivap  12132  prodssdc  12137  fprodssdc  12138  esum  12210  ege2le3  12219  efexp  12230  efzval  12231  eftlub  12238  effsumlt  12240  ef4p  12242  tanval3ap  12262  efi4p  12265  tan0  12279  efival  12280  tanaddap  12287  cos2t  12298  cos2tsin  12299  ef01bndlem  12304  cos1bnd  12307  cos2bnd  12308  demoivreALT  12322  eirraplem  12325  3dvds  12412  3dvdsdec  12413  3dvds2dec  12414  odd2np1lem  12420  odd2np1  12421  opoe  12443  omoe  12444  opeo  12445  omeo  12446  m1exp1  12449  n2dvdsm1  12461  flodddiv4  12484  bitsfzo  12503  gcdmultiple  12578  sqgcd  12587  nn0seqcvgd  12600  prmind2  12679  hashdvds  12780  phiprmpw  12781  phiprm  12782  eulerthlemth  12791  sumhashdc  12907  fldivp1  12908  prmpwdvds  12915  pockthlem  12916  pockthi  12918  4sqlem11  12961  4sqlem19  12969  dec5nprm  12974  mulgnndir  13725  mulgneg2  13730  cnfld1  14573  zsssubrg  14586  mulgrhm2  14611  expcncf  15320  divcncfap  15325  hovercncf  15357  dvid  15406  dvidre  15408  dvexp  15422  dvexp2  15423  dveflem  15437  plyaddlem1  15458  plymullem1  15459  dvply1  15476  reeff1olem  15482  eulerid  15513  cos2pi  15515  sincosq3sgn  15539  sincosq4sgn  15540  cosq23lt0  15544  tangtx  15549  sincos4thpi  15551  sincos6thpi  15553  pigt3  15555  abssinper  15557  coskpi  15559  cosq34lt1  15561  logdivlti  15592  rpcxpp1  15617  rpcxpsqrt  15633  rprelogbdiv  15668  binom4  15690  wilthlem1  15691  0sgm  15696  1sgmprm  15705  1sgm2ppw  15706  mersenne  15708  perfect1  15709  perfectlem1  15710  perfectlem2  15711  perfect  15712  zabsle1  15715  lgslem1  15716  lgslem2  15717  lgsfcl2  15722  lgsvalmod  15735  lgsneg  15740  lgsdilem  15743  lgsdir2lem1  15744  lgsdir2lem2  15745  lgsdir2lem3  15746  lgsdir2lem5  15748  lgsne0  15754  lgseisenlem1  15786  lgseisenlem2  15787  lgseisen  15790  lgsquadlem1  15793  lgsquadlem2  15794  lgsquad2lem1  15797  lgsquad2  15799  m1lgs  15801  2lgslem3c  15811  2lgsoddprmlem3c  15825  2lgsoddprmlem3d  15826  2sqlem10  15841  clwwlknonex2lem2  16223  ex-fl  16231  trilpolemeq1  16554