Axiom ax-1cn 7904

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7860. (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 7812	. 2 class 1
2		cc 7809	. 2 class CC
3	1, 2	wcel 2148	1 wff 1 e. CC

This axiom is referenced by:  0cn  7949  1ex  7952  mulrid  7954  mullid  7955  1cnd  7973  muladd11  8090  1p1times  8091  peano2cn  8092  peano2cnm  8223  0reALT  8254  pncan1  8334  npcan1  8335  kcnktkm1cn  8340  ine0  8351  mulm1  8357  mulsubfacd  8375  ixi  8540  inelr  8541  muleqadd  8625  recclap  8636  recap0  8642  recidap  8643  recidap2  8644  div1  8660  1div1e1  8661  diveqap1  8662  recdivap  8675  divdivap1  8680  divdivap2  8681  recdivap2  8682  conjmulap  8686  eqneg  8689  div2negap  8692  recreclt  8857  nn1m1nn  8937  nn1suc  8938  nnaddcl  8939  nnmulcl  8940  nnsub  8958  1m1e0  8988  neg1cn  9024  neg1ne0  9026  neg1ap0  9028  negneg1e1  9029  1pneg1e0  9030  1m0e1  9032  0p1e1  9033  1p0e1  9035  2m1e1  9037  3m1e2  9039  4m1e3  9040  5m1e4  9041  6m1e5  9042  7m1e6  9043  8m1e7  9044  9m1e8  9045  2p2e4  9046  1p2e3  9053  3p2e5  9060  3p3e6  9061  4p2e6  9062  4p3e7  9063  4p4e8  9064  5p2e7  9065  5p3e8  9066  5p4e9  9067  6p2e8  9068  6p3e9  9069  7p2e9  9070  1t1e1  9071  3t3e9  9076  neg1mulneg1e1  9131  1mhlfehlf  9137  8th4div3  9138  halfpm6th  9139  addltmul  9155  elnn0nn  9218  peano2z  9289  zlem1lt  9309  zltlem1  9310  nnaddm1cl  9314  elz2  9324  zextlt  9345  zeo  9358  peano5uzti  9361  numsuc  9397  numltc  9409  numsucc  9423  numaddc  9431  6p5lem  9453  5p5e10  9454  6p4e10  9455  7p3e10  9458  8p2e10  9463  10m1e9  9479  4t3lem  9480  7t4e28  9494  9t11e99  9513  decbin2  9524  halfthird  9526  5recm6rec  9527  uzp1  9561  peano2uzr  9585  uzaddcl  9586  qreccl  9642  iccf1o  10004  fz01en  10053  fztp  10078  fzsuc2  10079  fztpval  10083  fseq1m1p1  10095  elfzp1b  10097  fz0to4untppr  10124  fzoss2  10172  fzval3  10204  fzosplitsnm1  10209  fzo0to42pr  10220  fzosplitprm1  10234  fldiv4p1lem1div2  10305  flqdiv  10321  frecfzen2  10427  nn0ennn  10433  seq3m1  10468  monoord2  10477  ser3mono  10478  expcl  10538  m1expcl2  10542  expclzaplem  10544  expm1t  10548  1exp  10549  mulexpzap  10560  expadd  10562  expaddzap  10564  expmul  10565  expubnd  10577  neg1sqe1  10615  irec  10620  i4  10623  binom21  10633  bernneq  10641  bernneq2  10642  facndiv  10719  faclbnd6  10724  bcnp1n  10739  bcm1k  10740  bcp1nk  10742  bcn2  10744  bcp1m1  10745  bcpasc  10746  4bc3eq4  10753  hashfz  10801  hashfzo  10802  seq3coll  10822  rei  10908  imi  10909  caucvgrelemrec  10988  recan  11118  iserex  11347  serf0  11360  fsumm1  11424  fsump1  11428  telfsumo  11474  fsumparts  11478  hashiun  11486  binomlem  11491  binom  11492  binom1p  11493  binom11  11494  binom1dif  11495  bcxmas  11497  isumsplit  11499  isum1p  11500  arisum  11506  arisum2  11507  trireciplem  11508  geosergap  11514  geolim  11519  geolim2  11520  georeclim  11521  geo2sum  11522  geo2sum2  11523  0.999...  11529  geoihalfsum  11530  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodf1  11550  prodfclim1  11552  prodrbdclem  11579  fproddccvg  11580  prodmodclem2a  11584  fprodntrivap  11592  prodssdc  11597  fprodssdc  11598  esum  11670  ege2le3  11679  efexp  11690  efzval  11691  eftlub  11698  effsumlt  11700  ef4p  11702  tanval3ap  11722  efi4p  11725  tan0  11739  efival  11740  tanaddap  11747  cos2t  11758  cos2tsin  11759  ef01bndlem  11764  cos1bnd  11767  cos2bnd  11768  demoivreALT  11781  eirraplem  11784  3dvdsdec  11870  3dvds2dec  11871  odd2np1lem  11877  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  m1exp1  11906  n2dvdsm1  11918  flodddiv4  11939  gcdmultiple  12021  sqgcd  12030  nn0seqcvgd  12041  prmind2  12120  hashdvds  12221  phiprmpw  12222  phiprm  12223  eulerthlemth  12232  sumhashdc  12345  fldivp1  12346  prmpwdvds  12353  pockthlem  12354  pockthi  12356  mulgnndir  13012  mulgneg2  13017  cnfld1  13469  zsssubrg  13482  expcncf  14095  dvid  14165  dvexp  14178  dvexp2  14179  dveflem  14190  reeff1olem  14195  eulerid  14226  cos2pi  14228  sincosq3sgn  14252  sincosq4sgn  14253  cosq23lt0  14257  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  pigt3  14268  abssinper  14270  coskpi  14272  cosq34lt1  14274  logdivlti  14305  rpcxpp1  14330  rpcxpsqrt  14345  rprelogbdiv  14378  binom4  14400  zabsle1  14403  lgslem1  14404  lgslem2  14405  lgsfcl2  14410  lgsvalmod  14423  lgsneg  14428  lgsdilem  14431  lgsdir2lem1  14432  lgsdir2lem2  14433  lgsdir2lem3  14434  lgsdir2lem5  14436  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461  2sqlem10  14475  ex-fl  14480  trilpolemeq1  14791