Axiom ax-1cn 7906

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

This axiom is referenced by:  0cn  7951  1ex  7954  mulrid  7956  mullid  7957  1cnd  7975  muladd11  8092  1p1times  8093  peano2cn  8094  peano2cnm  8225  0reALT  8256  pncan1  8336  npcan1  8337  kcnktkm1cn  8342  ine0  8353  mulm1  8359  mulsubfacd  8377  ixi  8542  inelr  8543  muleqadd  8627  recclap  8638  recap0  8644  recidap  8645  recidap2  8646  div1  8662  1div1e1  8663  diveqap1  8664  recdivap  8677  divdivap1  8682  divdivap2  8683  recdivap2  8684  conjmulap  8688  eqneg  8691  div2negap  8694  recreclt  8859  nn1m1nn  8939  nn1suc  8940  nnaddcl  8941  nnmulcl  8942  nnsub  8960  1m1e0  8990  neg1cn  9026  neg1ne0  9028  neg1ap0  9030  negneg1e1  9031  1pneg1e0  9032  1m0e1  9034  0p1e1  9035  1p0e1  9037  2m1e1  9039  3m1e2  9041  4m1e3  9042  5m1e4  9043  6m1e5  9044  7m1e6  9045  8m1e7  9046  9m1e8  9047  2p2e4  9048  1p2e3  9055  3p2e5  9062  3p3e6  9063  4p2e6  9064  4p3e7  9065  4p4e8  9066  5p2e7  9067  5p3e8  9068  5p4e9  9069  6p2e8  9070  6p3e9  9071  7p2e9  9072  1t1e1  9073  3t3e9  9078  neg1mulneg1e1  9133  1mhlfehlf  9139  8th4div3  9140  halfpm6th  9141  addltmul  9157  elnn0nn  9220  peano2z  9291  zlem1lt  9311  zltlem1  9312  nnaddm1cl  9316  elz2  9326  zextlt  9347  zeo  9360  peano5uzti  9363  numsuc  9399  numltc  9411  numsucc  9425  numaddc  9433  6p5lem  9455  5p5e10  9456  6p4e10  9457  7p3e10  9460  8p2e10  9465  10m1e9  9481  4t3lem  9482  7t4e28  9496  9t11e99  9515  decbin2  9526  halfthird  9528  5recm6rec  9529  uzp1  9563  peano2uzr  9587  uzaddcl  9588  qreccl  9644  iccf1o  10006  fz01en  10055  fztp  10080  fzsuc2  10081  fztpval  10085  fseq1m1p1  10097  elfzp1b  10099  fz0to4untppr  10126  fzoss2  10174  fzval3  10206  fzosplitsnm1  10211  fzo0to42pr  10222  fzosplitprm1  10236  fldiv4p1lem1div2  10307  flqdiv  10323  frecfzen2  10429  nn0ennn  10435  seq3m1  10470  monoord2  10479  ser3mono  10480  expcl  10540  m1expcl2  10544  expclzaplem  10546  expm1t  10550  1exp  10551  mulexpzap  10562  expadd  10564  expaddzap  10566  expmul  10567  expubnd  10579  neg1sqe1  10617  irec  10622  i4  10625  binom21  10635  bernneq  10643  bernneq2  10644  facndiv  10721  faclbnd6  10726  bcnp1n  10741  bcm1k  10742  bcp1nk  10744  bcn2  10746  bcp1m1  10747  bcpasc  10748  4bc3eq4  10755  hashfz  10803  hashfzo  10804  seq3coll  10824  rei  10910  imi  10911  caucvgrelemrec  10990  recan  11120  iserex  11349  serf0  11362  fsumm1  11426  fsump1  11430  telfsumo  11476  fsumparts  11480  hashiun  11488  binomlem  11493  binom  11494  binom1p  11495  binom11  11496  binom1dif  11497  bcxmas  11499  isumsplit  11501  isum1p  11502  arisum  11508  arisum2  11509  trireciplem  11510  geosergap  11516  geolim  11521  geolim2  11522  georeclim  11523  geo2sum  11524  geo2sum2  11525  0.999...  11531  geoihalfsum  11532  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodf1  11552  prodfclim1  11554  prodrbdclem  11581  fproddccvg  11582  prodmodclem2a  11586  fprodntrivap  11594  prodssdc  11599  fprodssdc  11600  esum  11672  ege2le3  11681  efexp  11692  efzval  11693  eftlub  11700  effsumlt  11702  ef4p  11704  tanval3ap  11724  efi4p  11727  tan0  11741  efival  11742  tanaddap  11749  cos2t  11760  cos2tsin  11761  ef01bndlem  11766  cos1bnd  11769  cos2bnd  11770  demoivreALT  11783  eirraplem  11786  3dvdsdec  11872  3dvds2dec  11873  odd2np1lem  11879  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  m1exp1  11908  n2dvdsm1  11920  flodddiv4  11941  gcdmultiple  12023  sqgcd  12032  nn0seqcvgd  12043  prmind2  12122  hashdvds  12223  phiprmpw  12224  phiprm  12225  eulerthlemth  12234  sumhashdc  12347  fldivp1  12348  prmpwdvds  12355  pockthlem  12356  pockthi  12358  mulgnndir  13017  mulgneg2  13022  cnfld1  13505  zsssubrg  13518  expcncf  14131  dvid  14201  dvexp  14214  dvexp2  14215  dveflem  14226  reeff1olem  14231  eulerid  14262  cos2pi  14264  sincosq3sgn  14288  sincosq4sgn  14289  cosq23lt0  14293  tangtx  14298  sincos4thpi  14300  sincos6thpi  14302  pigt3  14304  abssinper  14306  coskpi  14308  cosq34lt1  14310  logdivlti  14341  rpcxpp1  14366  rpcxpsqrt  14381  rprelogbdiv  14414  binom4  14436  zabsle1  14439  lgslem1  14440  lgslem2  14441  lgsfcl2  14446  lgsvalmod  14459  lgsneg  14464  lgsdilem  14467  lgsdir2lem1  14468  lgsdir2lem2  14469  lgsdir2lem3  14470  lgsdir2lem5  14472  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2lgsoddprmlem3c  14496  2lgsoddprmlem3d  14497  2sqlem10  14511  ex-fl  14516  trilpolemeq1  14827