Axiom ax-1cn 7867

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

This axiom is referenced by:  0cn  7912  1ex  7915  mulid1  7917  mulid2  7918  1cnd  7936  muladd11  8052  1p1times  8053  peano2cn  8054  peano2cnm  8185  0reALT  8216  pncan1  8296  npcan1  8297  kcnktkm1cn  8302  ine0  8313  mulm1  8319  mulsubfacd  8337  ixi  8502  inelr  8503  muleqadd  8586  recclap  8596  recap0  8602  recidap  8603  recidap2  8604  div1  8620  1div1e1  8621  diveqap1  8622  recdivap  8635  divdivap1  8640  divdivap2  8641  recdivap2  8642  conjmulap  8646  eqneg  8649  div2negap  8652  recreclt  8816  nn1m1nn  8896  nn1suc  8897  nnaddcl  8898  nnmulcl  8899  nnsub  8917  1m1e0  8947  neg1cn  8983  neg1ne0  8985  neg1ap0  8987  negneg1e1  8988  1pneg1e0  8989  1m0e1  8991  0p1e1  8992  1p0e1  8994  2m1e1  8996  3m1e2  8998  4m1e3  8999  5m1e4  9000  6m1e5  9001  7m1e6  9002  8m1e7  9003  9m1e8  9004  2p2e4  9005  1p2e3  9012  3p2e5  9019  3p3e6  9020  4p2e6  9021  4p3e7  9022  4p4e8  9023  5p2e7  9024  5p3e8  9025  5p4e9  9026  6p2e8  9027  6p3e9  9028  7p2e9  9029  1t1e1  9030  3t3e9  9035  neg1mulneg1e1  9090  1mhlfehlf  9096  8th4div3  9097  halfpm6th  9098  addltmul  9114  elnn0nn  9177  peano2z  9248  zlem1lt  9268  zltlem1  9269  nnaddm1cl  9273  elz2  9283  zextlt  9304  zeo  9317  peano5uzti  9320  numsuc  9356  numltc  9368  numsucc  9382  numaddc  9390  6p5lem  9412  5p5e10  9413  6p4e10  9414  7p3e10  9417  8p2e10  9422  10m1e9  9438  4t3lem  9439  7t4e28  9453  9t11e99  9472  decbin2  9483  halfthird  9485  5recm6rec  9486  uzp1  9520  peano2uzr  9544  uzaddcl  9545  qreccl  9601  iccf1o  9961  fz01en  10009  fztp  10034  fzsuc2  10035  fztpval  10039  fseq1m1p1  10051  elfzp1b  10053  fz0to4untppr  10080  fzoss2  10128  fzval3  10160  fzosplitsnm1  10165  fzo0to42pr  10176  fzosplitprm1  10190  fldiv4p1lem1div2  10261  flqdiv  10277  frecfzen2  10383  nn0ennn  10389  seq3m1  10424  monoord2  10433  ser3mono  10434  expcl  10494  m1expcl2  10498  expclzaplem  10500  expm1t  10504  1exp  10505  mulexpzap  10516  expadd  10518  expaddzap  10520  expmul  10521  expubnd  10533  neg1sqe1  10570  irec  10575  i4  10578  binom21  10588  bernneq  10596  bernneq2  10597  facndiv  10673  faclbnd6  10678  bcnp1n  10693  bcm1k  10694  bcp1nk  10696  bcn2  10698  bcp1m1  10699  bcpasc  10700  4bc3eq4  10707  hashfz  10756  hashfzo  10757  seq3coll  10777  rei  10863  imi  10864  caucvgrelemrec  10943  recan  11073  iserex  11302  serf0  11315  fsumm1  11379  fsump1  11383  telfsumo  11429  fsumparts  11433  hashiun  11441  binomlem  11446  binom  11447  binom1p  11448  binom11  11449  binom1dif  11450  bcxmas  11452  isumsplit  11454  isum1p  11455  arisum  11461  arisum2  11462  trireciplem  11463  geosergap  11469  geolim  11474  geolim2  11475  georeclim  11476  geo2sum  11477  geo2sum2  11478  0.999...  11484  geoihalfsum  11485  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodf1  11505  prodfclim1  11507  prodrbdclem  11534  fproddccvg  11535  prodmodclem2a  11539  fprodntrivap  11547  prodssdc  11552  fprodssdc  11553  esum  11625  ege2le3  11634  efexp  11645  efzval  11646  eftlub  11653  effsumlt  11655  ef4p  11657  tanval3ap  11677  efi4p  11680  tan0  11694  efival  11695  tanaddap  11702  cos2t  11713  cos2tsin  11714  ef01bndlem  11719  cos1bnd  11722  cos2bnd  11723  demoivreALT  11736  eirraplem  11739  3dvdsdec  11824  3dvds2dec  11825  odd2np1lem  11831  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1exp1  11860  n2dvdsm1  11872  flodddiv4  11893  gcdmultiple  11975  sqgcd  11984  nn0seqcvgd  11995  prmind2  12074  hashdvds  12175  phiprmpw  12176  phiprm  12177  eulerthlemth  12186  sumhashdc  12299  fldivp1  12300  prmpwdvds  12307  pockthlem  12308  pockthi  12310  expcncf  13386  dvid  13456  dvexp  13469  dvexp2  13470  dveflem  13481  reeff1olem  13486  eulerid  13517  cos2pi  13519  sincosq3sgn  13543  sincosq4sgn  13544  cosq23lt0  13548  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  pigt3  13559  abssinper  13561  coskpi  13563  cosq34lt1  13565  logdivlti  13596  rpcxpp1  13621  rpcxpsqrt  13636  rprelogbdiv  13669  binom4  13691  zabsle1  13694  lgslem1  13695  lgslem2  13696  lgsfcl2  13701  lgsvalmod  13714  lgsneg  13719  lgsdilem  13722  lgsdir2lem1  13723  lgsdir2lem2  13724  lgsdir2lem3  13725  lgsdir2lem5  13727  lgsne0  13733  2sqlem10  13755  ex-fl  13760  trilpolemeq1  14072