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

Axiom ax-1cn 8811
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8787. (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 8754 . 2  class  1
2 cc 8751 . 2  class  CC
31, 2wcel 1696 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8847  1ex  8849  mulid1  8851  mulid2  8852  1re  8853  muladd11  8998  1p1times  8999  peano2cn  9000  mul02lem2  9005  addid1  9008  cnegex2  9010  addcom  9014  addcomd  9030  0reALT  9159  ine0  9231  mulm1  9237  0lt1  9312  ixi  9413  muleqadd  9428  reccl  9447  recne0  9453  recid  9454  recid2  9455  div1  9469  diveq1  9470  recrec  9473  rec11  9474  rec11r  9475  recdiv  9482  divdiv1  9487  divdiv2  9488  recdiv2  9489  conjmul  9493  rereccl  9494  eqneg  9496  div2neg  9499  subrec  9605  reclt1  9667  recgt1  9668  recp1lt1  9670  recreclt  9671  recgt0ii  9678  inelr  9752  ofnegsub  9760  peano5nni  9765  nn1m1nn  9782  nn1suc  9783  nnaddcl  9784  nnmulcl  9785  nnsub  9800  neg1cn  9829  1m1e0  9830  0p1e1  9855  2m1e1  9857  2p2e4  9858  2times  9859  3p2e5  9871  3p3e6  9872  4p2e6  9873  4p3e7  9874  4p4e8  9875  5p2e7  9876  5p3e8  9877  5p4e9  9878  5p5e10  9879  6p2e8  9880  6p3e9  9881  6p4e10  9882  7p2e9  9883  7p3e10  9884  8p2e10  9885  1t1e1  9886  3t3e9  9889  halflt1  9949  1mhlfehlf  9950  8th4div3  9951  halfpm6th  9952  addltmul  9963  elnn0nn  10022  elnnnn0  10023  elz2  10056  zlem1lt  10085  zltlem1  10086  nnaddm1cl  10089  zextlt  10102  zneo  10110  nneo  10111  zeo  10113  peano5uzi  10116  uzindOLD  10122  numsuc  10152  numltc  10160  numsucc  10166  numaddc  10175  6p5lem  10189  4t3lem  10211  7t4e28  10224  decbin2  10244  uzp1  10277  peano2uzr  10290  uzaddcl  10291  rebtwnz  10331  rpnnen1lem5  10362  qbtwnre  10542  lincmb01cmp  10793  iccf1o  10794  xov1plusxeqvd  10796  fz01en  10834  fztp  10857  fzsuc2  10858  fztpval  10861  fseq1m1p1  10874  fzm1  10878  fzoss2  10913  fzval3  10927  fladdz  10966  ceim1l  10973  fldiv  10980  modnegd  11020  uzrdgxfr  11045  fzen2  11047  nn0ennn  11057  seqm1  11079  seqshft2  11088  monoord2  11093  sermono  11094  seqf1olem1  11101  seqf1olem2  11102  seqz  11110  ser1const  11118  expneg  11127  expcl  11137  m1expcl2  11141  expclzlem  11143  expm1t  11146  1exp  11147  mulexpz  11158  expadd  11160  expaddz  11162  expmul  11163  expubnd  11178  sqrecii  11202  irec  11218  i4  11221  binom21  11235  binom3  11238  sq01  11239  zesq  11240  crreczi  11242  bernneq  11243  bernneq2  11244  nn0opthlem1  11299  facnn2  11313  facndiv  11317  faclbnd4lem1  11322  faclbnd6  11328  bcnp1n  11342  bcm1k  11343  bcp1n  11344  bcp1nk  11345  bcn2  11347  bcp1m1  11348  bcpasc  11349  hashgadd  11375  hashfz  11397  hashfzo  11399  hashxplem  11401  hashbclem  11406  hashf1lem2  11410  hashf1  11411  fz1isolem  11415  seqcoll  11417  swrds1  11489  wrdeqcats1  11490  wrdind  11493  revccat  11500  swrds2  11576  rei  11657  imi  11658  resqrex  11752  absi  11787  absexpz  11806  recan  11836  reccn2  12086  iserex  12146  isercolllem1  12154  isercoll2  12158  serf0  12169  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  sumrblem  12200  fsumm1  12232  fsump1  12235  fsumtscopo  12276  fsumparts  12280  hashiun  12296  binomlem  12303  binom  12304  binom1p  12305  binom11  12306  binom1dif  12307  bcxmas  12310  incexc  12312  incexc2  12313  isumsplit  12315  isum1p  12316  climcndslem1  12324  supcvg  12330  harmonic  12333  arisum  12334  arisum2  12335  trireciplem  12336  geoserg  12340  geolim  12342  geolim2  12343  georeclim  12344  geo2sum  12345  geo2sum2  12346  geoisum1c  12352  0.999...  12353  geoihalfsum  12354  cvgrat  12355  mertenslem1  12356  mertenslem2  12357  mertens  12358  ef0lem  12376  esum  12378  ege2le3  12387  efsub  12396  efexp  12397  efzval  12398  eftlub  12405  effsumlt  12407  eft0val  12408  ef4p  12409  tanval3  12430  efi4p  12433  tan0  12447  efival  12448  sinhval  12450  coshval  12451  tanaddlem  12462  tanadd  12463  cos2t  12474  cos2tsin  12475  ef01bndlem  12480  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  demoivreALT  12497  eirrlem  12498  rpnnen2lem3  12511  rpnnen2lem11  12519  ruclem12  12535  odd2np1lem  12602  odd2np1  12603  oddm1even  12604  oddp1even  12605  oexpneg  12606  3dvds  12607  bitsp1o  12640  bitsfzo  12642  bitsf1  12653  sadcp1  12662  gcdmultiple  12745  sqgcd  12753  nn0seqcvgd  12756  prmind2  12785  3prm  12791  qredeu  12802  hashdvds  12859  phiprmpw  12860  phiprm  12861  eulerthlem2  12866  prmdiv  12869  prmdiveq  12870  opoe  12880  omoe  12881  opeo  12882  omeo  12883  iserodd  12904  pcexp  12928  pc2dvds  12947  sumhash  12960  fldivp1  12961  prmpwdvds  12967  pockthlem  12968  pockthi  12970  prmreclem2  12980  prmreclem4  12982  prmreclem6  12984  4sqlem11  13018  4sqlem12  13019  4sqlem19  13026  vdwapun  13037  vdwapid1  13038  vdwlem3  13046  vdwlem5  13048  vdwlem6  13049  vdwlem8  13051  vdwlem9  13052  vdwnnlem2  13059  ramub1lem1  13089  ramub1lem2  13090  ramcl  13092  dec5nprm  13097  decexp2  13106  2exp16  13119  prmlem0  13123  prmlem1a  13124  23prm  13136  prmlem2  13137  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  gsumccat  14480  mulgnndir  14605  mulgneg2  14610  mulgnnass  14611  sylow1lem1  14925  sylow2a  14946  efgsval2  15058  efgsrel  15059  efgsres  15063  efgredlemc  15070  odadd2  15157  cncrng  16411  cnfld1  16415  cnfldmulg  16422  zsssubrg  16446  gzrngunit  16453  zrngunit  16454  zcyg  16461  prmirredlem  16462  mulgrhm2  16477  nminvr  18196  blcvx  18320  expcn  18392  iirevcn  18444  iihalf2  18447  icchmeo  18455  icopnfcnv  18456  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  icccvx  18464  evth  18473  lebnumii  18480  htpycom  18490  htpycc  18494  reparphti  18511  pco1  18529  pcohtpylem  18533  pcopt  18536  pcoass  18538  pcorevcl  18539  pcorevlem  18540  pcorev2  18542  pi1xfrcnv  18571  pjthlem1  18817  ovolunlem1a  18871  ovolunlem1  18872  ovolicc2lem4  18895  uniioombllem3  18956  uniioombllem4  18957  dyadovol  18964  opnmbllem  18972  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfi1fseqlem6  19091  iblitg  19139  iblcnlem1  19158  itgcnlem  19160  bddibl  19210  dvid  19283  dvnadd  19294  dvexp  19318  dvexp2  19319  dvmptid  19322  dvcnvlem  19339  dvexp3  19341  dveflem  19342  dvef  19343  dvsincos  19344  dvlipcn  19357  dvivthlem1  19371  lhop2  19378  dvcvx  19383  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem2  19390  degltp1le  19475  ply1divex  19538  fta1glem1  19567  plyaddlem1  19611  plymullem1  19612  coeidp  19660  dgrid  19661  dgrsub  19669  dgrcolem1  19670  dgrcolem2  19671  dvply1  19680  dvply2g  19681  plydivlem1  19689  plyremlem  19700  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  qaa  19719  iaa  19721  aalioulem3  19730  geolim3  19735  aaliou3lem2  19739  aaliou3lem3  19740  aaliou3lem8  19741  aaliou3lem7  19745  taylply2  19763  dvtaylp  19765  dvntaylp  19766  taylthlem1  19768  taylthlem2  19769  dvradcnv  19813  pserdvlem2  19820  pserdv2  19822  abelthlem1  19823  abelthlem2  19824  abelthlem6  19828  abelthlem7  19830  abelth  19833  reeff1olem  19838  reeff1o  19839  efcvx  19841  sinhalfpilem  19850  eulerid  19858  cos2pi  19860  ef2pi  19861  sincosq3sgn  19884  sincosq4sgn  19885  coseq00topi  19886  tangtx  19889  sincos4thpi  19897  sincos6thpi  19899  pige3  19901  abssinper  19902  coskpi  19904  coseq1  19906  efeq1  19907  tanregt0  19917  logneg2  19985  logdivlti  19987  logcnlem4  20008  dvlog2lem  20015  dvlog2  20016  advlog  20017  advlogexp  20018  logtayllem  20022  logtayl  20023  logtayl2  20025  logccv  20026  cxpval  20027  1cxp  20035  cxpcl  20037  cxpp1  20043  cxpmul2  20052  cxpsqr  20066  dvcxp1  20098  dvcxp2  20099  dvsqr  20100  resqrcn  20105  sqrcn  20106  cxpaddlelem  20107  root1id  20110  root1eq1  20111  root1cj  20112  cxpeq  20113  loglesqr  20114  angneg  20117  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  ang180lem5  20127  logrec  20133  isosctrlem1  20134  isosctrlem2  20135  isosctrlem3  20136  affineequiv  20139  affineequiv2  20140  angpieqvdlem  20141  chordthmlem2  20146  chordthmlem3  20147  chordthmlem5  20149  1cubrlem  20153  1cubr  20154  dcubic2  20156  dcubic  20158  mcubic  20159  binom4  20162  dquartlem1  20163  quart1lem  20167  quart1  20168  quartlem1  20169  quart  20173  asinlem  20180  asinlem2  20181  asinlem3a  20182  asinlem3  20183  asinf  20184  atandm2  20189  atandm4  20191  atanf  20192  asinneg  20198  efiasin  20200  sinasin  20201  asinsinlem  20203  asinsin  20204  asin1  20206  acos1  20207  reasinsin  20208  asinbnd  20211  cosasin  20216  atanneg  20219  atancj  20222  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsublem  20227  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  cosatanne0  20234  atantan  20235  atanbndlem  20237  bndatandm  20241  atans2  20243  atansopn  20244  dvatan  20247  atantayl  20249  atantayl2  20250  atantayl3  20251  leibpilem1  20252  leibpilem2  20253  leibpi  20254  log2cnv  20256  log2tlbnd  20257  log2ublem3  20260  log2ub  20261  birthdaylem2  20263  birthday  20265  efrlim  20280  dfef2  20281  cxplim  20282  divsqrsumlem  20290  cvxcl  20295  scvxcvx  20296  logdifbnd  20304  emcllem2  20306  emcllem3  20307  emcllem4  20308  emcllem5  20309  emcllem7  20311  harmonicbnd4  20320  fsumharmonic  20321  wilthlem1  20322  wilthlem2  20323  wilthlem3  20324  ftalem5  20330  basellem2  20335  basellem3  20336  basellem5  20338  basellem6  20339  basellem7  20340  basellem8  20341  basellem9  20342  isnsqf  20389  0sgm  20398  mule1  20402  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  chpp1  20409  mumullem2  20434  sqff1o  20436  musum  20447  muinv  20449  1sgmprm  20454  1sgm2ppw  20455  ppiublem2  20458  ppiub  20459  chtublem  20466  chtub  20467  logfaclbnd  20477  logfacbnd3  20478  logfacrlim  20479  logexprlim  20480  mersenne  20482  perfect1  20483  perfectlem1  20484  perfectlem2  20485  perfect  20486  dchrelbasd  20494  dchr1cl  20506  dchrmulid2  20507  dchrinvcl  20508  dchrfi  20510  dchr1  20512  dchrptlem1  20519  dchrptlem2  20520  dchrsum2  20523  sumdchr2  20525  bcmono  20532  bcp1ctr  20534  bclbnd  20535  bposlem1  20539  bposlem8  20546  bposlem9  20547  lgslem1  20551  lgslem2  20552  lgslem4  20554  lgsfcl2  20557  lgsvalmod  20570  lgsneg  20574  lgsdilem  20577  lgsdir2lem1  20578  lgsdir2lem2  20579  lgsdir2lem3  20580  lgsdir2lem4  20581  lgsdir2lem5  20582  lgsdir2  20583  lgsdir  20585  lgsdi  20587  lgsne0  20588  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem4  20607  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2lem1  20613  lgsquad2  20615  lgsquad3  20616  m1lgs  20617  2sqlem8  20627  2sqlem10  20629  2sqlem11  20630  2sqblem  20632  chtppilimlem2  20639  chtppilim  20640  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  rplogsumlem1  20649  rpvmasumlem  20652  dchrisumlem1  20654  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasum2lem  20661  dchrisum0flblem1  20673  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lem2a  20682  rpvmasum  20691  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  logdivsum  20698  vmalogdivsum2  20703  log2sumbnd  20709  selberg2lem  20715  logdivbnd  20721  pntrmax  20729  pntrsumo1  20730  pntrsumbnd2  20732  selberg34r  20736  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntlemd  20759  pntlemc  20760  pntlemg  20763  pntlemr  20767  pntlemf  20770  pntlemk  20771  pntlemo  20772  pntlem3  20774  pnt2  20778  pnt  20779  ostth2lem2  20799  ex-pr  20833  1kp2ke3k  20849  ex-fl  20850  gxsuc  20955  gxnn0add  20957  gxnn0mul  20960  ablomul  21038  mulid  21039  cnrngo  21086  vc2  21127  vc0  21141  vcm  21143  vcnegneg  21146  vcoprne  21151  nvnncan  21237  nvm1  21246  nvpi  21248  nvmtri  21253  nvge0  21256  smcnlem  21286  ipval2lem3  21294  ipval2lem6  21300  ipidsq  21302  lnoadd  21352  ip1ilem  21420  ip1i  21421  ip2i  21422  ipdirilem  21423  ipasslem1  21425  ipasslem2  21426  ipasslem10  21433  minvecolem2  21470  hvsubid  21621  hvaddsubval  21628  hv2times  21656  hvnegdii  21657  hvsubcan  21669  hvsubcan2  21670  hisubcomi  21699  normlem9  21713  normlem7tALT  21714  norm-ii-i  21732  normsubi  21736  polid2i  21752  hhssnv  21857  pjhthlem1  21986  h1de2bi  22149  homulid2  22396  honegneg  22402  ho2times  22415  lnop0  22562  lnopaddi  22567  lnophmlem2  22613  lnfn0i  22638  lnfnaddi  22639  hst1h  22823  sto2i  22833  stadd3i  22844  superpos  22950  addltmulALT  23042  bcm1n  23048  ltesubnnd  23049  ballotlem2  23063  ballotlemfp1  23066  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemodife  23072  ballotlem4  23073  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  ballotlemsgt1  23085  ballotlemsdom  23086  ballotlemsel1i  23087  ballotlemsi  23089  ballotlemsima  23090  ballotlem1ri  23109  logb1  23420  dya2ub  23590  dya2iocseg  23594  coinflippvt  23700  zetacvg  23704  subfacp1lem1  23725  subfacp1lem5  23730  subfacp1lem6  23731  subfacval2  23733  subfaclim  23734  subfacval3  23735  cvxpcon  23788  cvxscon  23789  rescon  23792  cvmliftlem7  23837  cvmliftlem10  23840  vdgr1b  23910  eupares  23914  eupap1  23915  eupath2lem3  23918  sinccvglem  24020  elfzp1b  24027  relexpadd  24050  sqdivzi  24094  4bc3eq4  24113  halfthird  24115  5recm6rec  24116  faclimlem3  24119  faclimlem5  24121  faclimlem6  24122  faclimlem8  24124  faclimlem9  24125  prodrblem  24152  fprodcvg  24153  prodmolem2a  24157  zprod  24160  prodf1  24165  prodfclim1  24167  prod1  24169  predfz  24273  brbtwn2  24604  colinearalglem4  24608  axsegconlem1  24616  ax5seglem1  24627  ax5seglem2  24628  ax5seglem3  24630  ax5seglem4  24631  ax5seglem5  24632  ax5seglem7  24634  ax5seglem9  24636  axbtwnid  24638  axpaschlem  24639  axlowdimlem6  24646  axlowdimlem13  24653  axlowdimlem14  24654  axlowdimlem16  24656  axlowdim  24660  axeuclidlem  24661  axeuclid  24662  axcontlem2  24664  axcontlem4  24666  axcontlem7  24669  axcontlem8  24670  bpoly0  24856  bpoly1  24857  bpolycl  24858  bpolysum  24859  bpolydiflem  24860  fsumkthpow  24862  bpoly2  24863  bpoly3  24864  bpoly4  24865  fsumcube  24866  ltflcei  24997  itg2addnclem2  25003  itg2addnc  25004  dvreasin  25025  dvreacos  25026  areacirclem2  25027  areacirclem5  25031  areacirc  25033  3timesi  25280  2eq3m1  25281  cntrset  25704  cnegvex2  25762  mulone  25787  vecscmonto  25788  clscnc  26112  fdc  26557  mettrifi  26575  heiborlem4  26640  heiborlem6  26642  bfp  26650  eldioph2lem1  26941  lzenom  26951  rabren3dioph  27000  irrapxlem1  27009  irrapxlem2  27010  pellexlem2  27017  pell1qrge1  27057  pell1qr1  27058  elpell1qr2  27059  pell1qrgaplem  27060  rmspecsqrnq  27093  rmspecfund  27096  rmxy0  27110  rmxm1  27121  rmym1  27122  2nn0ind  27132  jm2.24nn  27148  jm2.17a  27149  jm2.17b  27150  jm2.17c  27151  jm2.24  27152  acongeq  27172  jm2.18  27183  jm2.19lem3  27186  jm2.25  27194  jm2.16nn0  27199  jm2.27c  27202  jm3.1lem1  27212  jm3.1lem2  27213  rngunsnply  27480  flcidc  27481  psgnunilem5  27519  psgnunilem2  27520  psgnunilem4  27522  m1expaddsub  27523  psgnuni  27524  cnmsgnsubg  27536  cnmsgnbas  27537  cnmsgngrp  27538  proot1ex  27622  ofdivrec  27645  lhe4.4ex1a  27648  expgrowthi  27652  expgrowth  27654  refsum2cnlem1  27810  fmul01lt1lem2  27817  m1expeven  27827  clim1fr1  27829  isumneg  27830  climneg  27838  itgsin0pilem1  27846  itgsinexp  27851  stoweidlem1  27852  stoweidlem7  27858  stoweidlem10  27861  stoweidlem11  27862  stoweidlem13  27864  stoweidlem14  27865  stoweidlem16  27867  stoweidlem17  27868  stoweidlem26  27877  stoweidlem34  27885  stoweidlem37  27888  stoweidlem38  27889  stoweidlem41  27892  stoweidlem42  27893  stoweidlem45  27896  stoweidlem51  27902  wallispilem2  27917  wallispilem3  27918  wallispilem4  27919  wallispilem5  27920  wallispi  27921  wallispi2lem1  27922  wallispi2lem2  27923  wallispi2  27924  stirlinglem1  27925  stirlinglem3  27927  stirlinglem4  27928  stirlinglem5  27929  stirlinglem6  27930  stirlinglem7  27931  stirlinglem8  27932  stirlinglem10  27934  stirlinglem11  27935  stirlinglem12  27936  stirlinglem13  27937  stirlinglem15  27939  sigaradd  27958  fzo0to3tp  28209  fzo0to42pr  28210  usgraexvlem  28260  wlkdvspthlem  28364  fargshiftf1  28381  fargshiftfo  28382  eupatrl  28384  sec0  28483  onetansqsecsq  28484  cotsqcscsq  28485  5m4e1  28515
  Copyright terms: Public domain W3C validator