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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9162 . 2
2 cc 9159 . 2
31, 2wcel 1732 1
Colors of variables: wff set class
This axiom is referenced by:  0cn  9257  1ex  9260  mulid1  9262  mulid2  9263  1re  9264  1cnd  9281  muladd11  9416  1p1times  9417  peano2cn  9418  mul02lem2  9423  addid1  9426  cnegex2  9428  addcom  9432  addcomd  9448  0reALT  9580  pncan1  9646  npcan1  9647  ine0  9654  mulm1  9660  0lt1  9736  ixi  9838  muleqadd  9853  reccl  9872  recne0  9878  recid  9879  recid2  9880  div1  9894  1div1e1  9895  diveq1  9896  recrec  9899  rec11  9900  rec11r  9901  recdiv  9908  divdiv1  9913  divdiv2  9914  recdiv2  9915  conjmul  9919  rereccl  9920  eqneg  9922  div2neg  9925  subrec  10031  recp1lt1  10096  recreclt  10097  recgt0ii  10104  inelr  10178  ofnegsub  10186  peano5nni  10191  nn1m1nn  10208  nn1suc  10209  nnaddcl  10210  nnmulcl  10211  nnsub  10226  1m1e0  10256  neg1cn  10291  neg1ne0  10293  negneg1e1  10295  1pneg1e0  10296  1m0e1  10298  0p1e1  10299  1p0e1  10300  2m1e1  10302  3m1e2  10304  2p2e4  10305  2times  10306  1p2e3  10312  3p2e5  10320  3p3e6  10321  4p2e6  10322  4p3e7  10323  4p4e8  10324  5p2e7  10325  5p3e8  10326  5p4e9  10327  5p5e10  10328  6p2e8  10329  6p3e9  10330  6p4e10  10331  7p2e9  10332  7p3e10  10333  8p2e10  10334  1t1e1  10335  3t3e9  10340  neg1mulneg1e1  10405  1mhlfehlf  10410  8th4div3  10411  halfpm6th  10412  addltmul  10426  sub1m1  10440  elnn0nn  10488  elnnnn0  10489  nn0n0n1ge2  10507  elz2  10527  zlem1lt  10560  zltlem1  10561  nnaddm1cl  10565  zextlt  10580  zneo  10588  nneo  10589  zeo  10591  peano5uzi  10594  uzindOLD  10600  numsuc  10631  numltc  10639  numsucc  10645  numaddc  10654  6p5lem  10668  4t3lem  10690  7t4e28  10703  decbin2  10723  uzp1  10758  peano2uzr  10774  uzaddcl  10775  rebtwnz  10816  qbtwnre  11033  lincmb01cmp  11288  iccf1o  11289  xov1plusxeqvd  11291  fz01en  11333  fztp  11365  fzsuc2  11367  fztpval  11370  fseq1m1p1  11387  elfzp1b  11389  fzm1  11392  fzoss2  11429  fzval3  11457  fzosplitsnm1  11460  fzo0to42pr  11465  ubmelm1fzo  11472  fzoshftral  11485  fladdz  11519  ltdifltdiv  11527  dfceil2  11529  ceim1l  11535  fldiv  11548  modvalp1  11575  modnegd  11603  uzrdgxfr  11638  fzen2  11640  nn0ennn  11650  seqm1  11672  seqshft2  11681  monoord2  11686  sermono  11687  seqf1olem1  11694  seqf1olem2  11695  seqz  11703  ser1const  11711  expcl  11732  m1expcl2  11736  expclzlem  11738  expm1t  11741  1exp  11742  mulexpz  11753  expadd  11755  expaddz  11757  expmul  11758  expubnd  11773  sqrecii  11797  neg1sqe1  11810  irec  11814  i4  11817  binom21  11831  binom3  11834  sq01  11835  zesq  11836  crreczi  11838  bernneq  11839  bernneq2  11840  nn0opthlem1  11895  facnn2  11909  facndiv  11913  faclbnd4lem1  11918  faclbnd6  11924  bcnp1n  11939  bcm1k  11940  bcp1n  11941  bcp1nk  11942  bcn2  11944  bcp1m1  11945  bcpasc  11946  bcn2m1  11949  hashgadd  11989  hashfz  12035  hashfzo  12037  hashxplem  12042  hashbclem  12052  hashf1lem2  12056  hashf1  12057  seqcoll  12063  brfi1indlem  12065  lswccatn0lsw  12134  wrdlenccats1lenm1  12152  swrds1  12192  swrdlsw  12193  swrdccatwrd  12209  wrdeqcats1  12215  wrdind  12218  wrd2ind  12219  revccat  12253  repswrevw  12271  cshwidxm1  12290  cshwidxn  12292  cshweqrep  12302  swrds2  12392  swrd2lsw  12399  rei  12492  imi  12493  absexpz  12641  recan  12671  reccn2  12921  iserex  12981  isercolllem1  12989  isercoll2  12993  serf0  13005  iseraltlem2  13007  iseraltlem3  13008  iseralt  13009  sumrblem  13036  fsumm1  13068  fsump1  13071  fsumtscopo  13112  fsumparts  13116  hashiun  13132  binomlem  13139  binom  13140  binom1p  13141  binom11  13142  binom1dif  13143  bcxmas  13145  isumsplit  13150  isum1p  13151  climcndslem1  13159  supcvg  13165  harmonic  13168  arisum  13169  arisum2  13170  trireciplem  13171  geoserg  13175  geolim  13177  geolim2  13178  georeclim  13179  geo2sum  13180  geo2sum2  13181  geoisum1c  13187  0.999...  13188  geoihalfsum  13189  cvgrat  13190  mertenslem1  13191  mertenslem2  13192  mertens  13193  esum  13213  ege2le3  13222  efsub  13231  efexp  13232  efzval  13233  eftlub  13240  effsumlt  13242  ef4p  13244  tanval3  13265  efi4p  13268  tan0  13282  efival  13283  tanadd  13298  cos2t  13309  cos2tsin  13310  ef01bndlem  13315  cos1bnd  13318  cos2bnd  13319  demoivreALT  13332  eirrlem  13333  rpnnen2lem3  13346  rpnnen2lem11  13354  ruclem12  13370  odd2np1lem  13438  odd2np1  13439  oddm1even  13440  oddp1even  13441  oexpneg  13442  3dvds  13443  bitsp1o  13476  bitsfzo  13478  sadcp1  13498  gcdmultiple  13581  sqgcd  13589  nn0seqcvgd  13592  prmind2  13621  qredeu  13640  hashdvds  13697  phiprmpw  13698  phiprm  13699  eulerthlem2  13704  prmdiv  13707  prmdiveq  13708  opoe  13725  omoe  13726  opeo  13727  omeo  13728  iserodd  13749  pcexp  13773  pc2dvds  13792  sumhash  13805  fldivp1  13806  prmpwdvds  13812  pockthlem  13813  pockthi  13815  prmreclem2  13825  prmreclem4  13827  prmreclem6  13829  4sqlem11  13863  4sqlem12  13864  4sqlem19  13871  vdwapun  13882  vdwapid1  13883  vdwlem3  13891  vdwlem5  13893  vdwlem6  13894  vdwlem8  13896  vdwlem9  13897  vdwnnlem2  13904  ramub1lem1  13934  ramub1lem2  13935  ramcl  13937  dec5nprm  13942  decexp2  13951  2exp16  13964  prmlem0  13980  43prm  13996  83prm  13997  139prm  13998  163prm  13999  317prm  14000  631prm  14001  1259lem1  14002  1259lem2  14003  1259lem3  14004  1259lem4  14005  1259lem5  14006  1259prm  14007  2503lem1  14008  2503lem2  14009  2503lem3  14010  2503prm  14011  4001lem1  14012  4001lem2  14013  4001lem3  14014  4001lem4  14015  4001prm  14016  gsumccat  15357  mulgnndir  15483  mulgneg2  15488  sylow1lem1  15841  sylow2a  15862  efgsval2  15974  efgsrel  15975  efgsres  15979  efgredlemc  15986  cncrng  17347  cnfld1  17351  zsssubrg  17382  gzrngunit  17389  zrngunit  17390  zcyg  17397  prmirredlem  17398  mulgrhm2  17413  psgnunilem5  17647  psgnunilem2  17648  m1expaddsub  17651  cnmsgnsubg  17672  cnmsgnbas  17673  cnmsgngrp  17674  psgninv  17677  zrhpsgnodpm  17690  evpmodpmf1o  17694  nminvr  19720  blcvx  19844  iihalf2  19973  icopnfcnv  19982  icopnfhmeo  19983  iccpnfhmeo  19985  xrhmeo  19986  icccvx  19990  lebnumii  20006  reparphti  20037  pcoass  20064  pcorevlem  20066  pcorev2  20068  pi1xfrcnv  20097  pjthlem1  20353  ovolunlem1a  20407  ovolunlem1  20408  ovolicc2lem4  20431  uniioombllem3  20492  uniioombllem4  20493  dyadovol  20500  vitalilem4  20518  iblitg  20673  iblcnlem1  20692  itgcnlem  20694  dvid  20819  dvexp  20854  dvexp2  20855  dvmptid  20858  dvexp3  20877  dveflem  20878  dvef  20879  dvlipcn  20893  dvcvx  20919  dvfsumle  20920  dvfsumlem1  20925  degltp1le  21011  ply1divex  21074  fta1glem1  21103  plyaddlem1  21147  plymullem1  21148  coeidp  21196  dgrid  21197  dvply1  21216  dvply2g  21217  plyremlem  21236  fta1lem  21239  vieta1lem1  21242  vieta1lem2  21243  qaa  21255  iaa  21257  aalioulem3  21266  geolim3  21271  aaliou3lem2  21275  aaliou3lem8  21277  aaliou3lem7  21281  taylply2  21299  dvradcnv  21352  pserdvlem2  21359  pserdv2  21361  abelthlem1  21362  abelthlem2  21363  abelthlem6  21367  abelthlem7  21369  abelth  21372  reeff1olem  21377  reeff1o  21378  efcvx  21380  sinhalfpilem  21391  eulerid  21402  cos2pi  21404  sincosq3sgn  21428  sincosq4sgn  21429  tangtx  21433  sincos4thpi  21441  sincos6thpi  21443  pige3  21445  abssinper  21446  coskpi  21448  coseq1  21450  efeq1  21451  tanregt0  21461  logneg2  21530  logdivlti  21535  logcnlem4  21556  dvlog2lem  21563  dvlog2  21564  advlog  21565  advlogexp  21566  logtayl  21571  logtayl2  21573  logccv  21574  cxpval  21575  1cxp  21583  cxpcl  21585  cxpp1  21591  cxpsqr  21614  dvsqr  21648  sqrcn  21654  cxpaddlelem  21655  root1id  21658  root1cj  21660  loglesqr  21662  ang180lem1  21671  ang180lem2  21672  ang180lem3  21673  logrec  21681  isosctrlem1  21682  isosctrlem2  21683  affineequiv  21687  affineequiv2  21688  angpieqvdlem  21689  1cubrlem  21702  1cubr  21703  dcubic2  21705  dcubic  21707  mcubic  21708  binom4  21711  dquartlem1  21712  quart1lem  21716  quart1  21717  quartlem1  21718  asinlem  21729  asinlem2  21730  asinlem3a  21731  asinlem3  21732  asinf  21733  atandm2  21738  atandm4  21740  atanf  21741  asinneg  21747  efiasin  21749  sinasin  21750  asinsin  21753  asin1  21755  acos1  21756  reasinsin  21757  asinbnd  21760  cosasin  21765  atanneg  21768  atancj  21771  efiatan  21773  atanlogaddlem  21774  atanlogadd  21775  atanlogsublem  21776  atanlogsub  21777  efiatan2  21778  2efiatan  21779  tanatan  21780  cosatan  21782  cosatanne0  21783  atantan  21784  atanbndlem  21786  bndatandm  21790  atans2  21792  dvatan  21796  atantayl  21798  atantayl2  21799  atantayl3  21800  leibpilem1  21801  leibpilem2  21802  leibpi  21803  log2cnv  21805  log2tlbnd  21806  log2ublem3  21809  log2ub  21810  birthdaylem2  21812  birthday  21814  efrlim  21829  dfef2  21830  cvxcl  21844  scvxcvx  21845  emcllem2  21856  emcllem4  21858  emcllem7  21861  harmonicbnd4  21870  fsumharmonic  21871  wilthlem1  21872  wilthlem2  21873  wilthlem3  21874  basellem2  21885  basellem5  21888  basellem6  21889  basellem7  21890  basellem8  21891  basellem9  21892  0sgm  21948  mule1  21952  ppiprm  21955  ppinprm  21956  chtprm  21957  chtnprm  21958  chpp1  21959  mumullem2  21984  sqff1o  21986  1sgmprm  22004  1sgm2ppw  22005  ppiublem2  22008  ppiub  22009  chtublem  22016  chtub  22017  logfaclbnd  22027  logfacbnd3  22028  logfacrlim  22029  logexprlim  22030  mersenne  22032  perfect1  22033  perfectlem1  22034  perfectlem2  22035  perfect  22036  dchrelbasd  22044  dchr1cl  22056  dchrmulid2  22057  dchrinvcl  22058  dchrfi  22060  dchr1  22062  dchrsum2  22073  sumdchr2  22075  bcmono  22082  bcp1ctr  22084  bclbnd  22085  bposlem8  22096  lgslem1  22101  lgslem2  22102  lgsfcl2  22107  lgsvalmod  22120  lgsneg  22124  lgsdilem  22127  lgsdir2lem1  22128  lgsdir2lem2  22129  lgsdir2lem3  22130  lgsdir2lem5  22132  lgsdir2  22133  lgsdir  22135  lgsdi  22137  lgsne0  22138  lgseisenlem1  22154  lgseisenlem2  22155  lgseisenlem4  22157  lgseisen  22158  lgsquadlem1  22159  lgsquadlem2  22160  lgsquad2lem1  22163  lgsquad2  22165  m1lgs  22167  2sqlem8  22177  2sqlem10  22179  2sqlem11  22180  2sqblem  22182  chtppilimlem2  22189  chebbnd2  22192  chto1lb  22193  rplogsumlem1  22199  rpvmasumlem  22202  dchrmusumlema  22208  dchrmusum2  22209  dchrisum0flblem1  22223  rpvmasum2  22227  mudivsum  22245  mulogsum  22247  vmalogdivsum2  22253  selberg2lem  22265  logdivbnd  22271  pntrmax  22279  pntrsumo1  22280  pntrsumbnd2  22282  pntrlog2bndlem5  22296  pntpbnd1a  22300  pntpbnd2  22302  pntibndlem2  22306  pntlemd  22309  pntlemc  22310  pntlemr  22317  ostth2lem2  22349  usgraexvlem  22435  cusgrasizeinds  22506  cusgrasize2inds  22507  wlkdvspthlem  22628  fargshiftf1  22645  fargshiftfo  22646  eupatrl  22711  eupares  22718  eupap1  22719  eupath2lem3  22722  ex-fl  22776  gxsuc  22881  gxnn0add  22883  gxnn0mul  22886  ablomul  22964  mulid  22965  cnrngo  23012  vc2  23055  vc0  23069  vcm  23071  vcoprne  23079  nvm1  23174  nvmtri  23181  nvge0  23184  ipval2lem3  23222  ipval2lem6  23228  ipidsq  23230  lnoadd  23280  ip1ilem  23348  ip1i  23349  ip2i  23350  ipdirilem  23351  ipasslem1  23353  ipasslem2  23354  ipasslem10  23361  minvecolem2  23398  hvsubid  23550  hv2times  23585  hisubcomi  23628  normlem9  23642  normlem7tALT  23643  norm-ii-i  23661  normsubi  23665  hhssnv  23787  pjhthlem1  23916  h1de2bi  24079  homulid2  24326  ho2times  24345  lnop0  24492  lnopaddi  24497  lnophmlem2  24543  lnfn0i  24568  lnfnaddi  24569  hst1h  24753  sto2i  24763  stadd3i  24774  addltmulALT  24972  bcm1n  25209  ltesubnnd  25221  omndmul2  25307  isarchi3  25336  archirngz  25338  archiabllem1a  25340  qqhval2lem  25590  logb1  25642  dya2ub  25865  dya2icoseg  25872  eulerpartlemgs2  25937  ballotlem2  26021  ballotlemfp1  26024  ballotlemfc0  26025  ballotlemfcc  26026  ballotlemic  26039  ballotlem1c  26040  ballotlemsgt1  26043  ballotlemsdom  26044  ballotlemsel1i  26045  ballotlemsi  26047  ballotlemsima  26048  ballotlem1ri  26067  sgnneg  26073  sgn0bi  26080  signswch  26113  signstfvn  26121  signsvtn0  26122  signstfveq0  26129  signsvfn  26134  signsvtn  26136  signlem0  26139  signshf  26140  zetacvg  26147  lgamgulmlem2  26162  lgamgulmlem3  26163  lgamgulmlem4  26164  lgamgulmlem5  26165  lgamgulmlem6  26166  lgamgulm2  26168  lgamcvg2  26187  gamcvg  26188  gamcvg2lem  26191  lgam1  26196  gam1  26197  gamfac  26199  subfacp1lem1  26213  subfacp1lem5  26218  subfacp1lem6  26219  subfacval2  26221  subfaclim  26222  subfacval3  26223  cvxpcon  26277  cvxscon  26278  rescon  26281  cvmliftlem7  26326  cvmliftlem10  26329  sinccvglem  26457  relexpadd  26480  sqdivzi  26523  4bc3eq4  26542  halfthird  26544  5recm6rec  26545  divcnvlin  26551  muls1d  26552  prodf1  26558  prodfclim1  26560  prodfrec  26562  ntrivcvg  26564  ntrivcvgtail  26567  prodrblem  26594  fprodcvg  26595  prodmolem2a  26599  zprod  26602  fprodntriv  26607  prod1  26609  prodss  26612  fprodss  26613  fprodser  26614  fprodcl  26617  fprodsplit  26628  fprodm1  26629  fprodp1  26631  iprodgam  26658  risefacval2  26665  fallfacval2  26666  risefaccl  26670  fallfaccl  26671  risefacp1  26684  fallfacp1  26685  risefacfac  26690  fallfacfwd  26691  binomfallfaclem2  26695  binomfallfac  26696  fallfacval4  26698  faclimlem1  26701  faclimlem2  26702  faclimlem3  26703  faclim  26704  iprodfac  26705  faclim2  26706  predfz  26817  brbtwn2  27183  colinearalglem4  27187  ax5seglem1  27206  ax5seglem2  27207  ax5seglem3  27209  ax5seglem5  27211  ax5seglem7  27213  ax5seglem9  27215  axbtwnid  27217  axpaschlem  27218  axlowdimlem13  27232  axlowdimlem14  27233  axlowdimlem16  27235  axeuclidlem  27240  axcontlem2  27243  axcontlem4  27245  axcontlem7  27248  axcontlem8  27249  bpolycl  27437  bpolysum  27438  bpolydiflem  27439  fsumkthpow  27441  bpoly2  27442  bpoly3  27443  bpoly4  27444  fsumcube  27445  ltflcei  27600  sin2h  27603  cos2h  27604  tan2h  27605  opnmbllem0  27607  mblfinlem2  27609  mblfinlem3  27610  0mbf  27617  dvtan  27622  itg2addnclem2  27624  itg2addnclem3  27625  dvcnsqr  27658  dvasin  27660  dvacos  27661  areacirclem1  27664  areacirclem4  27667  areacirc  27669  fdc  27821  mettrifi  27835  heiborlem4  27895  heiborlem6  27897  bfp  27905  eldioph2lem1  28246  lzenom  28256  irrapxlem1  28311  pell1qrge1  28359  rmspecsqrnq  28395  rmspecfund  28398  rmxm1  28423  rmym1  28424  2nn0ind  28434  jm2.24nn  28450  jm2.17a  28451  jm2.17b  28452  jm2.17c  28453  jm2.24  28454  acongeq  28474  jm2.18  28485  jm2.19lem3  28488  jm2.25  28496  jm2.16nn0  28501  jm2.27c  28504  jm3.1lem1  28514  jm3.1lem2  28515  rngunsnply  28718  flcidc  28719  ofdivrec  28774  lhe4.4ex1a  28777  expgrowthi  28781  expgrowth  28783  refsum2cnlem1  28934  fmul01lt1lem2  28941  m1expeven  28950  clim1fr1  28952  isumneg  28953  climneg  28961  itgsin0pilem1  28969  itgsinexp  28974  stoweidlem1  28975  stoweidlem7  28981  stoweidlem10  28984  stoweidlem11  28985  stoweidlem13  28987  stoweidlem14  28988  stoweidlem17  28991  stoweidlem26  29000  stoweidlem34  29008  stoweidlem38  29012  stoweidlem42  29016  wallispilem2  29040  wallispilem3  29041  wallispilem4  29042  wallispilem5  29043  wallispi  29044  wallispi2lem1  29045  wallispi2lem2  29046  wallispi2  29047  stirlinglem1  29048  stirlinglem3  29050  stirlinglem4  29051  stirlinglem5  29052  stirlinglem6  29053  stirlinglem7  29054  stirlinglem8  29055  stirlinglem10  29057  stirlinglem11  29058  stirlinglem12  29059  stirlinglem13  29060  stirlinglem15  29062  sigaradd  29081  cnm1cn  29346  kcnktkm1cn  29349  mulsubfacd  29351  cnm2m1cnm3  29358  add1p1  29359  elfzom1elfzo  29398  zpnn0elfzo1  29403  fzosplitpr  29404  fzosplitprm1  29405  ccatw2s1p2  29451  wlklenfislenpm1  29465  wwlknimp  29502  wlkiswwlk1  29505  wlklniswwlkn2  29515  wwlknred  29536  wwlknext  29537  wwlknextbi  29538  wwlknredwwlkn  29539  wwlkextwrd  29541  wwlkextinj  29543  clwlkisclwwlklem2a1  29622  clwlkisclwwlklem2a4  29627  clwlkisclwwlklem2a  29628  clwlkisclwwlklem1  29630  clwlkisclwwlklem0  29631  clwlkisclwwlk  29632  clwwlkel  29636  clwwlkf  29637  clwwlkf1  29639  clwwlkext2edg  29645  wwlkext2clwwlk  29646  clwwisshclwwlem1  29650  clwwisshclww  29652  wlkp1lenfislenp  29693  nbhashuvtx1  29714  wwlkextproplem2  29742  wwlkextproplem3  29743  rusgra0edg  29754  frghash2spot  29837  usgreghash2spotv  29840  frgregordn0  29844  extwwlkfablem1  29848  extwwlkfablem2  29852  numclwwlkovf2ex  29860  numclwlk1lem2foa  29865  numclwlk1lem2fo  29869  numclwlk2lem2f  29877  numclwlk2lem2f1o  29879  numclwwlk6  29887  onetansqsecsq  29946  cotsqcscsq  29947  5m4e1  30001  isosctrlem1ALT  30516
  Copyright terms: Public domain W3C validator