Axiom ax-1cn 8124

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

This axiom is referenced by:  0cn  8170  1ex  8173  mulrid  8175  mullid  8176  1cnd  8194  muladd11  8311  1p1times  8312  peano2cn  8313  peano2cnm  8444  0reALT  8475  pncan1  8555  npcan1  8556  kcnktkm1cn  8561  ine0  8572  mulm1  8578  mulsubfacd  8597  ixi  8762  inelr  8763  muleqadd  8847  recclap  8858  recap0  8864  recidap  8865  recidap2  8866  div1  8882  1div1e1  8883  diveqap1  8884  recdivap  8897  divdivap1  8902  divdivap2  8903  recdivap2  8904  conjmulap  8908  eqneg  8911  div2negap  8914  recreclt  9079  ofnegsub  9141  nn1m1nn  9160  nn1suc  9161  nnaddcl  9162  nnmulcl  9163  nnsub  9181  1m1e0  9211  neg1cn  9247  neg1ne0  9249  neg1ap0  9251  negneg1e1  9252  1pneg1e0  9253  1m0e1  9255  0p1e1  9256  1p0e1  9258  2m1e1  9260  3m1e2  9262  4m1e3  9263  5m1e4  9264  6m1e5  9265  7m1e6  9266  8m1e7  9267  9m1e8  9268  2p2e4  9269  1p2e3  9277  3p2e5  9284  3p3e6  9285  4p2e6  9286  4p3e7  9287  4p4e8  9288  5p2e7  9289  5p3e8  9290  5p4e9  9291  6p2e8  9292  6p3e9  9293  7p2e9  9294  1t1e1  9295  3t3e9  9300  neg1mulneg1e1  9355  1mhlfehlf  9361  8th4div3  9362  halfpm6th  9363  addltmul  9380  elnn0nn  9443  peano2z  9514  zlem1lt  9535  zltlem1  9536  nnaddm1cl  9540  elz2  9550  zextlt  9571  zeo  9584  peano5uzti  9587  numsuc  9623  numltc  9635  numsucc  9649  numaddc  9657  6p5lem  9679  5p5e10  9680  6p4e10  9681  7p3e10  9684  8p2e10  9689  10m1e9  9705  4t3lem  9706  7t4e28  9720  9t11e99  9739  decbin2  9750  halfthird  9752  5recm6rec  9753  uzp1  9789  peano2uzr  9818  uzaddcl  9819  qreccl  9875  iccf1o  10238  fz01en  10287  fztp  10312  fzsuc2  10313  fztpval  10317  fseq1m1p1  10329  elfzp1b  10331  fz0to4untppr  10358  fzoss2  10408  fzval3  10448  fzosplitsnm1  10453  fzo0to42pr  10464  fzosplitprm1  10479  fldiv4p1lem1div2  10564  flqdiv  10582  frecfzen2  10688  nn0ennn  10694  xnn0nnen  10698  seq3m1  10734  seqshft2g  10743  monoord2  10747  ser3mono  10748  seqf1oglem1  10780  seqf1oglem2  10781  expcl  10818  m1expcl2  10822  expclzaplem  10824  expm1t  10828  1exp  10829  mulexpzap  10840  expadd  10842  expaddzap  10844  expmul  10845  expubnd  10857  neg1sqe1  10895  irec  10900  i4  10903  binom21  10913  bernneq  10921  bernneq2  10922  facndiv  11000  faclbnd6  11005  bcnp1n  11020  bcm1k  11021  bcp1nk  11023  bcn2  11025  bcp1m1  11026  bcpasc  11027  4bc3eq4  11034  hashfz  11084  hashfzo  11085  seq3coll  11105  swrds1  11248  swrdlsw  11249  wrdind  11302  wrd2ind  11303  rei  11459  imi  11460  caucvgrelemrec  11539  recan  11669  iserex  11899  serf0  11912  fsumm1  11976  fsump1  11980  telfsumo  12026  fsumparts  12030  hashiun  12038  binomlem  12043  binom  12044  binom1p  12045  binom11  12046  binom1dif  12047  bcxmas  12049  isumsplit  12051  isum1p  12052  arisum  12058  arisum2  12059  trireciplem  12060  geosergap  12066  geolim  12071  geolim2  12072  georeclim  12073  geo2sum  12074  geo2sum2  12075  0.999...  12081  geoihalfsum  12082  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodf1  12102  prodfclim1  12104  prodrbdclem  12131  fproddccvg  12132  prodmodclem2a  12136  fprodntrivap  12144  prodssdc  12149  fprodssdc  12150  esum  12222  ege2le3  12231  efexp  12242  efzval  12243  eftlub  12250  effsumlt  12252  ef4p  12254  tanval3ap  12274  efi4p  12277  tan0  12291  efival  12292  tanaddap  12299  cos2t  12310  cos2tsin  12311  ef01bndlem  12316  cos1bnd  12319  cos2bnd  12320  demoivreALT  12334  eirraplem  12337  3dvds  12424  3dvdsdec  12425  3dvds2dec  12426  odd2np1lem  12432  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  m1exp1  12461  n2dvdsm1  12473  flodddiv4  12496  bitsfzo  12515  gcdmultiple  12590  sqgcd  12599  nn0seqcvgd  12612  prmind2  12691  hashdvds  12792  phiprmpw  12793  phiprm  12794  eulerthlemth  12803  sumhashdc  12919  fldivp1  12920  prmpwdvds  12927  pockthlem  12928  pockthi  12930  4sqlem11  12973  4sqlem19  12981  dec5nprm  12986  mulgnndir  13737  mulgneg2  13742  cnfld1  14585  zsssubrg  14598  mulgrhm2  14623  expcncf  15332  divcncfap  15337  hovercncf  15369  dvid  15418  dvidre  15420  dvexp  15434  dvexp2  15435  dveflem  15449  plyaddlem1  15470  plymullem1  15471  dvply1  15488  reeff1olem  15494  eulerid  15525  cos2pi  15527  sincosq3sgn  15551  sincosq4sgn  15552  cosq23lt0  15556  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  pigt3  15567  abssinper  15569  coskpi  15571  cosq34lt1  15573  logdivlti  15604  rpcxpp1  15629  rpcxpsqrt  15645  rprelogbdiv  15680  binom4  15702  wilthlem1  15703  0sgm  15708  1sgmprm  15717  1sgm2ppw  15718  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  zabsle1  15727  lgslem1  15728  lgslem2  15729  lgsfcl2  15734  lgsvalmod  15747  lgsneg  15752  lgsdilem  15755  lgsdir2lem1  15756  lgsdir2lem2  15757  lgsdir2lem3  15758  lgsdir2lem5  15760  lgsne0  15766  lgseisenlem1  15798  lgseisenlem2  15799  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  lgsquad2  15811  m1lgs  15813  2lgslem3c  15823  2lgsoddprmlem3c  15837  2lgsoddprmlem3d  15838  2sqlem10  15853  clwwlknonex2lem2  16288  ex-fl  16321  trilpolemeq1  16644