Axiom ax-1cn 7713

Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7669. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	|- 1 e. CC

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 7621	. 2 class 1
2		cc 7618	. 2 class CC
3	1, 2	wcel 1480	1 wff 1 e. CC

This axiom is referenced by:  0cn  7758  1ex  7761  mulid1  7763  mulid2  7764  1cnd  7782  muladd11  7895  1p1times  7896  peano2cn  7897  peano2cnm  8028  0reALT  8059  pncan1  8139  npcan1  8140  kcnktkm1cn  8145  ine0  8156  mulm1  8162  mulsubfacd  8180  ixi  8345  inelr  8346  muleqadd  8429  recclap  8439  recap0  8445  recidap  8446  recidap2  8447  div1  8463  1div1e1  8464  diveqap1  8465  recdivap  8478  divdivap1  8483  divdivap2  8484  recdivap2  8485  conjmulap  8489  eqneg  8492  div2negap  8495  recreclt  8658  nn1m1nn  8738  nn1suc  8739  nnaddcl  8740  nnmulcl  8741  nnsub  8759  1m1e0  8789  neg1cn  8825  neg1ne0  8827  neg1ap0  8829  negneg1e1  8830  1pneg1e0  8831  1m0e1  8833  0p1e1  8834  1p0e1  8836  2m1e1  8838  3m1e2  8840  4m1e3  8841  5m1e4  8842  6m1e5  8843  7m1e6  8844  8m1e7  8845  9m1e8  8846  2p2e4  8847  1p2e3  8854  3p2e5  8861  3p3e6  8862  4p2e6  8863  4p3e7  8864  4p4e8  8865  5p2e7  8866  5p3e8  8867  5p4e9  8868  6p2e8  8869  6p3e9  8870  7p2e9  8871  1t1e1  8872  3t3e9  8877  neg1mulneg1e1  8932  1mhlfehlf  8938  8th4div3  8939  halfpm6th  8940  addltmul  8956  elnn0nn  9019  peano2z  9090  zlem1lt  9110  zltlem1  9111  nnaddm1cl  9115  elz2  9122  zextlt  9143  zeo  9156  peano5uzti  9159  numsuc  9195  numltc  9207  numsucc  9221  numaddc  9229  6p5lem  9251  5p5e10  9252  6p4e10  9253  7p3e10  9256  8p2e10  9261  10m1e9  9277  4t3lem  9278  7t4e28  9292  9t11e99  9311  decbin2  9322  halfthird  9324  5recm6rec  9325  uzp1  9359  peano2uzr  9380  uzaddcl  9381  qreccl  9434  iccf1o  9787  fz01en  9833  fztp  9858  fzsuc2  9859  fztpval  9863  fseq1m1p1  9875  elfzp1b  9877  fzoss2  9949  fzval3  9981  fzosplitsnm1  9986  fzo0to42pr  9997  fzosplitprm1  10011  fldiv4p1lem1div2  10078  flqdiv  10094  frecfzen2  10200  nn0ennn  10206  seq3m1  10241  monoord2  10250  ser3mono  10251  expcl  10311  m1expcl2  10315  expclzaplem  10317  expm1t  10321  1exp  10322  mulexpzap  10333  expadd  10335  expaddzap  10337  expmul  10338  expubnd  10350  neg1sqe1  10387  irec  10392  i4  10395  binom21  10404  bernneq  10412  bernneq2  10413  facndiv  10485  faclbnd6  10490  bcnp1n  10505  bcm1k  10506  bcp1nk  10508  bcn2  10510  bcp1m1  10511  bcpasc  10512  4bc3eq4  10519  hashfz  10567  hashfzo  10568  seq3coll  10585  rei  10671  imi  10672  caucvgrelemrec  10751  recan  10881  iserex  11108  serf0  11121  fsumm1  11185  fsump1  11189  telfsumo  11235  fsumparts  11239  hashiun  11247  binomlem  11252  binom  11253  binom1p  11254  binom11  11255  binom1dif  11256  bcxmas  11258  isumsplit  11260  isum1p  11261  arisum  11267  arisum2  11268  trireciplem  11269  geosergap  11275  geolim  11280  geolim2  11281  georeclim  11282  geo2sum  11283  geo2sum2  11284  0.999...  11290  geoihalfsum  11291  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodf1  11311  prodfclim1  11313  prodrbdclem  11340  fproddccvg  11341  prodmodclem2a  11345  esum  11368  ege2le3  11377  efexp  11388  efzval  11389  eftlub  11396  effsumlt  11398  ef4p  11400  tanval3ap  11421  efi4p  11424  tan0  11438  efival  11439  tanaddap  11446  cos2t  11457  cos2tsin  11458  ef01bndlem  11463  cos1bnd  11466  cos2bnd  11467  demoivreALT  11480  eirraplem  11483  3dvdsdec  11562  3dvds2dec  11563  odd2np1lem  11569  odd2np1  11570  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1exp1  11598  n2dvdsm1  11610  flodddiv4  11631  gcdmultiple  11708  sqgcd  11717  nn0seqcvgd  11722  prmind2  11801  hashdvds  11897  phiprmpw  11898  phiprm  11899  expcncf  12761  dvid  12831  dvexp  12844  dvexp2  12845  dveflem  12855  eulerid  12883  cos2pi  12885  sincosq3sgn  12909  sincosq4sgn  12910  cosq23lt0  12914  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  pigt3  12925  abssinper  12927  coskpi  12929  cosq34lt1  12931  ex-fl  12937  trilpolemeq1  13233