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

Axiom ax-1cn 8882
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 8858. (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 8825 . 2  class  1
2 cc 8822 . 2  class  CC
31, 2wcel 1710 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  8918  1ex  8920  mulid1  8922  mulid2  8923  1re  8924  muladd11  9069  1p1times  9070  peano2cn  9071  mul02lem2  9076  addid1  9079  cnegex2  9081  addcom  9085  addcomd  9101  0reALT  9230  ine0  9302  mulm1  9308  0lt1  9383  ixi  9484  muleqadd  9499  reccl  9518  recne0  9524  recid  9525  recid2  9526  div1  9540  diveq1  9541  recrec  9544  rec11  9545  rec11r  9546  recdiv  9553  divdiv1  9558  divdiv2  9559  recdiv2  9560  conjmul  9564  rereccl  9565  eqneg  9567  div2neg  9570  subrec  9676  reclt1  9738  recgt1  9739  recp1lt1  9741  recreclt  9742  recgt0ii  9749  inelr  9823  ofnegsub  9831  peano5nni  9836  nn1m1nn  9853  nn1suc  9854  nnaddcl  9855  nnmulcl  9856  nnsub  9871  neg1cn  9900  1m1e0  9901  0p1e1  9926  2m1e1  9928  3m1e2  9929  3m1e2OLD  9930  2p2e4  9931  2times  9932  3p2e5  9944  3p3e6  9945  4p2e6  9946  4p3e7  9947  4p4e8  9948  5p2e7  9949  5p3e8  9950  5p4e9  9951  5p5e10  9952  6p2e8  9953  6p3e9  9954  6p4e10  9955  7p2e9  9956  7p3e10  9957  8p2e10  9958  1t1e1  9959  3t3e9  9962  halflt1  10022  1mhlfehlf  10023  8th4div3  10024  halfpm6th  10025  addltmul  10036  elnn0nn  10095  elnnnn0  10096  elz2  10129  zlem1lt  10158  zltlem1  10159  nnaddm1cl  10162  zextlt  10175  zneo  10183  nneo  10184  zeo  10186  peano5uzi  10189  uzindOLD  10195  numsuc  10225  numltc  10233  numsucc  10239  numaddc  10248  6p5lem  10262  4t3lem  10284  7t4e28  10297  decbin2  10317  uzp1  10350  peano2uzr  10363  uzaddcl  10364  rebtwnz  10404  rpnnen1lem5  10435  qbtwnre  10615  lincmb01cmp  10866  iccf1o  10867  xov1plusxeqvd  10869  fz01en  10907  fztp  10930  fzsuc2  10931  fztpval  10934  fseq1m1p1  10947  fzm1  10951  fzoss2  10986  fzval3  11000  fladdz  11039  ceim1l  11046  fldiv  11053  modnegd  11093  uzrdgxfr  11118  fzen2  11120  nn0ennn  11130  seqm1  11152  seqshft2  11161  monoord2  11166  sermono  11167  seqf1olem1  11174  seqf1olem2  11175  seqz  11183  ser1const  11191  expneg  11201  expcl  11211  m1expcl2  11215  expclzlem  11217  expm1t  11220  1exp  11221  mulexpz  11232  expadd  11234  expaddz  11236  expmul  11237  expubnd  11252  sqrecii  11276  irec  11292  i4  11295  binom21  11309  binom3  11312  sq01  11313  zesq  11314  crreczi  11316  bernneq  11317  bernneq2  11318  nn0opthlem1  11373  facnn2  11387  facndiv  11391  faclbnd4lem1  11396  faclbnd6  11402  bcnp1n  11416  bcm1k  11417  bcp1n  11418  bcp1nk  11419  bcn2  11421  bcp1m1  11422  bcpasc  11423  hashgadd  11449  hashfz  11471  hashfzo  11473  hashxplem  11475  hashbclem  11480  hashf1lem2  11484  hashf1  11485  fz1isolem  11489  seqcoll  11491  swrds1  11563  wrdeqcats1  11564  wrdind  11567  revccat  11574  swrds2  11650  rei  11731  imi  11732  resqrex  11826  absi  11861  absexpz  11880  recan  11910  reccn2  12160  iserex  12220  isercolllem1  12228  isercoll2  12232  serf0  12244  iseraltlem2  12246  iseraltlem3  12247  iseralt  12248  sumrblem  12275  fsumm1  12307  fsump1  12310  fsumtscopo  12351  fsumparts  12355  hashiun  12371  binomlem  12378  binom  12379  binom1p  12380  binom11  12381  binom1dif  12382  bcxmas  12385  incexc  12387  incexc2  12388  isumsplit  12390  isum1p  12391  climcndslem1  12399  supcvg  12405  harmonic  12408  arisum  12409  arisum2  12410  trireciplem  12411  geoserg  12415  geolim  12417  geolim2  12418  georeclim  12419  geo2sum  12420  geo2sum2  12421  geoisum1c  12427  0.999...  12428  geoihalfsum  12429  cvgrat  12430  mertenslem1  12431  mertenslem2  12432  mertens  12433  ef0lem  12451  esum  12453  ege2le3  12462  efsub  12471  efexp  12472  efzval  12473  eftlub  12480  effsumlt  12482  eft0val  12483  ef4p  12484  tanval3  12505  efi4p  12508  tan0  12522  efival  12523  sinhval  12525  coshval  12526  tanaddlem  12537  tanadd  12538  cos2t  12549  cos2tsin  12550  ef01bndlem  12555  cos01bnd  12557  cos1bnd  12558  cos2bnd  12559  demoivreALT  12572  eirrlem  12573  rpnnen2lem3  12586  rpnnen2lem11  12594  ruclem12  12610  odd2np1lem  12677  odd2np1  12678  oddm1even  12679  oddp1even  12680  oexpneg  12681  3dvds  12682  bitsp1o  12715  bitsfzo  12717  bitsf1  12728  sadcp1  12737  gcdmultiple  12820  sqgcd  12828  nn0seqcvgd  12831  prmind2  12860  3prm  12866  qredeu  12877  hashdvds  12934  phiprmpw  12935  phiprm  12936  eulerthlem2  12941  prmdiv  12944  prmdiveq  12945  opoe  12955  omoe  12956  opeo  12957  omeo  12958  iserodd  12979  pcexp  13003  pc2dvds  13022  sumhash  13035  fldivp1  13036  prmpwdvds  13042  pockthlem  13043  pockthi  13045  prmreclem2  13055  prmreclem4  13057  prmreclem6  13059  4sqlem11  13093  4sqlem12  13094  4sqlem19  13101  vdwapun  13112  vdwapid1  13113  vdwlem3  13121  vdwlem5  13123  vdwlem6  13124  vdwlem8  13126  vdwlem9  13127  vdwnnlem2  13134  ramub1lem1  13164  ramub1lem2  13165  ramcl  13167  dec5nprm  13172  decexp2  13181  2exp16  13194  prmlem0  13198  prmlem1a  13199  23prm  13211  prmlem2  13212  43prm  13214  83prm  13215  139prm  13216  163prm  13217  317prm  13218  631prm  13219  1259lem1  13220  1259lem2  13221  1259lem3  13222  1259lem4  13223  1259lem5  13224  1259prm  13225  2503lem1  13226  2503lem2  13227  2503lem3  13228  2503prm  13229  4001lem1  13230  4001lem2  13231  4001lem3  13232  4001lem4  13233  4001prm  13234  gsumccat  14557  mulgnndir  14682  mulgneg2  14687  mulgnnass  14688  sylow1lem1  15002  sylow2a  15023  efgsval2  15135  efgsrel  15136  efgsres  15140  efgredlemc  15147  odadd2  15234  cncrng  16495  cnfld1  16499  cnfldmulg  16506  zsssubrg  16530  gzrngunit  16537  zrngunit  16538  zcyg  16545  prmirredlem  16546  mulgrhm2  16561  nminvr  18276  blcvx  18400  expcn  18473  iirevcn  18526  iihalf2  18529  icchmeo  18537  icopnfcnv  18538  icopnfhmeo  18539  iccpnfhmeo  18541  xrhmeo  18542  icccvx  18546  evth  18555  lebnumii  18562  htpycom  18572  htpycc  18576  reparphti  18593  pco1  18611  pcohtpylem  18615  pcopt  18618  pcoass  18620  pcorevcl  18621  pcorevlem  18622  pcorev2  18624  pi1xfrcnv  18653  pjthlem1  18899  ovolunlem1a  18953  ovolunlem1  18954  ovolicc2lem4  18977  uniioombllem3  19038  uniioombllem4  19039  dyadovol  19046  opnmbllem  19054  vitalilem4  19064  vitalilem5  19065  vitali  19066  mbfi1fseqlem6  19173  iblitg  19221  iblcnlem1  19240  itgcnlem  19242  bddibl  19292  dvid  19365  dvnadd  19376  dvexp  19400  dvexp2  19401  dvmptid  19404  dvcnvlem  19421  dvexp3  19423  dveflem  19424  dvef  19425  dvsincos  19426  dvlipcn  19439  dvivthlem1  19453  lhop2  19460  dvcvx  19465  dvfsumle  19466  dvfsumabs  19468  dvfsumlem1  19471  dvfsumlem2  19472  degltp1le  19557  ply1divex  19620  fta1glem1  19649  plyaddlem1  19693  plymullem1  19694  coeidp  19742  dgrid  19743  dgrsub  19751  dgrcolem1  19752  dgrcolem2  19753  dvply1  19762  dvply2g  19763  plydivlem1  19771  plyremlem  19782  fta1lem  19785  vieta1lem1  19788  vieta1lem2  19789  qaa  19801  iaa  19803  aalioulem3  19812  geolim3  19817  aaliou3lem2  19821  aaliou3lem3  19822  aaliou3lem8  19823  aaliou3lem7  19827  taylply2  19845  dvtaylp  19847  dvntaylp  19848  taylthlem1  19850  taylthlem2  19851  dvradcnv  19898  pserdvlem2  19905  pserdv2  19907  abelthlem1  19908  abelthlem2  19909  abelthlem6  19913  abelthlem7  19915  abelth  19918  reeff1olem  19923  reeff1o  19924  efcvx  19926  sinhalfpilem  19935  eulerid  19943  cos2pi  19945  ef2pi  19946  sincosq3sgn  19969  sincosq4sgn  19970  coseq00topi  19971  tangtx  19974  sincos4thpi  19982  sincos6thpi  19984  pige3  19986  abssinper  19987  coskpi  19989  coseq1  19991  efeq1  19992  tanregt0  20002  logneg2  20071  logdivlti  20076  logcnlem4  20097  dvlog2lem  20104  dvlog2  20105  advlog  20106  advlogexp  20107  logtayllem  20111  logtayl  20112  logtayl2  20114  logccv  20115  cxpval  20116  1cxp  20124  cxpcl  20126  cxpp1  20132  cxpmul2  20141  cxpsqr  20155  dvcxp1  20187  dvcxp2  20188  dvsqr  20189  resqrcn  20194  sqrcn  20195  cxpaddlelem  20196  root1id  20199  root1eq1  20200  root1cj  20201  cxpeq  20202  loglesqr  20203  angneg  20206  ang180lem1  20212  ang180lem2  20213  ang180lem3  20214  ang180lem4  20215  ang180lem5  20216  logrec  20222  isosctrlem1  20223  isosctrlem2  20224  isosctrlem3  20225  affineequiv  20228  affineequiv2  20229  angpieqvdlem  20230  chordthmlem2  20235  chordthmlem3  20236  chordthmlem5  20238  1cubrlem  20242  1cubr  20243  dcubic2  20245  dcubic  20247  mcubic  20248  binom4  20251  dquartlem1  20252  quart1lem  20256  quart1  20257  quartlem1  20258  quart  20262  asinlem  20269  asinlem2  20270  asinlem3a  20271  asinlem3  20272  asinf  20273  atandm2  20278  atandm4  20280  atanf  20281  asinneg  20287  efiasin  20289  sinasin  20290  asinsinlem  20292  asinsin  20293  asin1  20295  acos1  20296  reasinsin  20297  asinbnd  20300  cosasin  20305  atanneg  20308  atancj  20311  efiatan  20313  atanlogaddlem  20314  atanlogadd  20315  atanlogsublem  20316  atanlogsub  20317  efiatan2  20318  2efiatan  20319  tanatan  20320  cosatan  20322  cosatanne0  20323  atantan  20324  atanbndlem  20326  bndatandm  20330  atans2  20332  atansopn  20333  dvatan  20336  atantayl  20338  atantayl2  20339  atantayl3  20340  leibpilem1  20341  leibpilem2  20342  leibpi  20343  log2cnv  20345  log2tlbnd  20346  log2ublem3  20349  log2ub  20350  birthdaylem2  20352  birthday  20354  efrlim  20369  dfef2  20370  cxplim  20371  divsqrsumlem  20379  cvxcl  20384  scvxcvx  20385  logdifbnd  20393  emcllem2  20396  emcllem3  20397  emcllem4  20398  emcllem5  20399  emcllem7  20401  harmonicbnd4  20410  fsumharmonic  20411  wilthlem1  20412  wilthlem2  20413  wilthlem3  20414  ftalem5  20420  basellem2  20425  basellem3  20426  basellem5  20428  basellem6  20429  basellem7  20430  basellem8  20431  basellem9  20432  isnsqf  20479  0sgm  20488  mule1  20492  ppiprm  20495  ppinprm  20496  chtprm  20497  chtnprm  20498  chpp1  20499  mumullem2  20524  sqff1o  20526  musum  20537  muinv  20539  1sgmprm  20544  1sgm2ppw  20545  ppiublem2  20548  ppiub  20549  chtublem  20556  chtub  20557  logfaclbnd  20567  logfacbnd3  20568  logfacrlim  20569  logexprlim  20570  mersenne  20572  perfect1  20573  perfectlem1  20574  perfectlem2  20575  perfect  20576  dchrelbasd  20584  dchr1cl  20596  dchrmulid2  20597  dchrinvcl  20598  dchrfi  20600  dchr1  20602  dchrptlem1  20609  dchrptlem2  20610  dchrsum2  20613  sumdchr2  20615  bcmono  20622  bcp1ctr  20624  bclbnd  20625  bposlem1  20629  bposlem8  20636  bposlem9  20637  lgslem1  20641  lgslem2  20642  lgslem4  20644  lgsfcl2  20647  lgsvalmod  20660  lgsneg  20664  lgsdilem  20667  lgsdir2lem1  20668  lgsdir2lem2  20669  lgsdir2lem3  20670  lgsdir2lem4  20671  lgsdir2lem5  20672  lgsdir2  20673  lgsdir  20675  lgsdi  20677  lgsne0  20678  lgseisenlem1  20694  lgseisenlem2  20695  lgseisenlem4  20697  lgseisen  20698  lgsquadlem1  20699  lgsquadlem2  20700  lgsquad2lem1  20703  lgsquad2  20705  lgsquad3  20706  m1lgs  20707  2sqlem8  20717  2sqlem10  20719  2sqlem11  20720  2sqblem  20722  chtppilimlem2  20729  chtppilim  20730  chebbnd2  20732  chto1lb  20733  chpchtlim  20734  rplogsumlem1  20739  rpvmasumlem  20742  dchrisumlem1  20744  dchrmusumlema  20748  dchrmusum2  20749  dchrvmasum2lem  20751  dchrisum0flblem1  20763  rpvmasum2  20767  dchrisum0re  20768  dchrisum0lem2a  20772  rpvmasum  20781  mudivsum  20785  mulogsumlem  20786  mulogsum  20787  logdivsum  20788  vmalogdivsum2  20793  log2sumbnd  20799  selberg2lem  20805  logdivbnd  20811  pntrmax  20819  pntrsumo1  20820  pntrsumbnd2  20822  selberg34r  20826  pntrlog2bndlem2  20833  pntrlog2bndlem4  20835  pntrlog2bndlem5  20836  pntrlog2bndlem6  20838  pntpbnd1a  20840  pntpbnd2  20842  pntibndlem2  20846  pntlemd  20849  pntlemc  20850  pntlemg  20853  pntlemr  20857  pntlemf  20860  pntlemk  20861  pntlemo  20862  pntlem3  20864  pnt2  20868  pnt  20869  ostth2lem2  20889  ex-pr  20923  1kp2ke3k  20939  ex-fl  20940  gxsuc  21045  gxnn0add  21047  gxnn0mul  21050  ablomul  21128  mulid  21129  cnrngo  21176  vc2  21219  vc0  21233  vcm  21235  vcnegneg  21238  vcoprne  21243  nvnncan  21329  nvm1  21338  nvpi  21340  nvmtri  21345  nvge0  21348  smcnlem  21378  ipval2lem3  21386  ipval2lem6  21392  ipidsq  21394  lnoadd  21444  ip1ilem  21512  ip1i  21513  ip2i  21514  ipdirilem  21515  ipasslem1  21517  ipasslem2  21518  ipasslem10  21525  minvecolem2  21562  hvsubid  21713  hvaddsubval  21720  hv2times  21748  hvnegdii  21749  hvsubcan  21761  hvsubcan2  21762  hisubcomi  21791  normlem9  21805  normlem7tALT  21806  norm-ii-i  21824  normsubi  21828  polid2i  21844  hhssnv  21949  pjhthlem1  22078  h1de2bi  22241  homulid2  22488  honegneg  22494  ho2times  22507  lnop0  22654  lnopaddi  22659  lnophmlem2  22705  lnfn0i  22730  lnfnaddi  22731  hst1h  22915  sto2i  22925  stadd3i  22936  superpos  23042  addltmulALT  23134  bcm1n  23350  ltesubnnd  23366  qqhval2lem  23638  qqh1  23642  logb1  23669  dya2ub  23884  dya2icoseg  23891  coinflippvt  23991  ballotlem2  23995  ballotlemfp1  23998  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemodife  24004  ballotlem4  24005  ballotlemi1  24009  ballotlemii  24010  ballotlemic  24013  ballotlem1c  24014  ballotlemsgt1  24017  ballotlemsdom  24018  ballotlemsel1i  24019  ballotlemsi  24021  ballotlemsima  24022  ballotlem1ri  24041  zetacvg  24048  lgamgulmlem2  24063  lgamgulmlem3  24064  lgamgulmlem4  24065  lgamgulmlem5  24066  lgamgulmlem6  24067  lgamgulm2  24069  lgamcvg2  24088  gamcvg  24089  gamcvg2lem  24092  lgam1  24097  gam1  24098  facgam  24099  gamfac  24100  subfacp1lem1  24114  subfacp1lem5  24119  subfacp1lem6  24120  subfacval2  24122  subfaclim  24123  subfacval3  24124  cvxpcon  24177  cvxscon  24178  rescon  24181  cvmliftlem7  24226  cvmliftlem10  24229  vdgr1b  24299  eupares  24303  eupap1  24304  eupath2lem3  24307  sinccvglem  24409  elfzp1b  24416  relexpadd  24439  sqdivzi  24485  4bc3eq4  24504  halfthird  24506  5recm6rec  24507  divcnvlin  24513  muls1d  24514  prodf1  24520  prodfclim1  24522  prodfrec  24524  ntrivcvg  24526  ntrivcvgtail  24529  prodrblem  24556  fprodcvg  24557  prodmolem2a  24561  zprod  24564  fprodntriv  24569  prod1  24571  prodss  24574  fprodss  24575  fprodser  24576  fprodcl  24579  fproddiv  24586  fprodsplit  24590  fprodm1  24591  fprodp1  24593  risefacval2  24617  fallfacval2  24618  risefaccl  24621  fallfaccl  24622  risefacp1  24634  fallfacp1  24635  risefac1  24636  fallfac1  24637  risefacfac  24638  fallfacfac  24639  gamma1  24645  gammadenomn0  24648  peano2dmgamma  24649  rpdmgamma  24650  gammacvglem1  24651  gammacvglem2  24652  faclimlem1  24654  faclimlem2  24655  faclimlem3  24656  faclim  24657  iprodfac  24658  faclim2  24659  predfz  24761  brbtwn2  25092  colinearalglem4  25096  axsegconlem1  25104  ax5seglem1  25115  ax5seglem2  25116  ax5seglem3  25118  ax5seglem4  25119  ax5seglem5  25120  ax5seglem7  25122  ax5seglem9  25124  axbtwnid  25126  axpaschlem  25127  axlowdimlem6  25134  axlowdimlem13  25141  axlowdimlem14  25142  axlowdimlem16  25144  axlowdim  25148  axeuclidlem  25149  axeuclid  25150  axcontlem2  25152  axcontlem4  25154  axcontlem7  25157  axcontlem8  25158  bpoly0  25344  bpoly1  25345  bpolycl  25346  bpolysum  25347  bpolydiflem  25348  fsumkthpow  25350  bpoly2  25351  bpoly3  25352  bpoly4  25353  fsumcube  25354  ltflcei  25485  itg2addnclem2  25493  itg2addnc  25494  dvreasin  25515  dvreacos  25516  areacirclem2  25517  areacirclem5  25521  areacirc  25523  fdc  25779  mettrifi  25797  heiborlem4  25861  heiborlem6  25863  bfp  25871  eldioph2lem1  26162  lzenom  26172  rabren3dioph  26221  irrapxlem1  26230  irrapxlem2  26231  pellexlem2  26238  pell1qrge1  26278  pell1qr1  26279  elpell1qr2  26280  pell1qrgaplem  26281  rmspecsqrnq  26314  rmspecfund  26317  rmxy0  26331  rmxm1  26342  rmym1  26343  2nn0ind  26353  jm2.24nn  26369  jm2.17a  26370  jm2.17b  26371  jm2.17c  26372  jm2.24  26373  acongeq  26393  jm2.18  26404  jm2.19lem3  26407  jm2.25  26415  jm2.16nn0  26420  jm2.27c  26423  jm3.1lem1  26433  jm3.1lem2  26434  rngunsnply  26701  flcidc  26702  psgnunilem5  26740  psgnunilem2  26741  psgnunilem4  26743  m1expaddsub  26744  psgnuni  26745  cnmsgnsubg  26757  cnmsgnbas  26758  cnmsgngrp  26759  proot1ex  26843  ofdivrec  26866  lhe4.4ex1a  26869  expgrowthi  26873  expgrowth  26875  refsum2cnlem1  27031  fmul01lt1lem2  27038  m1expeven  27048  clim1fr1  27050  isumneg  27051  climneg  27059  itgsin0pilem1  27067  itgsinexp  27072  stoweidlem1  27073  stoweidlem7  27079  stoweidlem10  27082  stoweidlem11  27083  stoweidlem13  27085  stoweidlem14  27086  stoweidlem16  27088  stoweidlem17  27089  stoweidlem26  27098  stoweidlem34  27106  stoweidlem37  27109  stoweidlem38  27110  stoweidlem41  27113  stoweidlem42  27114  stoweidlem45  27117  stoweidlem51  27123  wallispilem2  27138  wallispilem3  27139  wallispilem4  27140  wallispilem5  27141  wallispi  27142  wallispi2lem1  27143  wallispi2lem2  27144  wallispi2  27145  stirlinglem1  27146  stirlinglem3  27148  stirlinglem4  27149  stirlinglem5  27150  stirlinglem6  27151  stirlinglem7  27152  stirlinglem8  27153  stirlinglem10  27155  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  stirlinglem15  27160  sigaradd  27179  nn0n0n1ge2  27449  fzo0to3tp  27455  fzo0to42pr  27456  bcn2m1  27462  brfi1indlem  27488  usgraexvlem  27560  cusgrasizeinds  27631  cusgrasize2inds  27632  wlkdvspthlem  27726  fargshiftf1  27743  fargshiftfo  27744  eupatrl  27746  vdgre1b  27794  sec0  27913  onetansqsecsq  27914  cotsqcscsq  27915  5m4e1  27945
  Copyright terms: Public domain W3C validator