Axiom ax-1cn 7934

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

This axiom is referenced by:  0cn  7979  1ex  7982  mulrid  7984  mullid  7985  1cnd  8003  muladd11  8120  1p1times  8121  peano2cn  8122  peano2cnm  8253  0reALT  8284  pncan1  8364  npcan1  8365  kcnktkm1cn  8370  ine0  8381  mulm1  8387  mulsubfacd  8405  ixi  8570  inelr  8571  muleqadd  8655  recclap  8666  recap0  8672  recidap  8673  recidap2  8674  div1  8690  1div1e1  8691  diveqap1  8692  recdivap  8705  divdivap1  8710  divdivap2  8711  recdivap2  8712  conjmulap  8716  eqneg  8719  div2negap  8722  recreclt  8887  nn1m1nn  8967  nn1suc  8968  nnaddcl  8969  nnmulcl  8970  nnsub  8988  1m1e0  9018  neg1cn  9054  neg1ne0  9056  neg1ap0  9058  negneg1e1  9059  1pneg1e0  9060  1m0e1  9062  0p1e1  9063  1p0e1  9065  2m1e1  9067  3m1e2  9069  4m1e3  9070  5m1e4  9071  6m1e5  9072  7m1e6  9073  8m1e7  9074  9m1e8  9075  2p2e4  9076  1p2e3  9083  3p2e5  9090  3p3e6  9091  4p2e6  9092  4p3e7  9093  4p4e8  9094  5p2e7  9095  5p3e8  9096  5p4e9  9097  6p2e8  9098  6p3e9  9099  7p2e9  9100  1t1e1  9101  3t3e9  9106  neg1mulneg1e1  9161  1mhlfehlf  9167  8th4div3  9168  halfpm6th  9169  addltmul  9185  elnn0nn  9248  peano2z  9319  zlem1lt  9339  zltlem1  9340  nnaddm1cl  9344  elz2  9354  zextlt  9375  zeo  9388  peano5uzti  9391  numsuc  9427  numltc  9439  numsucc  9453  numaddc  9461  6p5lem  9483  5p5e10  9484  6p4e10  9485  7p3e10  9488  8p2e10  9493  10m1e9  9509  4t3lem  9510  7t4e28  9524  9t11e99  9543  decbin2  9554  halfthird  9556  5recm6rec  9557  uzp1  9591  peano2uzr  9615  uzaddcl  9616  qreccl  9672  iccf1o  10034  fz01en  10083  fztp  10108  fzsuc2  10109  fztpval  10113  fseq1m1p1  10125  elfzp1b  10127  fz0to4untppr  10154  fzoss2  10202  fzval3  10234  fzosplitsnm1  10239  fzo0to42pr  10250  fzosplitprm1  10264  fldiv4p1lem1div2  10336  flqdiv  10352  frecfzen2  10458  nn0ennn  10464  seq3m1  10499  monoord2  10508  ser3mono  10509  expcl  10569  m1expcl2  10573  expclzaplem  10575  expm1t  10579  1exp  10580  mulexpzap  10591  expadd  10593  expaddzap  10595  expmul  10596  expubnd  10608  neg1sqe1  10646  irec  10651  i4  10654  binom21  10664  bernneq  10672  bernneq2  10673  facndiv  10751  faclbnd6  10756  bcnp1n  10771  bcm1k  10772  bcp1nk  10774  bcn2  10776  bcp1m1  10777  bcpasc  10778  4bc3eq4  10785  hashfz  10833  hashfzo  10834  seq3coll  10854  rei  10940  imi  10941  caucvgrelemrec  11020  recan  11150  iserex  11379  serf0  11392  fsumm1  11456  fsump1  11460  telfsumo  11506  fsumparts  11510  hashiun  11518  binomlem  11523  binom  11524  binom1p  11525  binom11  11526  binom1dif  11527  bcxmas  11529  isumsplit  11531  isum1p  11532  arisum  11538  arisum2  11539  trireciplem  11540  geosergap  11546  geolim  11551  geolim2  11552  georeclim  11553  geo2sum  11554  geo2sum2  11555  0.999...  11561  geoihalfsum  11562  mertenslemi1  11575  mertenslem2  11576  mertensabs  11577  prodf1  11582  prodfclim1  11584  prodrbdclem  11611  fproddccvg  11612  prodmodclem2a  11616  fprodntrivap  11624  prodssdc  11629  fprodssdc  11630  esum  11702  ege2le3  11711  efexp  11722  efzval  11723  eftlub  11730  effsumlt  11732  ef4p  11734  tanval3ap  11754  efi4p  11757  tan0  11771  efival  11772  tanaddap  11779  cos2t  11790  cos2tsin  11791  ef01bndlem  11796  cos1bnd  11799  cos2bnd  11800  demoivreALT  11813  eirraplem  11816  3dvdsdec  11902  3dvds2dec  11903  odd2np1lem  11909  odd2np1  11910  opoe  11932  omoe  11933  opeo  11934  omeo  11935  m1exp1  11938  n2dvdsm1  11950  flodddiv4  11971  gcdmultiple  12053  sqgcd  12062  nn0seqcvgd  12073  prmind2  12152  hashdvds  12253  phiprmpw  12254  phiprm  12255  eulerthlemth  12264  sumhashdc  12379  fldivp1  12380  prmpwdvds  12387  pockthlem  12388  pockthi  12390  4sqlem11  12433  4sqlem19  12441  mulgnndir  13091  mulgneg2  13096  cnfld1  13875  zsssubrg  13888  mulgrhm2  13908  expcncf  14552  dvid  14622  dvexp  14635  dvexp2  14636  dveflem  14647  reeff1olem  14652  eulerid  14683  cos2pi  14685  sincosq3sgn  14709  sincosq4sgn  14710  cosq23lt0  14714  tangtx  14719  sincos4thpi  14721  sincos6thpi  14723  pigt3  14725  abssinper  14727  coskpi  14729  cosq34lt1  14731  logdivlti  14762  rpcxpp1  14787  rpcxpsqrt  14802  rprelogbdiv  14835  binom4  14857  wilthlem1  14858  zabsle1  14861  lgslem1  14862  lgslem2  14863  lgsfcl2  14868  lgsvalmod  14881  lgsneg  14886  lgsdilem  14889  lgsdir2lem1  14890  lgsdir2lem2  14891  lgsdir2lem3  14892  lgsdir2lem5  14894  lgsne0  14900  lgseisenlem1  14911  lgseisenlem2  14912  m1lgs  14913  2lgsoddprmlem3c  14918  2lgsoddprmlem3d  14919  2sqlem10  14933  ex-fl  14938  trilpolemeq1  15250