Axiom ax-1cn 7706

Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7662. (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 7614	. 2 class 1
2		cc 7611	. 2 class CC
3	1, 2	wcel 1480	1 wff 1 e. CC

This axiom is referenced by:  0cn  7751  1ex  7754  mulid1  7756  mulid2  7757  1cnd  7775  muladd11  7888  1p1times  7889  peano2cn  7890  peano2cnm  8021  0reALT  8052  pncan1  8132  npcan1  8133  kcnktkm1cn  8138  ine0  8149  mulm1  8155  mulsubfacd  8173  ixi  8338  inelr  8339  muleqadd  8422  recclap  8432  recap0  8438  recidap  8439  recidap2  8440  div1  8456  1div1e1  8457  diveqap1  8458  recdivap  8471  divdivap1  8476  divdivap2  8477  recdivap2  8478  conjmulap  8482  eqneg  8485  div2negap  8488  recreclt  8651  nn1m1nn  8731  nn1suc  8732  nnaddcl  8733  nnmulcl  8734  nnsub  8752  1m1e0  8782  neg1cn  8818  neg1ne0  8820  neg1ap0  8822  negneg1e1  8823  1pneg1e0  8824  1m0e1  8826  0p1e1  8827  1p0e1  8829  2m1e1  8831  3m1e2  8833  4m1e3  8834  5m1e4  8835  6m1e5  8836  7m1e6  8837  8m1e7  8838  9m1e8  8839  2p2e4  8840  1p2e3  8847  3p2e5  8854  3p3e6  8855  4p2e6  8856  4p3e7  8857  4p4e8  8858  5p2e7  8859  5p3e8  8860  5p4e9  8861  6p2e8  8862  6p3e9  8863  7p2e9  8864  1t1e1  8865  3t3e9  8870  neg1mulneg1e1  8925  1mhlfehlf  8931  8th4div3  8932  halfpm6th  8933  addltmul  8949  elnn0nn  9012  peano2z  9083  zlem1lt  9103  zltlem1  9104  nnaddm1cl  9108  elz2  9115  zextlt  9136  zeo  9149  peano5uzti  9152  numsuc  9188  numltc  9200  numsucc  9214  numaddc  9222  6p5lem  9244  5p5e10  9245  6p4e10  9246  7p3e10  9249  8p2e10  9254  10m1e9  9270  4t3lem  9271  7t4e28  9285  9t11e99  9304  decbin2  9315  halfthird  9317  5recm6rec  9318  uzp1  9352  peano2uzr  9373  uzaddcl  9374  qreccl  9427  iccf1o  9780  fz01en  9826  fztp  9851  fzsuc2  9852  fztpval  9856  fseq1m1p1  9868  elfzp1b  9870  fzoss2  9942  fzval3  9974  fzosplitsnm1  9979  fzo0to42pr  9990  fzosplitprm1  10004  fldiv4p1lem1div2  10071  flqdiv  10087  frecfzen2  10193  nn0ennn  10199  seq3m1  10234  monoord2  10243  ser3mono  10244  expcl  10304  m1expcl2  10308  expclzaplem  10310  expm1t  10314  1exp  10315  mulexpzap  10326  expadd  10328  expaddzap  10330  expmul  10331  expubnd  10343  neg1sqe1  10380  irec  10385  i4  10388  binom21  10397  bernneq  10405  bernneq2  10406  facndiv  10478  faclbnd6  10483  bcnp1n  10498  bcm1k  10499  bcp1nk  10501  bcn2  10503  bcp1m1  10504  bcpasc  10505  4bc3eq4  10512  hashfz  10560  hashfzo  10561  seq3coll  10578  rei  10664  imi  10665  caucvgrelemrec  10744  recan  10874  iserex  11101  serf0  11114  fsumm1  11178  fsump1  11182  telfsumo  11228  fsumparts  11232  hashiun  11240  binomlem  11245  binom  11246  binom1p  11247  binom11  11248  binom1dif  11249  bcxmas  11251  isumsplit  11253  isum1p  11254  arisum  11260  arisum2  11261  trireciplem  11262  geosergap  11268  geolim  11273  geolim2  11274  georeclim  11275  geo2sum  11276  geo2sum2  11277  0.999...  11283  geoihalfsum  11284  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  prodf1  11304  prodfclim1  11306  prodrbdclem  11333  fproddccvg  11334  esum  11357  ege2le3  11366  efexp  11377  efzval  11378  eftlub  11385  effsumlt  11387  ef4p  11389  tanval3ap  11410  efi4p  11413  tan0  11427  efival  11428  tanaddap  11435  cos2t  11446  cos2tsin  11447  ef01bndlem  11452  cos1bnd  11455  cos2bnd  11456  demoivreALT  11469  eirraplem  11472  3dvdsdec  11551  3dvds2dec  11552  odd2np1lem  11558  odd2np1  11559  opoe  11581  omoe  11582  opeo  11583  omeo  11584  m1exp1  11587  n2dvdsm1  11599  flodddiv4  11620  gcdmultiple  11697  sqgcd  11706  nn0seqcvgd  11711  prmind2  11790  hashdvds  11886  phiprmpw  11887  phiprm  11888  expcncf  12750  dvid  12820  dvexp  12833  dvexp2  12834  dveflem  12844  eulerid  12872  cos2pi  12874  sincosq3sgn  12898  sincosq4sgn  12899  cosq23lt0  12903  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  pigt3  12914  abssinper  12916  coskpi  12918  cosq34lt1  12920  ex-fl  12926  trilpolemeq1  13222