Axiom ax-1cn 9004

Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8980. (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 8947	. 2 class 1
2		cc 8944	. 2 class CC
3	1, 2	wcel 1721	1 wff 1 e. CC

This axiom is referenced by:  0cn  9040  1ex  9042  mulid1  9044  mulid2  9045  1re  9046  muladd11  9192  1p1times  9193  peano2cn  9194  mul02lem2  9199  addid1  9202  cnegex2  9204  addcom  9208  addcomd  9224  0reALT  9353  ine0  9425  mulm1  9431  0lt1  9506  ixi  9607  muleqadd  9622  reccl  9641  recne0  9647  recid  9648  recid2  9649  div1  9663  diveq1  9664  recrec  9667  rec11  9668  rec11r  9669  recdiv  9676  divdiv1  9681  divdiv2  9682  recdiv2  9683  conjmul  9687  rereccl  9688  eqneg  9690  div2neg  9693  subrec  9799  reclt1  9861  recgt1  9862  recp1lt1  9864  recreclt  9865  recgt0ii  9872  inelr  9946  ofnegsub  9954  peano5nni  9959  nn1m1nn  9976  nn1suc  9977  nnaddcl  9978  nnmulcl  9979  nnsub  9994  neg1cn  10023  1m1e0  10024  0p1e1  10049  2m1e1  10051  3m1e2  10052  3m1e2OLD  10053  2p2e4  10054  2times  10055  3p2e5  10067  3p3e6  10068  4p2e6  10069  4p3e7  10070  4p4e8  10071  5p2e7  10072  5p3e8  10073  5p4e9  10074  5p5e10  10075  6p2e8  10076  6p3e9  10077  6p4e10  10078  7p2e9  10079  7p3e10  10080  8p2e10  10081  1t1e1  10082  3t3e9  10085  halflt1  10145  1mhlfehlf  10146  8th4div3  10147  halfpm6th  10148  addltmul  10159  elnn0nn  10218  elnnnn0  10219  nn0n0n1ge2  10236  elz2  10254  zlem1lt  10283  zltlem1  10284  nnaddm1cl  10287  zextlt  10300  zneo  10308  nneo  10309  zeo  10311  peano5uzi  10314  uzindOLD  10320  numsuc  10350  numltc  10358  numsucc  10364  numaddc  10373  6p5lem  10387  4t3lem  10409  7t4e28  10422  decbin2  10442  uzp1  10475  peano2uzr  10488  uzaddcl  10489  rebtwnz  10529  rpnnen1lem5  10560  qbtwnre  10741  lincmb01cmp  10994  iccf1o  10995  xov1plusxeqvd  10997  fz01en  11035  fztp  11058  fzsuc2  11060  fztpval  11063  fseq1m1p1  11078  fzm1  11082  fzoss2  11118  fzval3  11135  fzo0to42pr  11141  fladdz  11182  ceim1l  11189  fldiv  11196  modnegd  11236  uzrdgxfr  11261  fzen2  11263  nn0ennn  11273  seqm1  11295  seqshft2  11304  monoord2  11309  sermono  11310  seqf1olem1  11317  seqf1olem2  11318  seqz  11326  ser1const  11334  expneg  11344  expcl  11354  m1expcl2  11358  expclzlem  11360  expm1t  11363  1exp  11364  mulexpz  11375  expadd  11377  expaddz  11379  expmul  11380  expubnd  11395  sqrecii  11419  irec  11435  i4  11438  binom21  11452  binom3  11455  sq01  11456  zesq  11457  crreczi  11459  bernneq  11460  bernneq2  11461  nn0opthlem1  11516  facnn2  11530  facndiv  11534  faclbnd4lem1  11539  faclbnd6  11545  bcnp1n  11560  bcm1k  11561  bcp1n  11562  bcp1nk  11563  bcn2  11565  bcp1m1  11566  bcpasc  11567  bcn2m1  11570  hashgadd  11606  hashfz  11647  hashfzo  11649  hashxplem  11651  hashbclem  11656  hashf1lem2  11660  hashf1  11661  fz1isolem  11665  seqcoll  11667  brfi1indlem  11669  swrds1  11742  wrdeqcats1  11743  wrdind  11746  revccat  11753  swrds2  11835  rei  11916  imi  11917  resqrex  12011  absi  12046  absexpz  12065  recan  12095  reccn2  12345  iserex  12405  isercolllem1  12413  isercoll2  12417  serf0  12429  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  sumrblem  12460  fsumm1  12492  fsump1  12495  fsumtscopo  12536  fsumparts  12540  hashiun  12556  binomlem  12563  binom  12564  binom1p  12565  binom11  12566  binom1dif  12567  bcxmas  12570  incexc  12572  incexc2  12573  isumsplit  12575  isum1p  12576  climcndslem1  12584  supcvg  12590  harmonic  12593  arisum  12594  arisum2  12595  trireciplem  12596  geoserg  12600  geolim  12602  geolim2  12603  georeclim  12604  geo2sum  12605  geo2sum2  12606  geoisum1c  12612  0.999...  12613  geoihalfsum  12614  cvgrat  12615  mertenslem1  12616  mertenslem2  12617  mertens  12618  ef0lem  12636  esum  12638  ege2le3  12647  efsub  12656  efexp  12657  efzval  12658  eftlub  12665  effsumlt  12667  eft0val  12668  ef4p  12669  tanval3  12690  efi4p  12693  tan0  12707  efival  12708  sinhval  12710  coshval  12711  tanaddlem  12722  tanadd  12723  cos2t  12734  cos2tsin  12735  ef01bndlem  12740  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  demoivreALT  12757  eirrlem  12758  rpnnen2lem3  12771  rpnnen2lem11  12779  ruclem12  12795  odd2np1lem  12862  odd2np1  12863  oddm1even  12864  oddp1even  12865  oexpneg  12866  3dvds  12867  bitsp1o  12900  bitsfzo  12902  bitsf1  12913  sadcp1  12922  gcdmultiple  13005  sqgcd  13013  nn0seqcvgd  13016  prmind2  13045  qredeu  13062  hashdvds  13119  phiprmpw  13120  phiprm  13121  eulerthlem2  13126  prmdiv  13129  prmdiveq  13130  opoe  13140  omoe  13141  opeo  13142  omeo  13143  iserodd  13164  pcexp  13188  pc2dvds  13207  sumhash  13220  fldivp1  13221  prmpwdvds  13227  pockthlem  13228  pockthi  13230  prmreclem2  13240  prmreclem4  13242  prmreclem6  13244  4sqlem11  13278  4sqlem12  13279  4sqlem19  13286  vdwapun  13297  vdwapid1  13298  vdwlem3  13306  vdwlem5  13308  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  vdwnnlem2  13319  ramub1lem1  13349  ramub1lem2  13350  ramcl  13352  dec5nprm  13357  decexp2  13366  2exp16  13379  prmlem0  13383  prmlem1a  13384  23prm  13396  prmlem2  13397  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  gsumccat  14742  mulgnndir  14867  mulgneg2  14872  mulgnnass  14873  sylow1lem1  15187  sylow2a  15208  efgsval2  15320  efgsrel  15321  efgsres  15325  efgredlemc  15332  odadd2  15419  cncrng  16677  cnfld1  16681  cnfldmulg  16688  zsssubrg  16712  gzrngunit  16719  zrngunit  16720  zcyg  16727  prmirredlem  16728  mulgrhm2  16743  nminvr  18658  blcvx  18782  expcn  18855  iirevcn  18908  iihalf2  18911  icchmeo  18919  icopnfcnv  18920  icopnfhmeo  18921  iccpnfhmeo  18923  xrhmeo  18924  icccvx  18928  evth  18937  lebnumii  18944  htpycom  18954  reparphti  18975  pcoass  19002  pcorevcl  19003  pcorevlem  19004  pcorev2  19006  pi1xfrcnv  19035  pjthlem1  19291  ovolunlem1a  19345  ovolunlem1  19346  ovolicc2lem4  19369  uniioombllem3  19430  uniioombllem4  19431  dyadovol  19438  opnmbllem  19446  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfi1fseqlem6  19565  iblitg  19613  iblcnlem1  19632  itgcnlem  19634  bddibl  19684  dvid  19757  dvnadd  19768  dvexp  19792  dvexp2  19793  dvmptid  19796  dvcnvlem  19813  dvexp3  19815  dveflem  19816  dvef  19817  dvsincos  19818  dvlipcn  19831  dvivthlem1  19845  lhop2  19852  dvcvx  19857  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  degltp1le  19949  ply1divex  20012  fta1glem1  20041  plyaddlem1  20085  plymullem1  20086  coeidp  20134  dgrid  20135  dgrsub  20143  dgrcolem1  20144  dgrcolem2  20145  dvply1  20154  dvply2g  20155  plydivlem1  20163  plyremlem  20174  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  qaa  20193  iaa  20195  aalioulem3  20204  geolim3  20209  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem7  20219  taylply2  20237  dvtaylp  20239  dvntaylp  20240  taylthlem1  20242  taylthlem2  20243  dvradcnv  20290  pserdvlem2  20297  pserdv2  20299  abelthlem1  20300  abelthlem2  20301  abelthlem6  20305  abelthlem7  20307  abelth  20310  reeff1olem  20315  reeff1o  20316  efcvx  20318  sinhalfpilem  20327  eulerid  20335  cos2pi  20337  ef2pi  20338  sincosq3sgn  20361  sincosq4sgn  20362  coseq00topi  20363  tangtx  20366  sincos4thpi  20374  sincos6thpi  20376  pige3  20378  abssinper  20379  coskpi  20381  coseq1  20383  efeq1  20384  tanregt0  20394  logneg2  20463  logdivlti  20468  logcnlem4  20489  dvlog2lem  20496  dvlog2  20497  advlog  20498  advlogexp  20499  logtayllem  20503  logtayl  20504  logtayl2  20506  logccv  20507  cxpval  20508  1cxp  20516  cxpcl  20518  cxpp1  20524  cxpmul2  20533  cxpsqr  20547  dvcxp1  20579  dvcxp2  20580  dvsqr  20581  resqrcn  20586  sqrcn  20587  cxpaddlelem  20588  root1id  20591  root1eq1  20592  root1cj  20593  cxpeq  20594  loglesqr  20595  angneg  20598  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  ang180lem5  20608  logrec  20614  isosctrlem1  20615  isosctrlem2  20616  isosctrlem3  20617  affineequiv  20620  affineequiv2  20621  angpieqvdlem  20622  chordthmlem2  20627  chordthmlem3  20628  chordthmlem5  20630  1cubrlem  20634  1cubr  20635  dcubic2  20637  dcubic  20639  mcubic  20640  binom4  20643  dquartlem1  20644  quart1lem  20648  quart1  20649  quartlem1  20650  quart  20654  asinlem  20661  asinlem2  20662  asinlem3a  20663  asinlem3  20664  asinf  20665  atandm2  20670  atandm4  20672  atanf  20673  asinneg  20679  efiasin  20681  sinasin  20682  asinsinlem  20684  asinsin  20685  asin1  20687  acos1  20688  reasinsin  20689  asinbnd  20692  cosasin  20697  atanneg  20700  atancj  20703  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  cosatan  20714  cosatanne0  20715  atantan  20716  atanbndlem  20718  bndatandm  20722  atans2  20724  atansopn  20725  dvatan  20728  atantayl  20730  atantayl2  20731  atantayl3  20732  leibpilem1  20733  leibpilem2  20734  leibpi  20735  log2cnv  20737  log2tlbnd  20738  log2ublem3  20741  log2ub  20742  birthdaylem2  20744  birthday  20746  efrlim  20761  dfef2  20762  cxplim  20763  divsqrsumlem  20771  cvxcl  20776  scvxcvx  20777  logdifbnd  20785  emcllem2  20788  emcllem3  20789  emcllem4  20790  emcllem5  20791  emcllem7  20793  harmonicbnd4  20802  fsumharmonic  20803  wilthlem1  20804  wilthlem2  20805  wilthlem3  20806  ftalem5  20812  basellem2  20817  basellem3  20818  basellem5  20820  basellem6  20821  basellem7  20822  basellem8  20823  basellem9  20824  isnsqf  20871  0sgm  20880  mule1  20884  ppiprm  20887  ppinprm  20888  chtprm  20889  chtnprm  20890  chpp1  20891  mumullem2  20916  sqff1o  20918  musum  20929  muinv  20931  1sgmprm  20936  1sgm2ppw  20937  ppiublem2  20940  ppiub  20941  chtublem  20948  chtub  20949  logfaclbnd  20959  logfacbnd3  20960  logfacrlim  20961  logexprlim  20962  mersenne  20964  perfect1  20965  perfectlem1  20966  perfectlem2  20967  perfect  20968  dchrelbasd  20976  dchr1cl  20988  dchrmulid2  20989  dchrinvcl  20990  dchrfi  20992  dchr1  20994  dchrptlem1  21001  dchrptlem2  21002  dchrsum2  21005  sumdchr2  21007  bcmono  21014  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  bposlem8  21028  bposlem9  21029  lgslem1  21033  lgslem2  21034  lgsfcl2  21039  lgsvalmod  21052  lgsneg  21056  lgsdilem  21059  lgsdir2lem1  21060  lgsdir2lem2  21061  lgsdir2lem3  21062  lgsdir2lem4  21063  lgsdir2lem5  21064  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsne0  21070  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  lgsquad2lem1  21095  lgsquad2  21097  lgsquad3  21098  m1lgs  21099  2sqlem8  21109  2sqlem10  21111  2sqlem11  21112  2sqblem  21114  chtppilimlem2  21121  chtppilim  21122  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  rplogsumlem1  21131  rpvmasumlem  21134  dchrisumlem1  21136  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasum2lem  21143  dchrisum0flblem1  21155  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem2a  21164  rpvmasum  21173  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  vmalogdivsum2  21185  selberg2lem  21197  logdivbnd  21203  pntrmax  21211  pntrsumo1  21212  pntrsumbnd2  21214  selberg34r  21218  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntpbnd1a  21232  pntpbnd2  21234  pntibndlem2  21238  pntlemd  21241  pntlemc  21242  pntlemg  21245  pntlemr  21249  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlem3  21256  pnt2  21260  pnt  21261  ostth2lem2  21281  usgraexvlem  21367  cusgrasizeinds  21438  cusgrasize2inds  21439  wlkdvspthlem  21560  fargshiftf1  21577  fargshiftfo  21578  vdgr1b  21628  eupatrl  21643  eupares  21650  eupap1  21651  eupath2lem3  21654  ex-pr  21691  1kp2ke3k  21707  ex-fl  21708  gxsuc  21813  gxnn0add  21815  gxnn0mul  21818  ablomul  21896  mulid  21897  cnrngo  21944  vc2  21987  vc0  22001  vcm  22003  vcnegneg  22006  vcoprne  22011  nvnncan  22097  nvm1  22106  nvpi  22108  nvmtri  22113  nvge0  22116  smcnlem  22146  ipval2lem3  22154  ipval2lem6  22160  ipidsq  22162  lnoadd  22212  ip1ilem  22280  ip1i  22281  ip2i  22282  ipdirilem  22283  ipasslem1  22285  ipasslem2  22286  ipasslem10  22293  minvecolem2  22330  hvsubid  22481  hvaddsubval  22488  hv2times  22516  hvnegdii  22517  hvsubcan  22529  hvsubcan2  22530  hisubcomi  22559  normlem9  22573  normlem7tALT  22574  norm-ii-i  22592  normsubi  22596  polid2i  22612  hhssnv  22717  pjhthlem1  22846  h1de2bi  23009  homulid2  23256  honegneg  23262  ho2times  23275  lnop0  23422  lnopaddi  23427  lnophmlem2  23473  lnfn0i  23498  lnfnaddi  23499  hst1h  23683  sto2i  23693  stadd3i  23704  superpos  23810  addltmulALT  23902  bcm1n  24104  ltesubnnd  24115  qqhval2lem  24318  qqh1  24322  logb1  24356  dya2ub  24573  dya2icoseg  24580  ballotlem2  24699  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemic  24717  ballotlem1c  24718  ballotlemsgt1  24721  ballotlemsdom  24722  ballotlemsel1i  24723  ballotlemsi  24725  ballotlemsima  24726  ballotlem1ri  24745  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamgulm2  24773  lgamcvg2  24792  gamcvg  24793  gamcvg2lem  24796  lgam1  24801  gam1  24802  gamfac  24804  subfacp1lem1  24818  subfacp1lem5  24823  subfacp1lem6  24824  subfacval2  24826  subfaclim  24827  subfacval3  24828  m1expevenALT  24858  cvxpcon  24882  cvxscon  24883  rescon  24886  cvmliftlem7  24931  cvmliftlem10  24934  sinccvglem  25062  elfzp1b  25069  relexpadd  25091  sqdivzi  25137  4bc3eq4  25156  halfthird  25158  5recm6rec  25159  divcnvlin  25165  muls1d  25166  prodf1  25172  prodfclim1  25174  prodfrec  25176  ntrivcvg  25178  ntrivcvgtail  25181  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  fprodntriv  25221  prod1  25223  prodss  25226  fprodss  25227  fprodser  25228  fprodcl  25231  fproddiv  25238  fprodsplit  25242  fprodm1  25243  fprodp1  25245  iprodgam  25272  risefacval2  25279  fallfacval2  25280  risefaccl  25283  fallfaccl  25284  risefacp1  25297  fallfacp1  25298  risefacfac  25301  fallfacfac  25302  fallfacfwd  25303  binomfallfaclem2  25307  binomfallfac  25308  faclimlem1  25310  faclimlem2  25311  faclimlem3  25312  faclim  25313  iprodfac  25314  faclim2  25315  predfz  25417  brbtwn2  25748  colinearalglem4  25752  axsegconlem1  25760  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3  25774  ax5seglem4  25775  ax5seglem5  25776  ax5seglem7  25778  ax5seglem9  25780  axbtwnid  25782  axpaschlem  25783  axlowdimlem6  25790  axlowdimlem13  25797  axlowdimlem14  25798  axlowdimlem16  25800  axeuclidlem  25805  axeuclid  25806  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  bpoly0  26000  bpoly1  26001  bpolycl  26002  bpolysum  26003  bpolydiflem  26004  fsumkthpow  26006  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  ltflcei  26140  mblfinlem  26143  mblfinlem2  26144  0mbf  26151  itg2addnclem2  26156  itg2addnclem3  26157  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem5  26185  areacirc  26187  fdc  26339  mettrifi  26353  heiborlem4  26413  heiborlem6  26415  bfp  26423  eldioph2lem1  26708  lzenom  26718  rabren3dioph  26766  irrapxlem1  26775  irrapxlem2  26776  pellexlem2  26783  pell1qrge1  26823  pell1qr1  26824  elpell1qr2  26825  pell1qrgaplem  26826  rmspecsqrnq  26859  rmspecfund  26862  rmxy0  26876  rmxm1  26887  rmym1  26888  2nn0ind  26898  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  jm2.24  26918  acongeq  26938  jm2.18  26949  jm2.19lem3  26952  jm2.25  26960  jm2.16nn0  26965  jm2.27c  26968  jm3.1lem1  26978  jm3.1lem2  26979  rngunsnply  27246  flcidc  27247  psgnunilem5  27285  psgnunilem2  27286  psgnunilem4  27288  m1expaddsub  27289  psgnuni  27290  cnmsgnsubg  27302  cnmsgnbas  27303  cnmsgngrp  27304  proot1ex  27388  ofdivrec  27411  lhe4.4ex1a  27414  expgrowthi  27418  expgrowth  27420  refsum2cnlem1  27575  fmul01lt1lem2  27582  m1expeven  27592  clim1fr1  27594  isumneg  27595  climneg  27603  itgsin0pilem1  27611  itgsinexp  27616  stoweidlem1  27617  stoweidlem7  27623  stoweidlem10  27626  stoweidlem11  27627  stoweidlem13  27629  stoweidlem14  27630  stoweidlem17  27633  stoweidlem26  27642  stoweidlem34  27650  stoweidlem38  27654  stoweidlem41  27657  stoweidlem42  27658  stoweidlem45  27661  wallispilem2  27682  wallispilem3  27683  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem15  27704  sigaradd  27723  cnm1cn  27968  kcnktkm1cn  27969  ubmelm1fzo  27987  fzosplitsnm1  27991  frghash2spot  28166  usgreghash2spotv  28169  frgregordn0  28173  sec0  28217  onetansqsecsq  28218  cotsqcscsq  28219  5m4e1  28249