Axiom ax-1cn 7846

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

This axiom is referenced by:  0cn  7891  1ex  7894  mulid1  7896  mulid2  7897  1cnd  7915  muladd11  8031  1p1times  8032  peano2cn  8033  peano2cnm  8164  0reALT  8195  pncan1  8275  npcan1  8276  kcnktkm1cn  8281  ine0  8292  mulm1  8298  mulsubfacd  8316  ixi  8481  inelr  8482  muleqadd  8565  recclap  8575  recap0  8581  recidap  8582  recidap2  8583  div1  8599  1div1e1  8600  diveqap1  8601  recdivap  8614  divdivap1  8619  divdivap2  8620  recdivap2  8621  conjmulap  8625  eqneg  8628  div2negap  8631  recreclt  8795  nn1m1nn  8875  nn1suc  8876  nnaddcl  8877  nnmulcl  8878  nnsub  8896  1m1e0  8926  neg1cn  8962  neg1ne0  8964  neg1ap0  8966  negneg1e1  8967  1pneg1e0  8968  1m0e1  8970  0p1e1  8971  1p0e1  8973  2m1e1  8975  3m1e2  8977  4m1e3  8978  5m1e4  8979  6m1e5  8980  7m1e6  8981  8m1e7  8982  9m1e8  8983  2p2e4  8984  1p2e3  8991  3p2e5  8998  3p3e6  8999  4p2e6  9000  4p3e7  9001  4p4e8  9002  5p2e7  9003  5p3e8  9004  5p4e9  9005  6p2e8  9006  6p3e9  9007  7p2e9  9008  1t1e1  9009  3t3e9  9014  neg1mulneg1e1  9069  1mhlfehlf  9075  8th4div3  9076  halfpm6th  9077  addltmul  9093  elnn0nn  9156  peano2z  9227  zlem1lt  9247  zltlem1  9248  nnaddm1cl  9252  elz2  9262  zextlt  9283  zeo  9296  peano5uzti  9299  numsuc  9335  numltc  9347  numsucc  9361  numaddc  9369  6p5lem  9391  5p5e10  9392  6p4e10  9393  7p3e10  9396  8p2e10  9401  10m1e9  9417  4t3lem  9418  7t4e28  9432  9t11e99  9451  decbin2  9462  halfthird  9464  5recm6rec  9465  uzp1  9499  peano2uzr  9523  uzaddcl  9524  qreccl  9580  iccf1o  9940  fz01en  9988  fztp  10013  fzsuc2  10014  fztpval  10018  fseq1m1p1  10030  elfzp1b  10032  fz0to4untppr  10059  fzoss2  10107  fzval3  10139  fzosplitsnm1  10144  fzo0to42pr  10155  fzosplitprm1  10169  fldiv4p1lem1div2  10240  flqdiv  10256  frecfzen2  10362  nn0ennn  10368  seq3m1  10403  monoord2  10412  ser3mono  10413  expcl  10473  m1expcl2  10477  expclzaplem  10479  expm1t  10483  1exp  10484  mulexpzap  10495  expadd  10497  expaddzap  10499  expmul  10500  expubnd  10512  neg1sqe1  10549  irec  10554  i4  10557  binom21  10567  bernneq  10575  bernneq2  10576  facndiv  10652  faclbnd6  10657  bcnp1n  10672  bcm1k  10673  bcp1nk  10675  bcn2  10677  bcp1m1  10678  bcpasc  10679  4bc3eq4  10686  hashfz  10734  hashfzo  10735  seq3coll  10755  rei  10841  imi  10842  caucvgrelemrec  10921  recan  11051  iserex  11280  serf0  11293  fsumm1  11357  fsump1  11361  telfsumo  11407  fsumparts  11411  hashiun  11419  binomlem  11424  binom  11425  binom1p  11426  binom11  11427  binom1dif  11428  bcxmas  11430  isumsplit  11432  isum1p  11433  arisum  11439  arisum2  11440  trireciplem  11441  geosergap  11447  geolim  11452  geolim2  11453  georeclim  11454  geo2sum  11455  geo2sum2  11456  0.999...  11462  geoihalfsum  11463  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodf1  11483  prodfclim1  11485  prodrbdclem  11512  fproddccvg  11513  prodmodclem2a  11517  fprodntrivap  11525  prodssdc  11530  fprodssdc  11531  esum  11603  ege2le3  11612  efexp  11623  efzval  11624  eftlub  11631  effsumlt  11633  ef4p  11635  tanval3ap  11655  efi4p  11658  tan0  11672  efival  11673  tanaddap  11680  cos2t  11691  cos2tsin  11692  ef01bndlem  11697  cos1bnd  11700  cos2bnd  11701  demoivreALT  11714  eirraplem  11717  3dvdsdec  11802  3dvds2dec  11803  odd2np1lem  11809  odd2np1  11810  opoe  11832  omoe  11833  opeo  11834  omeo  11835  m1exp1  11838  n2dvdsm1  11850  flodddiv4  11871  gcdmultiple  11953  sqgcd  11962  nn0seqcvgd  11973  prmind2  12052  hashdvds  12153  phiprmpw  12154  phiprm  12155  eulerthlemth  12164  sumhashdc  12277  fldivp1  12278  prmpwdvds  12285  pockthlem  12286  pockthi  12288  expcncf  13232  dvid  13302  dvexp  13315  dvexp2  13316  dveflem  13327  reeff1olem  13332  eulerid  13363  cos2pi  13365  sincosq3sgn  13389  sincosq4sgn  13390  cosq23lt0  13394  tangtx  13399  sincos4thpi  13401  sincos6thpi  13403  pigt3  13405  abssinper  13407  coskpi  13409  cosq34lt1  13411  logdivlti  13442  rpcxpp1  13467  rpcxpsqrt  13482  rprelogbdiv  13515  binom4  13537  zabsle1  13540  lgslem1  13541  lgslem2  13542  lgsfcl2  13547  lgsvalmod  13560  lgsneg  13565  lgsdilem  13568  lgsdir2lem1  13569  lgsdir2lem2  13570  lgsdir2lem3  13571  lgsdir2lem5  13573  lgsne0  13579  2sqlem10  13601  ex-fl  13606  trilpolemeq1  13919