Axiom ax-1cn 8053

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

This axiom is referenced by:  0cn  8099  1ex  8102  mulrid  8104  mullid  8105  1cnd  8123  muladd11  8240  1p1times  8241  peano2cn  8242  peano2cnm  8373  0reALT  8404  pncan1  8484  npcan1  8485  kcnktkm1cn  8490  ine0  8501  mulm1  8507  mulsubfacd  8526  ixi  8691  inelr  8692  muleqadd  8776  recclap  8787  recap0  8793  recidap  8794  recidap2  8795  div1  8811  1div1e1  8812  diveqap1  8813  recdivap  8826  divdivap1  8831  divdivap2  8832  recdivap2  8833  conjmulap  8837  eqneg  8840  div2negap  8843  recreclt  9008  ofnegsub  9070  nn1m1nn  9089  nn1suc  9090  nnaddcl  9091  nnmulcl  9092  nnsub  9110  1m1e0  9140  neg1cn  9176  neg1ne0  9178  neg1ap0  9180  negneg1e1  9181  1pneg1e0  9182  1m0e1  9184  0p1e1  9185  1p0e1  9187  2m1e1  9189  3m1e2  9191  4m1e3  9192  5m1e4  9193  6m1e5  9194  7m1e6  9195  8m1e7  9196  9m1e8  9197  2p2e4  9198  1p2e3  9206  3p2e5  9213  3p3e6  9214  4p2e6  9215  4p3e7  9216  4p4e8  9217  5p2e7  9218  5p3e8  9219  5p4e9  9220  6p2e8  9221  6p3e9  9222  7p2e9  9223  1t1e1  9224  3t3e9  9229  neg1mulneg1e1  9284  1mhlfehlf  9290  8th4div3  9291  halfpm6th  9292  addltmul  9309  elnn0nn  9372  peano2z  9443  zlem1lt  9464  zltlem1  9465  nnaddm1cl  9469  elz2  9479  zextlt  9500  zeo  9513  peano5uzti  9516  numsuc  9552  numltc  9564  numsucc  9578  numaddc  9586  6p5lem  9608  5p5e10  9609  6p4e10  9610  7p3e10  9613  8p2e10  9618  10m1e9  9634  4t3lem  9635  7t4e28  9649  9t11e99  9668  decbin2  9679  halfthird  9681  5recm6rec  9682  uzp1  9717  peano2uzr  9741  uzaddcl  9742  qreccl  9798  iccf1o  10161  fz01en  10210  fztp  10235  fzsuc2  10236  fztpval  10240  fseq1m1p1  10252  elfzp1b  10254  fz0to4untppr  10281  fzoss2  10331  fzval3  10370  fzosplitsnm1  10375  fzo0to42pr  10386  fzosplitprm1  10400  fldiv4p1lem1div2  10485  flqdiv  10503  frecfzen2  10609  nn0ennn  10615  xnn0nnen  10619  seq3m1  10655  seqshft2g  10664  monoord2  10668  ser3mono  10669  seqf1oglem1  10701  seqf1oglem2  10702  expcl  10739  m1expcl2  10743  expclzaplem  10745  expm1t  10749  1exp  10750  mulexpzap  10761  expadd  10763  expaddzap  10765  expmul  10766  expubnd  10778  neg1sqe1  10816  irec  10821  i4  10824  binom21  10834  bernneq  10842  bernneq2  10843  facndiv  10921  faclbnd6  10926  bcnp1n  10941  bcm1k  10942  bcp1nk  10944  bcn2  10946  bcp1m1  10947  bcpasc  10948  4bc3eq4  10955  hashfz  11003  hashfzo  11004  seq3coll  11024  swrds1  11159  swrdlsw  11160  wrdind  11213  wrd2ind  11214  rei  11325  imi  11326  caucvgrelemrec  11405  recan  11535  iserex  11765  serf0  11778  fsumm1  11842  fsump1  11846  telfsumo  11892  fsumparts  11896  hashiun  11904  binomlem  11909  binom  11910  binom1p  11911  binom11  11912  binom1dif  11913  bcxmas  11915  isumsplit  11917  isum1p  11918  arisum  11924  arisum2  11925  trireciplem  11926  geosergap  11932  geolim  11937  geolim2  11938  georeclim  11939  geo2sum  11940  geo2sum2  11941  0.999...  11947  geoihalfsum  11948  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodf1  11968  prodfclim1  11970  prodrbdclem  11997  fproddccvg  11998  prodmodclem2a  12002  fprodntrivap  12010  prodssdc  12015  fprodssdc  12016  esum  12088  ege2le3  12097  efexp  12108  efzval  12109  eftlub  12116  effsumlt  12118  ef4p  12120  tanval3ap  12140  efi4p  12143  tan0  12157  efival  12158  tanaddap  12165  cos2t  12176  cos2tsin  12177  ef01bndlem  12182  cos1bnd  12185  cos2bnd  12186  demoivreALT  12200  eirraplem  12203  3dvds  12290  3dvdsdec  12291  3dvds2dec  12292  odd2np1lem  12298  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  m1exp1  12327  n2dvdsm1  12339  flodddiv4  12362  bitsfzo  12381  gcdmultiple  12456  sqgcd  12465  nn0seqcvgd  12478  prmind2  12557  hashdvds  12658  phiprmpw  12659  phiprm  12660  eulerthlemth  12669  sumhashdc  12785  fldivp1  12786  prmpwdvds  12793  pockthlem  12794  pockthi  12796  4sqlem11  12839  4sqlem19  12847  dec5nprm  12852  mulgnndir  13602  mulgneg2  13607  cnfld1  14449  zsssubrg  14462  mulgrhm2  14487  expcncf  15196  divcncfap  15201  hovercncf  15233  dvid  15282  dvidre  15284  dvexp  15298  dvexp2  15299  dveflem  15313  plyaddlem1  15334  plymullem1  15335  dvply1  15352  reeff1olem  15358  eulerid  15389  cos2pi  15391  sincosq3sgn  15415  sincosq4sgn  15416  cosq23lt0  15420  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  pigt3  15431  abssinper  15433  coskpi  15435  cosq34lt1  15437  logdivlti  15468  rpcxpp1  15493  rpcxpsqrt  15509  rprelogbdiv  15544  binom4  15566  wilthlem1  15567  0sgm  15572  1sgmprm  15581  1sgm2ppw  15582  mersenne  15584  perfect1  15585  perfectlem1  15586  perfectlem2  15587  perfect  15588  zabsle1  15591  lgslem1  15592  lgslem2  15593  lgsfcl2  15598  lgsvalmod  15611  lgsneg  15616  lgsdilem  15619  lgsdir2lem1  15620  lgsdir2lem2  15621  lgsdir2lem3  15622  lgsdir2lem5  15624  lgsne0  15630  lgseisenlem1  15662  lgseisenlem2  15663  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  lgsquad2  15675  m1lgs  15677  2lgslem3c  15687  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  2sqlem10  15717  ex-fl  15861  trilpolemeq1  16181