MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1cn Unicode version

Axiom ax-1cn 8795
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8771. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn  |-  1  e.  CC

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 8738 . 2  class  1
2 cc 8735 . 2  class  CC
31, 2wcel 1684 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8831  1ex  8833  mulid1  8835  mulid2  8836  1re  8837  muladd11  8982  1p1times  8983  peano2cn  8984  mul02lem2  8989  addid1  8992  cnegex2  8994  addcom  8998  addcomd  9014  0reALT  9143  ine0  9215  mulm1  9221  0lt1  9296  ixi  9397  muleqadd  9412  reccl  9431  recne0  9437  recid  9438  recid2  9439  div1  9453  diveq1  9454  recrec  9457  rec11  9458  rec11r  9459  recdiv  9466  divdiv1  9471  divdiv2  9472  recdiv2  9473  conjmul  9477  rereccl  9478  eqneg  9480  div2neg  9483  subrec  9589  reclt1  9651  recgt1  9652  recp1lt1  9654  recreclt  9655  recgt0ii  9662  inelr  9736  ofnegsub  9744  peano5nni  9749  nn1m1nn  9766  nn1suc  9767  nnaddcl  9768  nnmulcl  9769  nnsub  9784  neg1cn  9813  1m1e0  9814  0p1e1  9839  2m1e1  9841  2p2e4  9842  2times  9843  3p2e5  9855  3p3e6  9856  4p2e6  9857  4p3e7  9858  4p4e8  9859  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  1t1e1  9870  3t3e9  9873  halflt1  9933  1mhlfehlf  9934  8th4div3  9935  halfpm6th  9936  addltmul  9947  elnn0nn  10006  elnnnn0  10007  elz2  10040  zlem1lt  10069  zltlem1  10070  nnaddm1cl  10073  zextlt  10086  zneo  10094  nneo  10095  zeo  10097  peano5uzi  10100  uzindOLD  10106  numsuc  10136  numltc  10144  numsucc  10150  numaddc  10159  6p5lem  10173  4t3lem  10195  7t4e28  10208  decbin2  10228  uzp1  10261  peano2uzr  10274  uzaddcl  10275  rebtwnz  10315  rpnnen1lem5  10346  qbtwnre  10526  lincmb01cmp  10777  iccf1o  10778  xov1plusxeqvd  10780  fz01en  10818  fztp  10841  fzsuc2  10842  fztpval  10845  fseq1m1p1  10858  fzm1  10862  fzoss2  10897  fzval3  10911  fladdz  10950  ceim1l  10957  fldiv  10964  modnegd  11004  uzrdgxfr  11029  fzen2  11031  nn0ennn  11041  seqm1  11063  seqshft2  11072  monoord2  11077  sermono  11078  seqf1olem1  11085  seqf1olem2  11086  seqz  11094  ser1const  11102  expneg  11111  expcl  11121  m1expcl2  11125  expclzlem  11127  expm1t  11130  1exp  11131  mulexpz  11142  expadd  11144  expaddz  11146  expmul  11147  expubnd  11162  sqrecii  11186  irec  11202  i4  11205  binom21  11219  binom3  11222  sq01  11223  zesq  11224  crreczi  11226  bernneq  11227  bernneq2  11228  nn0opthlem1  11283  facnn2  11297  facndiv  11301  faclbnd4lem1  11306  faclbnd6  11312  bcnp1n  11326  bcm1k  11327  bcp1n  11328  bcp1nk  11329  bcn2  11331  bcp1m1  11332  bcpasc  11333  hashgadd  11359  hashfz  11381  hashfzo  11383  hashxplem  11385  hashbclem  11390  hashf1lem2  11394  hashf1  11395  fz1isolem  11399  seqcoll  11401  swrds1  11473  wrdeqcats1  11474  wrdind  11477  revccat  11484  swrds2  11560  rei  11641  imi  11642  resqrex  11736  absi  11771  absexpz  11790  recan  11820  reccn2  12070  iserex  12130  isercolllem1  12138  isercoll2  12142  serf0  12153  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  sumrblem  12184  fsumm1  12216  fsump1  12219  fsumtscopo  12260  fsumparts  12264  hashiun  12280  binomlem  12287  binom  12288  binom1p  12289  binom11  12290  binom1dif  12291  bcxmas  12294  incexc  12296  incexc2  12297  isumsplit  12299  isum1p  12300  climcndslem1  12308  supcvg  12314  harmonic  12317  arisum  12318  arisum2  12319  trireciplem  12320  geoserg  12324  geolim  12326  geolim2  12327  georeclim  12328  geo2sum  12329  geo2sum2  12330  geoisum1c  12336  0.999...  12337  geoihalfsum  12338  cvgrat  12339  mertenslem1  12340  mertenslem2  12341  mertens  12342  ef0lem  12360  esum  12362  ege2le3  12371  efsub  12380  efexp  12381  efzval  12382  eftlub  12389  effsumlt  12391  eft0val  12392  ef4p  12393  tanval3  12414  efi4p  12417  tan0  12431  efival  12432  sinhval  12434  coshval  12435  tanaddlem  12446  tanadd  12447  cos2t  12458  cos2tsin  12459  ef01bndlem  12464  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  demoivreALT  12481  eirrlem  12482  rpnnen2lem3  12495  rpnnen2lem11  12503  ruclem12  12519  odd2np1lem  12586  odd2np1  12587  oddm1even  12588  oddp1even  12589  oexpneg  12590  3dvds  12591  bitsp1o  12624  bitsfzo  12626  bitsf1  12637  sadcp1  12646  gcdmultiple  12729  sqgcd  12737  nn0seqcvgd  12740  prmind2  12769  3prm  12775  qredeu  12786  hashdvds  12843  phiprmpw  12844  phiprm  12845  eulerthlem2  12850  prmdiv  12853  prmdiveq  12854  opoe  12864  omoe  12865  opeo  12866  omeo  12867  iserodd  12888  pcexp  12912  pc2dvds  12931  sumhash  12944  fldivp1  12945  prmpwdvds  12951  pockthlem  12952  pockthi  12954  prmreclem2  12964  prmreclem4  12966  prmreclem6  12968  4sqlem11  13002  4sqlem12  13003  4sqlem19  13010  vdwapun  13021  vdwapid1  13022  vdwlem3  13030  vdwlem5  13032  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwnnlem2  13043  ramub1lem1  13073  ramub1lem2  13074  ramcl  13076  dec5nprm  13081  decexp2  13090  2exp16  13103  prmlem0  13107  prmlem1a  13108  23prm  13120  prmlem2  13121  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  gsumccat  14464  mulgnndir  14589  mulgneg2  14594  mulgnnass  14595  sylow1lem1  14909  sylow2a  14930  efgsval2  15042  efgsrel  15043  efgsres  15047  efgredlemc  15054  odadd2  15141  cncrng  16395  cnfld1  16399  cnfldmulg  16406  zsssubrg  16430  gzrngunit  16437  zrngunit  16438  zcyg  16445  prmirredlem  16446  mulgrhm2  16461  nminvr  18180  blcvx  18304  expcn  18376  iirevcn  18428  iihalf2  18431  icchmeo  18439  icopnfcnv  18440  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  icccvx  18448  evth  18457  lebnumii  18464  htpycom  18474  htpycc  18478  reparphti  18495  pco1  18513  pcohtpylem  18517  pcopt  18520  pcoass  18522  pcorevcl  18523  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  pjthlem1  18801  ovolunlem1a  18855  ovolunlem1  18856  ovolicc2lem4  18879  uniioombllem3  18940  uniioombllem4  18941  dyadovol  18948  opnmbllem  18956  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfi1fseqlem6  19075  iblitg  19123  iblcnlem1  19142  itgcnlem  19144  bddibl  19194  dvid  19267  dvnadd  19278  dvexp  19302  dvexp2  19303  dvmptid  19306  dvcnvlem  19323  dvexp3  19325  dveflem  19326  dvef  19327  dvsincos  19328  dvlipcn  19341  dvivthlem1  19355  lhop2  19362  dvcvx  19367  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  degltp1le  19459  ply1divex  19522  fta1glem1  19551  plyaddlem1  19595  plymullem1  19596  coeidp  19644  dgrid  19645  dgrsub  19653  dgrcolem1  19654  dgrcolem2  19655  dvply1  19664  dvply2g  19665  plydivlem1  19673  plyremlem  19684  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  qaa  19703  iaa  19705  aalioulem3  19714  geolim3  19719  aaliou3lem2  19723  aaliou3lem3  19724  aaliou3lem8  19725  aaliou3lem7  19729  taylply2  19747  dvtaylp  19749  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  dvradcnv  19797  pserdvlem2  19804  pserdv2  19806  abelthlem1  19807  abelthlem2  19808  abelthlem6  19812  abelthlem7  19814  abelth  19817  reeff1olem  19822  reeff1o  19823  efcvx  19825  sinhalfpilem  19834  eulerid  19842  cos2pi  19844  ef2pi  19845  sincosq3sgn  19868  sincosq4sgn  19869  coseq00topi  19870  tangtx  19873  sincos4thpi  19881  sincos6thpi  19883  pige3  19885  abssinper  19886  coskpi  19888  coseq1  19890  efeq1  19891  tanregt0  19901  logneg2  19969  logdivlti  19971  logcnlem4  19992  dvlog2lem  19999  dvlog2  20000  advlog  20001  advlogexp  20002  logtayllem  20006  logtayl  20007  logtayl2  20009  logccv  20010  cxpval  20011  1cxp  20019  cxpcl  20021  cxpp1  20027  cxpmul2  20036  cxpsqr  20050  dvcxp1  20082  dvcxp2  20083  dvsqr  20084  resqrcn  20089  sqrcn  20090  cxpaddlelem  20091  root1id  20094  root1eq1  20095  root1cj  20096  cxpeq  20097  loglesqr  20098  angneg  20101  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  ang180lem5  20111  logrec  20117  isosctrlem1  20118  isosctrlem2  20119  isosctrlem3  20120  affineequiv  20123  affineequiv2  20124  angpieqvdlem  20125  chordthmlem2  20130  chordthmlem3  20131  chordthmlem5  20133  1cubrlem  20137  1cubr  20138  dcubic2  20140  dcubic  20142  mcubic  20143  binom4  20146  dquartlem1  20147  quart1lem  20151  quart1  20152  quartlem1  20153  quart  20157  asinlem  20164  asinlem2  20165  asinlem3a  20166  asinlem3  20167  asinf  20168  atandm2  20173  atandm4  20175  atanf  20176  asinneg  20182  efiasin  20184  sinasin  20185  asinsinlem  20187  asinsin  20188  asin1  20190  acos1  20191  reasinsin  20192  asinbnd  20195  cosasin  20200  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  cosatan  20217  cosatanne0  20218  atantan  20219  atanbndlem  20221  bndatandm  20225  atans2  20227  atansopn  20228  dvatan  20231  atantayl  20233  atantayl2  20234  atantayl3  20235  leibpilem1  20236  leibpilem2  20237  leibpi  20238  log2cnv  20240  log2tlbnd  20241  log2ublem3  20244  log2ub  20245  birthdaylem2  20247  birthday  20249  efrlim  20264  dfef2  20265  cxplim  20266  divsqrsumlem  20274  cvxcl  20279  scvxcvx  20280  logdifbnd  20288  emcllem2  20290  emcllem3  20291  emcllem4  20292  emcllem5  20293  emcllem7  20295  harmonicbnd4  20304  fsumharmonic  20305  wilthlem1  20306  wilthlem2  20307  wilthlem3  20308  ftalem5  20314  basellem2  20319  basellem3  20320  basellem5  20322  basellem6  20323  basellem7  20324  basellem8  20325  basellem9  20326  isnsqf  20373  0sgm  20382  mule1  20386  ppiprm  20389  ppinprm  20390  chtprm  20391  chtnprm  20392  chpp1  20393  mumullem2  20418  sqff1o  20420  musum  20431  muinv  20433  1sgmprm  20438  1sgm2ppw  20439  ppiublem2  20442  ppiub  20443  chtublem  20450  chtub  20451  logfaclbnd  20461  logfacbnd3  20462  logfacrlim  20463  logexprlim  20464  mersenne  20466  perfect1  20467  perfectlem1  20468  perfectlem2  20469  perfect  20470  dchrelbasd  20478  dchr1cl  20490  dchrmulid2  20491  dchrinvcl  20492  dchrfi  20494  dchr1  20496  dchrptlem1  20503  dchrptlem2  20504  dchrsum2  20507  sumdchr2  20509  bcmono  20516  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  bposlem8  20530  bposlem9  20531  lgslem1  20535  lgslem2  20536  lgslem4  20538  lgsfcl2  20541  lgsvalmod  20554  lgsneg  20558  lgsdilem  20561  lgsdir2lem1  20562  lgsdir2lem2  20563  lgsdir2lem3  20564  lgsdir2lem4  20565  lgsdir2lem5  20566  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsne0  20572  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  lgsquad2lem1  20597  lgsquad2  20599  lgsquad3  20600  m1lgs  20601  2sqlem8  20611  2sqlem10  20613  2sqlem11  20614  2sqblem  20616  chtppilimlem2  20623  chtppilim  20624  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  rplogsumlem1  20633  rpvmasumlem  20636  dchrisumlem1  20638  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasum2lem  20645  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem2a  20666  rpvmasum  20675  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  logdivsum  20682  vmalogdivsum2  20687  log2sumbnd  20693  selberg2lem  20699  logdivbnd  20705  pntrmax  20713  pntrsumo1  20714  pntrsumbnd2  20716  selberg34r  20720  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntpbnd1a  20734  pntpbnd2  20736  pntibndlem2  20740  pntlemd  20743  pntlemc  20744  pntlemg  20747  pntlemr  20751  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlem3  20758  pnt2  20762  pnt  20763  ostth2lem2  20783  ex-pr  20817  1kp2ke3k  20833  ex-fl  20834  gxsuc  20939  gxnn0add  20941  gxnn0mul  20944  ablomul  21022  mulid  21023  cnrngo  21070  vc2  21111  vc0  21125  vcm  21127  vcnegneg  21130  vcoprne  21135  nvnncan  21221  nvm1  21230  nvpi  21232  nvmtri  21237  nvge0  21240  smcnlem  21270  ipval2lem3  21278  ipval2lem6  21284  ipidsq  21286  lnoadd  21336  ip1ilem  21404  ip1i  21405  ip2i  21406  ipdirilem  21407  ipasslem1  21409  ipasslem2  21410  ipasslem10  21417  minvecolem2  21454  hvsubid  21605  hvaddsubval  21612  hv2times  21640  hvnegdii  21641  hvsubcan  21653  hvsubcan2  21654  hisubcomi  21683  normlem9  21697  normlem7tALT  21698  norm-ii-i  21716  normsubi  21720  polid2i  21736  hhssnv  21841  pjhthlem1  21970  h1de2bi  22133  homulid2  22380  honegneg  22386  ho2times  22399  lnop0  22546  lnopaddi  22551  lnophmlem2  22597  lnfn0i  22622  lnfnaddi  22623  hst1h  22807  sto2i  22817  stadd3i  22828  superpos  22934  addltmulALT  23026  bcm1n  23032  ltesubnnd  23033  ballotlem2  23047  ballotlemfp1  23050  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemodife  23056  ballotlem4  23057  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  ballotlemsgt1  23069  ballotlemsdom  23070  ballotlemsel1i  23071  ballotlemsi  23073  ballotlemsima  23074  ballotlem1ri  23093  logb1  23405  dya2ub  23575  dya2iocseg  23579  coinflippvt  23685  zetacvg  23689  subfacp1lem1  23710  subfacp1lem5  23715  subfacp1lem6  23716  subfacval2  23718  subfaclim  23719  subfacval3  23720  cvxpcon  23773  cvxscon  23774  rescon  23777  cvmliftlem7  23822  cvmliftlem10  23825  vdgr1b  23895  eupares  23899  eupap1  23900  eupath2lem3  23903  sinccvglem  24005  elfzp1b  24012  relexpadd  24035  sqdivzi  24079  4bc3eq4  24098  halfthird  24100  5recm6rec  24101  predfz  24203  brbtwn2  24533  colinearalglem4  24537  axsegconlem1  24545  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3  24559  ax5seglem4  24560  ax5seglem5  24561  ax5seglem7  24563  ax5seglem9  24565  axbtwnid  24567  axpaschlem  24568  axlowdimlem6  24575  axlowdimlem13  24582  axlowdimlem14  24583  axlowdimlem16  24585  axlowdim  24589  axeuclidlem  24590  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  bpoly0  24785  bpoly1  24786  bpolycl  24787  bpolysum  24788  bpolydiflem  24789  fsumkthpow  24791  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem5  24929  areacirc  24931  3timesi  25178  2eq3m1  25179  cntrset  25602  cnegvex2  25660  mulone  25685  vecscmonto  25686  clscnc  26010  fdc  26455  mettrifi  26473  heiborlem4  26538  heiborlem6  26540  bfp  26548  eldioph2lem1  26839  lzenom  26849  rabren3dioph  26898  irrapxlem1  26907  irrapxlem2  26908  pellexlem2  26915  pell1qrge1  26955  pell1qr1  26956  elpell1qr2  26957  pell1qrgaplem  26958  rmspecsqrnq  26991  rmspecfund  26994  rmxy0  27008  rmxm1  27019  rmym1  27020  2nn0ind  27030  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  jm2.24  27050  acongeq  27070  jm2.18  27081  jm2.19lem3  27084  jm2.25  27092  jm2.16nn0  27097  jm2.27c  27100  jm3.1lem1  27110  jm3.1lem2  27111  rngunsnply  27378  flcidc  27379  psgnunilem5  27417  psgnunilem2  27418  psgnunilem4  27420  m1expaddsub  27421  psgnuni  27422  cnmsgnsubg  27434  cnmsgnbas  27435  cnmsgngrp  27436  proot1ex  27520  ofdivrec  27543  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552  refsum2cnlem1  27708  fmul01lt1lem2  27715  m1expeven  27725  clim1fr1  27727  isumneg  27728  climneg  27736  itgsin0pilem1  27744  itgsinexp  27749  stoweidlem1  27750  stoweidlem7  27756  stoweidlem10  27759  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem16  27765  stoweidlem17  27766  stoweidlem26  27775  stoweidlem34  27783  stoweidlem37  27786  stoweidlem38  27787  stoweidlem41  27790  stoweidlem42  27791  stoweidlem45  27794  stoweidlem51  27800  wallispilem2  27815  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem15  27837  sigaradd  27856  usgraexvlem  28127  sec0  28230  onetansqsecsq  28231  cotsqcscsq  28232  5m4e1  28259
  Copyright terms: Public domain W3C validator