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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9275 . 2
2 cc 9272 . 2
31, 2wcel 1756 1
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9370  1ex  9373  mulid1  9375  mulid2  9376  1re  9377  1cnd  9394  muladd11  9531  1p1times  9532  peano2cn  9533  mul02lem2  9538  addid1  9541  cnegex2  9543  addcom  9547  addcomd  9563  0reALT  9697  pncan1  9764  npcan1  9765  ine0  9772  mulm1  9778  0lt1  9854  ixi  9957  muleqadd  9972  reccl  9993  recne0  9999  recid  10000  recid2  10001  div1  10015  1div1e1  10016  diveq1  10017  recrec  10020  rec11  10021  rec11r  10022  recdiv  10029  divdiv1  10034  divdiv2  10035  recdiv2  10036  conjmul  10040  rereccl  10041  eqneg  10043  div2neg  10046  subrec  10152  recp1lt1  10222  recreclt  10223  recgt0ii  10230  inelr  10304  ofnegsub  10312  peano5nni  10317  nn1m1nn  10334  nn1suc  10335  nnaddcl  10336  nnmulcl  10337  nnsub  10352  1m1e0  10382  neg1cn  10417  neg1ne0  10419  negneg1e1  10421  1pneg1e0  10422  1m0e1  10424  0p1e1  10425  1p0e1  10426  2m1e1  10428  3m1e2  10430  2p2e4  10431  2times  10432  1p2e3  10438  3p2e5  10446  3p3e6  10447  4p2e6  10448  4p3e7  10449  4p4e8  10450  5p2e7  10451  5p3e8  10452  5p4e9  10453  5p5e10  10454  6p2e8  10455  6p3e9  10456  6p4e10  10457  7p2e9  10458  7p3e10  10459  8p2e10  10460  1t1e1  10461  3t3e9  10466  neg1mulneg1e1  10531  1mhlfehlf  10536  8th4div3  10537  halfpm6th  10538  addltmul  10552  sub1m1  10566  elnn0nn  10614  elnnnn0  10615  nn0n0n1ge2  10635  elz2  10655  zlem1lt  10688  zltlem1  10689  nnaddm1cl  10693  zextlt  10708  zneo  10716  nneo  10717  zeo  10719  peano5uzi  10722  uzindOLD  10728  numsuc  10759  numltc  10767  numsucc  10773  numaddc  10782  6p5lem  10796  4t3lem  10818  7t4e28  10831  decbin2  10851  uzp1  10886  peano2uzr  10902  uzaddcl  10903  rebtwnz  10944  qbtwnre  11161  lincmb01cmp  11420  iccf1o  11421  xov1plusxeqvd  11423  fz01en  11469  fztp  11504  fzsuc2  11506  fztpval  11510  fseq1m1p1  11527  elfzp1b  11529  fzm1  11532  fzoss2  11569  fzval3  11597  fzosplitsnm1  11600  fzo0to42pr  11608  ubmelm1fzo  11615  fzoshftral  11628  fladdz  11662  ltdifltdiv  11670  dfceil2  11672  ceim1l  11678  fldiv  11691  modvalp1  11718  modnegd  11746  uzrdgxfr  11781  fzen2  11783  nn0ennn  11793  seqm1  11815  seqshft2  11824  monoord2  11829  sermono  11830  seqf1olem1  11837  seqf1olem2  11838  seqz  11846  ser1const  11854  expcl  11875  m1expcl2  11879  expclzlem  11881  expm1t  11884  1exp  11885  mulexpz  11896  expadd  11898  expaddz  11900  expmul  11901  expubnd  11916  sqrecii  11940  neg1sqe1  11953  irec  11957  i4  11960  binom21  11974  binom3  11977  sq01  11978  zesq  11979  crreczi  11981  bernneq  11982  bernneq2  11983  nn0opthlem1  12038  facnn2  12052  facndiv  12056  faclbnd4lem1  12061  faclbnd6  12067  bcnp1n  12082  bcm1k  12083  bcp1n  12084  bcp1nk  12085  bcn2  12087  bcp1m1  12088  bcpasc  12089  bcn2m1  12092  hashgadd  12132  hashfz  12180  hashfzo  12182  hashxplem  12187  hashbclem  12197  hashf1lem2  12201  hashf1  12202  seqcoll  12208  brfi1indlem  12210  lswccatn0lsw  12279  wrdlenccats1lenm1  12297  swrds1  12337  swrdlsw  12338  swrdccatwrd  12354  wrdeqcats1  12360  wrdind  12363  wrd2ind  12364  revccat  12398  repswrevw  12416  cshwidxm1  12435  cshwidxn  12437  cshweqrep  12447  swrds2  12537  swrd2lsw  12544  rei  12637  imi  12638  absexpz  12786  recan  12816  reccn2  13066  iserex  13126  isercolllem1  13134  isercoll2  13138  serf0  13150  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  sumrblem  13180  fsumm1  13212  fsump1  13215  fsumtscopo  13257  fsumparts  13261  hashiun  13277  binomlem  13284  binom  13285  binom1p  13286  binom11  13287  binom1dif  13288  bcxmas  13290  isumsplit  13295  isum1p  13296  climcndslem1  13304  supcvg  13310  harmonic  13313  arisum  13314  arisum2  13315  trireciplem  13316  geoserg  13320  geolim  13322  geolim2  13323  georeclim  13324  geo2sum  13325  geo2sum2  13326  geoisum1c  13332  0.999...  13333  geoihalfsum  13334  cvgrat  13335  mertenslem1  13336  mertenslem2  13337  mertens  13338  esum  13358  ege2le3  13367  efsub  13376  efexp  13377  efzval  13378  eftlub  13385  effsumlt  13387  ef4p  13389  tanval3  13410  efi4p  13413  tan0  13427  efival  13428  tanadd  13443  cos2t  13454  cos2tsin  13455  ef01bndlem  13460  cos1bnd  13463  cos2bnd  13464  demoivreALT  13477  eirrlem  13478  rpnnen2lem3  13491  rpnnen2lem11  13499  ruclem12  13515  odd2np1lem  13583  odd2np1  13584  oddm1even  13585  oddp1even  13586  oexpneg  13587  3dvds  13588  bitsp1o  13621  bitsfzo  13623  sadcp1  13643  gcdmultiple  13726  sqgcd  13734  nn0seqcvgd  13737  prmind2  13766  qredeu  13785  hashdvds  13842  phiprmpw  13843  phiprm  13844  eulerthlem2  13849  prmdiv  13852  prmdiveq  13853  opoe  13870  omoe  13871  opeo  13872  omeo  13873  iserodd  13894  pcexp  13918  pc2dvds  13937  sumhash  13950  fldivp1  13951  prmpwdvds  13957  pockthlem  13958  pockthi  13960  prmreclem2  13970  prmreclem4  13972  prmreclem6  13974  4sqlem11  14008  4sqlem12  14009  4sqlem19  14016  vdwapun  14027  vdwapid1  14028  vdwlem3  14036  vdwlem5  14038  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  vdwnnlem2  14049  ramub1lem1  14079  ramub1lem2  14080  ramcl  14082  dec5nprm  14087  decexp2  14096  2exp16  14109  prmlem0  14125  43prm  14141  83prm  14142  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  gsumccat  15510  mulgnndir  15640  mulgneg2  15645  psgnunilem5  15991  psgnunilem2  15992  m1expaddsub  15995  sylow1lem1  16088  sylow2a  16109  efgsval2  16221  efgsrel  16222  efgsres  16226  efgredlemc  16233  cncrng  17817  cnfld1  17821  zsssubrg  17851  gzrngunit  17858  zringcyg  17887  zcyg  17892  zrngunit  17895  prmirredlemOLD  17900  mulgrhm2  17907  mulgrhm2OLD  17910  cnmsgnsubg  17987  cnmsgnbas  17988  cnmsgngrp  17989  psgninv  17992  zrhpsgnodpm  18002  evpmodpmf1o  18006  nminvr  20230  blcvx  20355  iihalf2  20485  icopnfcnv  20494  icopnfhmeo  20495  iccpnfhmeo  20497  xrhmeo  20498  icccvx  20502  lebnumii  20518  reparphti  20549  pcoass  20576  pcorevlem  20578  pcorev2  20580  pi1xfrcnv  20609  pjthlem1  20904  ovolunlem1a  20959  ovolunlem1  20960  ovolicc2lem4  20983  uniioombllem3  21045  uniioombllem4  21046  dyadovol  21053  vitalilem4  21071  iblitg  21226  iblcnlem1  21245  itgcnlem  21247  dvid  21372  dvexp  21407  dvexp2  21408  dvmptid  21411  dvexp3  21430  dveflem  21431  dvef  21432  dvlipcn  21446  dvcvx  21472  dvfsumle  21473  dvfsumlem1  21478  degltp1le  21524  ply1divex  21588  fta1glem1  21617  plyaddlem1  21661  plymullem1  21662  coeidp  21710  dgrid  21711  dvply1  21730  dvply2g  21731  plyremlem  21750  fta1lem  21753  vieta1lem1  21756  vieta1lem2  21757  qaa  21769  iaa  21771  aalioulem3  21780  geolim3  21785  aaliou3lem2  21789  aaliou3lem8  21791  aaliou3lem7  21795  taylply2  21813  dvradcnv  21866  pserdvlem2  21873  pserdv2  21875  abelthlem1  21876  abelthlem2  21877  abelthlem6  21881  abelthlem7  21883  abelth  21886  reeff1olem  21891  reeff1o  21892  efcvx  21894  sinhalfpilem  21905  eulerid  21916  cos2pi  21918  sincosq3sgn  21942  sincosq4sgn  21943  tangtx  21947  sincos4thpi  21955  sincos6thpi  21957  pige3  21959  abssinper  21960  coskpi  21962  coseq1  21964  efeq1  21965  tanregt0  21975  logneg2  22044  logdivlti  22049  logcnlem4  22070  dvlog2lem  22077  dvlog2  22078  advlog  22079  advlogexp  22080  logtayl  22085  logtayl2  22087  logccv  22088  cxpval  22089  1cxp  22097  cxpcl  22099  cxpp1  22105  cxpsqr  22128  dvsqr  22162  sqrcn  22168  cxpaddlelem  22169  root1id  22172  root1cj  22174  loglesqr  22176  ang180lem1  22185  ang180lem2  22186  ang180lem3  22187  logrec  22195  isosctrlem1  22196  isosctrlem2  22197  affineequiv  22201  affineequiv2  22202  angpieqvdlem  22203  1cubrlem  22216  1cubr  22217  dcubic2  22219  dcubic  22221  mcubic  22222  binom4  22225  dquartlem1  22226  quart1lem  22230  quart1  22231  quartlem1  22232  asinlem  22243  asinlem2  22244  asinlem3a  22245  asinlem3  22246  asinf  22247  atandm2  22252  atandm4  22254  atanf  22255  asinneg  22261  efiasin  22263  sinasin  22264  asinsin  22267  asin1  22269  acos1  22270  reasinsin  22271  asinbnd  22274  cosasin  22279  atanneg  22282  atancj  22285  efiatan  22287  atanlogaddlem  22288  atanlogadd  22289  atanlogsublem  22290  atanlogsub  22291  efiatan2  22292  2efiatan  22293  tanatan  22294  cosatan  22296  cosatanne0  22297  atantan  22298  atanbndlem  22300  bndatandm  22304  atans2  22306  dvatan  22310  atantayl  22312  atantayl2  22313  atantayl3  22314  leibpilem1  22315  leibpilem2  22316  leibpi  22317  log2cnv  22319  log2tlbnd  22320  log2ublem3  22323  log2ub  22324  birthdaylem2  22326  birthday  22328  efrlim  22343  dfef2  22344  cvxcl  22358  scvxcvx  22359  emcllem2  22370  emcllem4  22372  emcllem7  22375  harmonicbnd4  22384  fsumharmonic  22385  wilthlem1  22386  wilthlem2  22387  wilthlem3  22388  basellem2  22399  basellem5  22402  basellem6  22403  basellem7  22404  basellem8  22405  basellem9  22406  0sgm  22462  mule1  22466  ppiprm  22469  ppinprm  22470  chtprm  22471  chtnprm  22472  chpp1  22473  mumullem2  22498  sqff1o  22500  1sgmprm  22518  1sgm2ppw  22519  ppiublem2  22522  ppiub  22523  chtublem  22530  chtub  22531  logfaclbnd  22541  logfacbnd3  22542  logfacrlim  22543  logexprlim  22544  mersenne  22546  perfect1  22547  perfectlem1  22548  perfectlem2  22549  perfect  22550  dchrelbasd  22558  dchr1cl  22570  dchrmulid2  22571  dchrinvcl  22572  dchrfi  22574  dchr1  22576  dchrsum2  22587  sumdchr2  22589  bcmono  22596  bcp1ctr  22598  bclbnd  22599  bposlem8  22610  lgslem1  22615  lgslem2  22616  lgsfcl2  22621  lgsvalmod  22634  lgsneg  22638  lgsdilem  22641  lgsdir2lem1  22642  lgsdir2lem2  22643  lgsdir2lem3  22644  lgsdir2lem5  22646  lgsdir2  22647  lgsdir  22649  lgsdi  22651  lgsne0  22652  lgseisenlem1  22668  lgseisenlem2  22669  lgseisen  22672  lgsquadlem1  22673  lgsquadlem2  22674  lgsquad2lem1  22677  lgsquad2  22679  m1lgs  22681  2sqlem8  22691  2sqlem10  22693  2sqlem11  22694  2sqblem  22696  chtppilimlem2  22703  chebbnd2  22706  chto1lb  22707  rplogsumlem1  22713  rpvmasumlem  22716  dchrmusumlema  22722  dchrmusum2  22723  dchrisum0flblem1  22737  rpvmasum2  22741  mudivsum  22759  mulogsum  22761  vmalogdivsum2  22767  selberg2lem  22779  logdivbnd  22785  pntrmax  22793  pntrsumo1  22794  pntrsumbnd2  22796  pntrlog2bndlem5  22810  pntpbnd1a  22814  pntpbnd2  22816  pntibndlem2  22820  pntlemd  22823  pntlemc  22824  pntlemr  22831  ostth2lem2  22863  brbtwn2  23119  colinearalglem4  23123  ax5seglem1  23142  ax5seglem2  23143  ax5seglem3  23145  ax5seglem5  23147  ax5seglem7  23149  ax5seglem9  23151  axbtwnid  23153  axpaschlem  23154  axlowdimlem13  23168  axlowdimlem14  23169  axlowdimlem16  23171  axeuclidlem  23176  axcontlem2  23179  axcontlem4  23181  axcontlem7  23184  axcontlem8  23185  usgraexvlem  23281  cusgrasizeinds  23352  cusgrasize2inds  23353  wlkdvspthlem  23474  fargshiftf1  23491  fargshiftfo  23492  eupatrl  23557  eupares  23564  eupap1  23565  eupath2lem3  23568  ex-fl  23622  gxsuc  23727  gxnn0add  23729  gxnn0mul  23732  ablomul  23810  mulid  23811  cnrngo  23858  vc2  23901  vc0  23915  vcm  23917  vcoprne  23925  nvm1  24020  nvmtri  24027  nvge0  24030  ipval2lem3  24068  ipval2lem6  24074  ipidsq  24076  lnoadd  24126  ip1ilem  24194  ip1i  24195  ip2i  24196  ipdirilem  24197  ipasslem1  24199  ipasslem2  24200  ipasslem10  24207  minvecolem2  24244  hvsubid  24396  hv2times  24431  hisubcomi  24474  normlem9  24488  normlem7tALT  24489  norm-ii-i  24507  normsubi  24511  hhssnv  24633  pjhthlem1  24762  h1de2bi  24925  homulid2  25172  ho2times  25191  lnop0  25338  lnopaddi  25343  lnophmlem2  25389  lnfn0i  25414  lnfnaddi  25415  hst1h  25599  sto2i  25609  stadd3i  25620  addltmulALT  25818  bcm1n  26047  ltesubnnd  26059  omndmul2  26143  isarchi3  26172  archirngz  26174  archiabllem1a  26176  qqhval2lem  26379  logb1  26431  dya2ub  26654  dya2icoseg  26661  eulerpartlemgs2  26732  fib5  26757  fib6  26758  ballotlem2  26840  ballotlemfp1  26843  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemic  26858  ballotlem1c  26859  ballotlemsgt1  26862  ballotlemsdom  26863  ballotlemsel1i  26864  ballotlemsi  26866  ballotlemsima  26867  ballotlem1ri  26886  sgnneg  26892  sgn0bi  26899  signswch  26931  signstfvn  26939  signsvtn0  26940  signstfveq0  26947  signsvfn  26952  signsvtn  26954  signlem0  26957  signshf  26958  zetacvg  26970  lgamgulmlem2  26985  lgamgulmlem3  26986  lgamgulmlem4  26987  lgamgulmlem5  26988  lgamgulmlem6  26989  lgamgulm2  26991  lgamcvg2  27010  gamcvg  27011  gamcvg2lem  27014  lgam1  27019  gam1  27020  gamfac  27022  subfacp1lem1  27036  subfacp1lem5  27041  subfacp1lem6  27042  subfacval2  27044  subfaclim  27045  subfacval3  27046  cvxpcon  27100  cvxscon  27101  rescon  27104  cvmliftlem7  27149  cvmliftlem10  27152  problem4  27270  sinccvglem  27286  relexpadd  27309  sqdivzi  27352  4bc3eq4  27359  halfthird  27361  5recm6rec  27362  divcnvlin  27368  muls1d  27369  prodf1  27375  prodfclim1  27377  prodfrec  27379  ntrivcvg  27381  ntrivcvgtail  27384  prodrblem  27411  fprodcvg  27412  prodmolem2a  27416  zprod  27419  fprodntriv  27424  prod1  27426  prodss  27429  fprodss  27430  fprodser  27431  fprodcl  27434  fprodsplit  27445  fprodm1  27446  fprodp1  27448  iprodgam  27475  risefacval2  27482  fallfacval2  27483  risefaccl  27487  fallfaccl  27488  risefacp1  27501  fallfacp1  27502  risefacfac  27507  fallfacfwd  27508  binomfallfaclem2  27512  binomfallfac  27513  fallfacval4  27515  faclimlem1  27518  faclimlem2  27519  faclimlem3  27520  faclim  27521  iprodfac  27522  faclim2  27523  predfz  27633  bpolycl  28164  bpolysum  28165  bpolydiflem  28166  fsumkthpow  28168  bpoly2  28169  bpoly3  28170  bpoly4  28171  fsumcube  28172  ltflcei  28390  sin2h  28393  cos2h  28394  tan2h  28395  opnmbllem0  28398  mblfinlem2  28400  mblfinlem3  28401  0mbf  28408  dvtan  28413  itg2addnclem2  28415  itg2addnclem3  28416  dvcnsqr  28449  dvasin  28451  dvacos  28452  areacirclem1  28455  areacirclem4  28458  areacirc  28460  fdc  28612  mettrifi  28624  heiborlem4  28684  heiborlem6  28686  bfp  28694  eldioph2lem1  29069  lzenom  29079  irrapxlem1  29134  pell1qrge1  29182  rmspecsqrnq  29218  rmspecfund  29221  rmxm1  29246  rmym1  29247  2nn0ind  29257  jm2.24nn  29273  jm2.17a  29274  jm2.17b  29275  jm2.17c  29276  jm2.24  29277  acongeq  29297  jm2.18  29308  jm2.19lem3  29311  jm2.25  29319  jm2.16nn0  29324  jm2.27c  29327  jm3.1lem1  29337  jm3.1lem2  29338  rngunsnply  29501  flcidc  29502  ofdivrec  29571  lhe4.4ex1a  29574  expgrowthi  29578  expgrowth  29580  refsum2cnlem1  29730  fmul01lt1lem2  29737  m1expeven  29743  clim1fr1  29745  isumneg  29746  climneg  29754  itgsin0pilem1  29761  itgsinexp  29766  stoweidlem13  29779  stoweidlem26  29792  stoweidlem34  29800  stoweidlem38  29804  wallispilem2  29832  wallispilem3  29833  wallispilem4  29834  wallispilem5  29835  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  wallispi2  29839  stirlinglem1  29840  stirlinglem3  29842  stirlinglem4  29843  stirlinglem5  29844  stirlinglem6  29845  stirlinglem7  29846  stirlinglem8  29847  stirlinglem10  29849  stirlinglem11  29850  stirlinglem12  29851  stirlinglem13  29852  stirlinglem15  29854  sigaradd  29873  cnm1cn  30138  kcnktkm1cn  30141  mulsubfacd  30143  cnm2m1cnm3  30150  add1p1  30151  elfzom1elfzo  30188  zpnn0elfzo1  30193  fzosplitpr  30194  fzosplitprm1  30195  ccatw2s1p2  30241  wlklenfislenpm1  30255  wwlknimp  30292  wlkiswwlk1  30295  wlklniswwlkn2  30305  wwlknred  30326  wwlknext  30327  wwlknextbi  30328  wwlknredwwlkn  30329  wwlkextwrd  30331  wwlkextinj  30333  clwlkisclwwlklem2a1  30412  clwlkisclwwlklem2a4  30417  clwlkisclwwlklem2a  30418  clwlkisclwwlklem1  30420  clwlkisclwwlklem0  30421  clwlkisclwwlk  30422  clwwlkel  30426  clwwlkf  30427  clwwlkf1  30429  clwwlkext2edg  30435  wwlkext2clwwlk  30436  clwwisshclwwlem1  30440  clwwisshclww  30442  wlkp1lenfislenp  30483  nbhashuvtx1  30504  wwlkextproplem2  30532  wwlkextproplem3  30533  rusgra0edg  30544  frghash2spot  30627  usgreghash2spotv  30630  frgregordn0  30634  extwwlkfablem1  30638  extwwlkfablem2  30642  numclwwlkovf2ex  30650  numclwlk1lem2foa  30655  numclwlk1lem2fo  30659  numclwlk2lem2f  30667  numclwlk2lem2f1o  30669  numclwwlk6  30677  altgsumbcALT  30719  exple2lt6  30736  onetansqsecsq  31027  cotsqcscsq  31028  5m4e1  31078  isosctrlem1ALT  31599
  Copyright terms: Public domain W3C validator