Axiom ax-1cn 7965

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

This axiom is referenced by:  0cn  8011  1ex  8014  mulrid  8016  mullid  8017  1cnd  8035  muladd11  8152  1p1times  8153  peano2cn  8154  peano2cnm  8285  0reALT  8316  pncan1  8396  npcan1  8397  kcnktkm1cn  8402  ine0  8413  mulm1  8419  mulsubfacd  8437  ixi  8602  inelr  8603  muleqadd  8687  recclap  8698  recap0  8704  recidap  8705  recidap2  8706  div1  8722  1div1e1  8723  diveqap1  8724  recdivap  8737  divdivap1  8742  divdivap2  8743  recdivap2  8744  conjmulap  8748  eqneg  8751  div2negap  8754  recreclt  8919  ofnegsub  8981  nn1m1nn  9000  nn1suc  9001  nnaddcl  9002  nnmulcl  9003  nnsub  9021  1m1e0  9051  neg1cn  9087  neg1ne0  9089  neg1ap0  9091  negneg1e1  9092  1pneg1e0  9093  1m0e1  9095  0p1e1  9096  1p0e1  9098  2m1e1  9100  3m1e2  9102  4m1e3  9103  5m1e4  9104  6m1e5  9105  7m1e6  9106  8m1e7  9107  9m1e8  9108  2p2e4  9109  1p2e3  9116  3p2e5  9123  3p3e6  9124  4p2e6  9125  4p3e7  9126  4p4e8  9127  5p2e7  9128  5p3e8  9129  5p4e9  9130  6p2e8  9131  6p3e9  9132  7p2e9  9133  1t1e1  9134  3t3e9  9139  neg1mulneg1e1  9194  1mhlfehlf  9200  8th4div3  9201  halfpm6th  9202  addltmul  9219  elnn0nn  9282  peano2z  9353  zlem1lt  9373  zltlem1  9374  nnaddm1cl  9378  elz2  9388  zextlt  9409  zeo  9422  peano5uzti  9425  numsuc  9461  numltc  9473  numsucc  9487  numaddc  9495  6p5lem  9517  5p5e10  9518  6p4e10  9519  7p3e10  9522  8p2e10  9527  10m1e9  9543  4t3lem  9544  7t4e28  9558  9t11e99  9577  decbin2  9588  halfthird  9590  5recm6rec  9591  uzp1  9626  peano2uzr  9650  uzaddcl  9651  qreccl  9707  iccf1o  10070  fz01en  10119  fztp  10144  fzsuc2  10145  fztpval  10149  fseq1m1p1  10161  elfzp1b  10163  fz0to4untppr  10190  fzoss2  10239  fzval3  10271  fzosplitsnm1  10276  fzo0to42pr  10287  fzosplitprm1  10301  fldiv4p1lem1div2  10374  flqdiv  10392  frecfzen2  10498  nn0ennn  10504  xnn0nnen  10508  seq3m1  10544  seqshft2g  10553  monoord2  10557  ser3mono  10558  seqf1oglem1  10590  seqf1oglem2  10591  expcl  10628  m1expcl2  10632  expclzaplem  10634  expm1t  10638  1exp  10639  mulexpzap  10650  expadd  10652  expaddzap  10654  expmul  10655  expubnd  10667  neg1sqe1  10705  irec  10710  i4  10713  binom21  10723  bernneq  10731  bernneq2  10732  facndiv  10810  faclbnd6  10815  bcnp1n  10830  bcm1k  10831  bcp1nk  10833  bcn2  10835  bcp1m1  10836  bcpasc  10837  4bc3eq4  10844  hashfz  10892  hashfzo  10893  seq3coll  10913  rei  11043  imi  11044  caucvgrelemrec  11123  recan  11253  iserex  11482  serf0  11495  fsumm1  11559  fsump1  11563  telfsumo  11609  fsumparts  11613  hashiun  11621  binomlem  11626  binom  11627  binom1p  11628  binom11  11629  binom1dif  11630  bcxmas  11632  isumsplit  11634  isum1p  11635  arisum  11641  arisum2  11642  trireciplem  11643  geosergap  11649  geolim  11654  geolim2  11655  georeclim  11656  geo2sum  11657  geo2sum2  11658  0.999...  11664  geoihalfsum  11665  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodf1  11685  prodfclim1  11687  prodrbdclem  11714  fproddccvg  11715  prodmodclem2a  11719  fprodntrivap  11727  prodssdc  11732  fprodssdc  11733  esum  11805  ege2le3  11814  efexp  11825  efzval  11826  eftlub  11833  effsumlt  11835  ef4p  11837  tanval3ap  11857  efi4p  11860  tan0  11874  efival  11875  tanaddap  11882  cos2t  11893  cos2tsin  11894  ef01bndlem  11899  cos1bnd  11902  cos2bnd  11903  demoivreALT  11917  eirraplem  11920  3dvdsdec  12006  3dvds2dec  12007  odd2np1lem  12013  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  m1exp1  12042  n2dvdsm1  12054  flodddiv4  12075  gcdmultiple  12157  sqgcd  12166  nn0seqcvgd  12179  prmind2  12258  hashdvds  12359  phiprmpw  12360  phiprm  12361  eulerthlemth  12370  sumhashdc  12485  fldivp1  12486  prmpwdvds  12493  pockthlem  12494  pockthi  12496  4sqlem11  12539  4sqlem19  12547  mulgnndir  13221  mulgneg2  13226  cnfld1  14060  zsssubrg  14073  mulgrhm2  14098  expcncf  14763  divcncfap  14768  hovercncf  14800  dvid  14847  dvexp  14860  dvexp2  14861  dveflem  14872  plyaddlem1  14893  plymullem1  14894  reeff1olem  14906  eulerid  14937  cos2pi  14939  sincosq3sgn  14963  sincosq4sgn  14964  cosq23lt0  14968  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  pigt3  14979  abssinper  14981  coskpi  14983  cosq34lt1  14985  logdivlti  15016  rpcxpp1  15041  rpcxpsqrt  15056  rprelogbdiv  15089  binom4  15111  wilthlem1  15112  zabsle1  15115  lgslem1  15116  lgslem2  15117  lgsfcl2  15122  lgsvalmod  15135  lgsneg  15140  lgsdilem  15143  lgsdir2lem1  15144  lgsdir2lem2  15145  lgsdir2lem3  15146  lgsdir2lem5  15148  lgsne0  15154  lgseisenlem1  15186  lgseisenlem2  15187  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  2sqlem10  15212  ex-fl  15217  trilpolemeq1  15530