Axiom ax-1cn 9994

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

This axiom is referenced by:  0cn  10032  1ex  10035  mulid1  10037  mulid2  10038  1re  10039  1cnd  10056  muladd11  10206  peano2cn  10208  mul02lem2  10213  addid1  10216  cnegex2  10218  peano2cnm  10347  0reALT  10378  ine0  10465  mulm1  10471  0lt1  10550  ixi  10656  muleqadd  10671  reccl  10692  recne0  10698  recid  10699  recid2  10700  div1  10716  1div1e1  10717  diveq1  10718  recdiv  10731  divdiv1  10736  divdiv2  10737  recdiv2  10738  conjmul  10742  eqneg  10745  div2neg  10748  recp1lt1  10921  recreclt  10922  recgt0ii  10929  inelr  11010  ofnegsub  11018  peano5nni  11023  nn1m1nn  11040  nn1suc  11041  nnaddcl  11042  nnmulcl  11043  nnsub  11059  1m1e0  11089  neg1cn  11124  neg1ne0  11126  negneg1e1  11128  1pneg1e0  11129  1m0e1  11131  0p1e1  11132  1p0e1  11133  2m1e1  11135  3m1e2  11137  4m1e3  11138  5m1e4  11139  6m1e5  11140  7m1e6  11141  8m1e7  11142  9m1e8  11143  2p2e4  11144  1p2e3  11152  3p2e5  11160  3p3e6  11161  4p2e6  11162  4p3e7  11163  4p4e8  11164  5p2e7  11165  5p3e8  11166  5p4e9  11167  5p5e10OLD  11168  6p2e8  11169  6p3e9  11170  6p4e10OLD  11171  7p2e9  11172  7p3e10OLD  11173  8p2e10OLD  11174  1t1e1  11175  3t3e9  11180  neg1mulneg1e1  11245  1mhlfehlf  11251  8th4div3  11252  halfpm6th  11253  addltmul  11268  elnn0nn  11335  elz2  11394  zlem1lt  11429  zltlem1  11430  nnaddm1cl  11434  zextlt  11451  zeo  11463  peano5uzi  11466  numsuc  11511  numltc  11528  numsucc  11549  numaddc  11561  6p5lem  11595  5p5e10  11596  6p4e10  11598  7p3e10  11603  8p2e10  11610  10m1e9  11630  4t3lem  11631  7t4e28  11650  9t11e99  11671  9t11e99OLD  11672  decbin2  11683  halfthird  11685  5recm6rec  11686  uzp1  11721  peano2uzr  11743  uzaddcl  11744  rebtwnz  11787  qbtwnre  12030  iccf1o  12316  fz01en  12369  fztp  12397  fzsuc2  12398  fztpval  12402  fseq1m1p1  12415  elfzp1b  12417  fz0to4untppr  12442  predfz  12464  fzoss2  12496  fzval3  12536  fzosplitsnm1  12542  fzo0to42pr  12555  fzo1to4tp  12556  fldiv4p1lem1div2  12636  ceim1l  12646  fldiv  12659  uzrdgxfr  12766  fzen2  12768  nn0ennn  12778  seqm1  12818  seqshft2  12827  monoord2  12832  sermono  12833  seqf1olem1  12840  seqf1olem2  12841  seqz  12849  ser1const  12857  expcl  12878  m1expcl2  12882  expclzlem  12884  expm1t  12888  1exp  12889  mulexpz  12900  expadd  12902  expaddz  12904  expmul  12905  expubnd  12921  sqrecii  12946  neg1sqe1  12959  irec  12964  i4  12967  binom21  12980  sq01  12986  crreczi  12989  bernneq  12990  bernneq2  12991  nn0opthlem1  13055  facndiv  13075  faclbnd4lem1  13080  faclbnd6  13086  bcnp1n  13101  bcm1k  13102  bcp1nk  13104  bcn2  13106  bcp1m1  13107  bcpasc  13108  4bc3eq4  13115  hashgadd  13166  hashfz  13214  hashfzo  13216  hashxplem  13220  hashbclem  13236  hashf1  13241  seqcoll  13248  swrds1  13451  swrdlsw  13452  wrdind  13476  wrd2ind  13477  swrds2  13685  relexpaddg  13793  rei  13896  imi  13897  recan  14076  iserex  14387  isercoll2  14399  serf0  14411  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  sumrblem  14442  fsumm1  14480  fsump1  14487  telfsumo  14534  fsumparts  14538  hashiun  14554  binomlem  14561  binom  14562  binom1p  14563  binom11  14564  binom1dif  14565  bcxmas  14567  isumsplit  14572  isum1p  14573  climcndslem1  14581  supcvg  14588  harmonic  14591  arisum  14592  arisum2  14593  trireciplem  14594  geoserg  14598  geolim  14601  geolim2  14602  georeclim  14603  geo2sum  14604  geo2sum2  14605  geoisum1c  14611  0.999...  14612  0.999...OLD  14613  geoihalfsum  14614  cvgrat  14615  mertenslem1  14616  mertenslem2  14617  mertens  14618  prodf1  14623  prodfclim1  14625  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  fprodntriv  14672  prodss  14677  fprodss  14678  fprodsplit  14696  fprodn0f  14722  fprodclf  14723  risefaccl  14746  fallfaccl  14747  risefacfac  14766  binomfallfac  14772  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  bpoly2  14788  bpoly3  14789  bpoly4  14790  fsumcube  14791  esum  14811  ege2le3  14820  efsub  14830  efexp  14831  efzval  14832  eftlub  14839  effsumlt  14841  ef4p  14843  tanval3  14864  efi4p  14867  tan0  14881  efival  14882  tanadd  14897  cos2t  14908  cos2tsin  14909  ef01bndlem  14914  cos1bnd  14917  cos2bnd  14918  demoivreALT  14931  eirrlem  14932  rpnnen2lem3  14945  rpnnen2lem11  14953  ruclem12  14970  3dvds  15052  3dvdsOLD  15053  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  odd2np1lem  15064  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  m1exp1  15093  n2dvdsm1  15105  flodddiv4  15137  bitsfzo  15157  gcdmultiple  15269  sqgcd  15278  nn0seqcvgd  15283  prmind2  15398  hashdvds  15480  phiprmpw  15481  phiprm  15482  eulerthlem2  15487  iserodd  15540  sumhash  15600  fldivp1  15601  prmpwdvds  15608  pockthlem  15609  pockthi  15611  prmreclem4  15623  prmreclem6  15625  4sqlem11  15659  4sqlem19  15667  vdwapun  15678  vdwapid1  15679  vdwlem3  15687  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  vdwnnlem2  15700  ramub1lem1  15730  ramub1lem2  15731  ramcl  15733  prmo1  15741  dec5nprm  15770  decexp2  15779  prmlem0  15812  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  prmo4  15835  prmo5  15836  prmo6  15837  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  gsumccat  17378  mulgnndir  17569  mulgnndirOLD  17570  mulgneg2  17575  m1expaddsub  17918  sylow1lem1  18013  sylow2a  18034  efgsval2  18146  efgsrel  18147  efgsres  18151  cnfld1  19771  zsssubrg  19804  cnmgpid  19808  zringcyg  19839  mulgrhm2  19847  cnmsgnsubg  19923  cnmsgnbas  19924  cnmsgngrp  19925  psgninv  19928  evpmodpmf1o  19942  blcvx  22601  iihalf2  22732  icopnfcnv  22741  iccpnfhmeo  22744  xrhmeo  22745  icccvx  22749  lebnumii  22765  reparphti  22797  pcoass  22824  pcorevlem  22826  pcorev2  22828  pi1xfrcnv  22857  cnstrcvs  22941  cncvs  22945  ncvsm1  22954  pjthlem1  23208  divcncf  23216  ovolunlem1a  23264  ovolunlem1  23265  ovolicc2lem4  23288  uniioombllem3  23353  uniioombllem4  23354  dyadovol  23361  vitalilem4  23380  iblitg  23535  iblcnlem1  23554  itgcnlem  23556  dvid  23681  dvexp  23716  dvexp2  23717  dvexp3  23741  dveflem  23742  dvef  23743  dvlipcn  23757  dvcvx  23783  dvfsumle  23784  dvfsumlem1  23789  degltp1le  23833  ply1divex  23896  fta1glem1  23925  plyaddlem1  23969  plymullem1  23970  coeidp  24019  dgrid  24020  dvply1  24039  dvply2g  24040  plyremlem  24059  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  qaa  24078  iaa  24080  aalioulem3  24089  geolim3  24094  aaliou3lem2  24098  aaliou3lem7  24104  taylply2  24122  dvradcnv  24175  pserdvlem2  24182  pserdv2  24184  abelthlem1  24185  abelthlem2  24186  abelthlem6  24190  abelthlem7  24192  abelth  24195  reeff1olem  24200  reeff1o  24201  efcvx  24203  sinhalfpilem  24215  eulerid  24226  cos2pi  24228  sincosq3sgn  24252  sincosq4sgn  24253  tangtx  24257  sincos4thpi  24265  sincos6thpi  24267  pige3  24269  abssinper  24270  coskpi  24272  coseq1  24274  efeq1  24275  tanregt0  24285  logneg2  24361  logdivlti  24366  logcnlem4  24391  dvlog2lem  24398  dvlog2  24399  advlog  24400  advlogexp  24401  logtayl  24406  logtayl2  24408  logccv  24409  cxpval  24410  1cxp  24418  cxpcl  24420  cxpp1  24426  cxpsqrt  24449  dvsqrt  24483  dvcnsqrt  24485  sqrtcn  24491  cxpaddlelem  24492  root1id  24495  root1cj  24497  logrec  24501  logb1  24507  logbmpt  24526  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  isosctrlem1  24548  isosctrlem2  24549  1cubrlem  24568  1cubr  24569  mcubic  24574  binom4  24577  dquartlem1  24578  quartlem1  24584  asinlem  24595  asinlem2  24596  asinlem3a  24597  asinlem3  24598  asinf  24599  atandm2  24604  atandm4  24606  atanf  24607  asinneg  24613  efiasin  24615  sinasin  24616  asinsin  24619  asin1  24621  acos1  24622  reasinsin  24623  asinbnd  24626  cosasin  24631  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atanlogsub  24643  efiatan2  24644  2efiatan  24645  tanatan  24646  cosatan  24648  cosatanne0  24649  atantan  24650  atanbndlem  24652  bndatandm  24656  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  atantayl3  24666  leibpilem1  24667  leibpilem2  24668  leibpi  24669  log2cnv  24671  log2tlbnd  24672  log2ublem3  24675  log2ub  24676  birthdaylem2  24679  birthday  24681  efrlim  24696  dfef2  24697  cvxcl  24711  scvxcvx  24712  emcllem2  24723  emcllem4  24725  emcllem7  24728  harmonicbnd4  24737  fsumharmonic  24738  zetacvg  24741  lgamcvg2  24781  lgam1  24790  gam1  24791  wilthlem1  24794  wilthlem2  24795  wilthlem3  24796  basellem2  24808  basellem5  24811  basellem6  24812  basellem7  24813  basellem8  24814  basellem9  24815  0sgm  24870  mule1  24874  ppiprm  24877  ppinprm  24878  chtprm  24879  chtnprm  24880  chpp1  24881  mumullem2  24906  1sgmprm  24924  1sgm2ppw  24925  ppiublem2  24928  ppiub  24929  chtublem  24936  chtub  24937  logfaclbnd  24947  logfacbnd3  24948  logfacrlim  24949  logexprlim  24950  mersenne  24952  perfect1  24953  perfectlem1  24954  perfectlem2  24955  perfect  24956  dchrelbasd  24964  dchrmulid2  24977  dchrfi  24980  dchrsum2  24993  sumdchr2  24995  bcp1ctr  25004  bposlem8  25016  zabsle1  25021  lgslem1  25022  lgslem2  25023  lgsfcl2  25028  lgsvalmod  25041  lgsneg  25046  lgsdilem  25049  lgsdir2lem1  25050  lgsdir2lem2  25051  lgsdir2lem3  25052  lgsdir2lem5  25054  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsne0  25060  lgseisenlem1  25100  lgseisenlem2  25101  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquad2lem1  25109  lgsquad2  25111  m1lgs  25113  2lgslem3c  25123  2lgsoddprmlem3b  25136  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  2sqlem10  25153  2sqlem11  25154  2sqblem  25156  chtppilimlem2  25163  chebbnd2  25166  chto1lb  25167  rplogsumlem1  25173  rpvmasumlem  25176  dchrmusumlema  25182  dchrmusum2  25183  dchrisum0flblem1  25197  rpvmasum2  25201  mudivsum  25219  mulogsum  25221  vmalogdivsum2  25227  selberg2lem  25239  logdivbnd  25245  pntrmax  25253  pntrsumo1  25254  pntrsumbnd2  25256  pntrlog2bndlem5  25270  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemd  25283  pntlemc  25284  pntlemr  25291  brbtwn2  25785  colinearalglem4  25789  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem7  25815  ax5seglem9  25817  axbtwnid  25819  axpaschlem  25820  axlowdimlem13  25834  axlowdimlem14  25835  axlowdimlem16  25837  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  crctcshwlkn0lem6  26707  wwlksnext  26788  clwwlksf1  26917  wwlksext2clwwlk  26924  numclwwlkovf2exlem2  27212  ex-fl  27304  ex-ind-dvds  27318  vc2OLD  27423  vc0  27429  vcm  27431  nvm1  27520  nvmtri  27526  nvge0  27528  ipval2lem3  27560  ipidsq  27565  lnoadd  27613  ip1ilem  27681  ip1i  27682  ip2i  27683  ipdirilem  27684  ipasslem1  27686  ipasslem2  27687  ipasslem10  27694  minvecolem2  27731  hvsubid  27883  hv2times  27918  hisubcomi  27961  normlem9  27975  normlem7tALT  27976  norm-ii-i  27994  normsubi  27998  hhssnv  28121  pjhthlem1  28250  h1de2bi  28413  homulid2  28659  ho2times  28678  lnop0  28825  lnopaddi  28830  lnophmlem2  28876  lnfn0i  28901  lnfnaddi  28902  hst1h  29086  sto2i  29096  stadd3i  29107  addltmulALT  29305  dpmul4  29622  isarchi3  29741  archirngz  29743  psgnid  29847  lmatfvlem  29881  qqhval2lem  30025  dya2ub  30332  omssubadd  30362  eulerpartlemgs2  30442  fib5  30467  fib6  30468  ballotlem2  30550  sgnneg  30602  signswch  30638  signlem0  30664  itgexpif  30684  reprlt  30697  breprexp  30711  breprexpnat  30712  hgt750lem2  30730  subfacp1lem5  31166  subfacp1lem6  31167  subfacval2  31169  subfaclim  31170  subfacval3  31171  cvxsconn  31225  resconn  31228  cvmliftlem7  31273  cvmliftlem10  31276  problem4  31562  sinccvglem  31566  sqdivzi  31610  faclimlem1  31629  dnibndlem5  32472  dnibndlem10  32477  ltflcei  33397  sin2h  33399  cos2h  33400  tan2h  33401  pigt3  33402  poimirlem13  33422  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem31  33440  mblfinlem2  33447  mblfinlem3  33448  0mbf  33455  dvtan  33460  itg2addnclem3  33463  dvasin  33496  dvacos  33497  areacirc  33505  fdc  33541  mettrifi  33553  heiborlem4  33613  heiborlem6  33615  eldioph2lem1  37323  lzenom  37333  irrapxlem1  37386  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  rmxm1  37499  rmym1  37500  2nn0ind  37510  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  jm2.24  37530  acongeq  37550  jm2.18  37555  jm2.27c  37574  jm3.1lem2  37585  rngunsnply  37743  flcidc  37744  inductionexd  38453  unitadd  38498  hashnzfzclim  38521  ofdivrec  38525  lhe4.4ex1a  38528  expgrowth  38534  dvradcnv2  38546  binomcxplemrat  38549  binomcxplemnotnn0  38555  isosctrlem1ALT  39170  dvsinax  40127  dvnprodlem3  40163  itgsin0pilem1  40165  itgsbtaddcnst  40198  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  stoweidlem38  40255  wallispilem2  40283  wallispilem4  40285  wallispi2lem1  40288  stirlinglem1  40291  stirlinglem5  40295  stirlinglem10  40300  dirkerper  40313  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem4  40323  fourierdlem24  40348  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  1t10e1p1e11  41319  1t10e1p1e11OLD  41320  fmtnorec3  41460  fmtno5lem4  41468  fmtno5  41469  257prm  41473  fmtno4nprmfac193  41486  m3prm  41506  139prmALT  41511  127prm  41515  m7prm  41516  lighneallem3  41524  proththd  41531  3exp4mod41  41533  41prothprmlem2  41535  perfectALTVlem2  41631  perfectALTV  41632  evengpop3  41686  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  0nodd  41810  altgsumbcALT  42131  exple2lt6  42145  nn0sumshdiglemB  42414  onetansqsecsq  42502  cotsqcscsq  42503  5m4e1  42543