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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9042 . 2
2 cc 9039 . 2
31, 2wcel 1728 1
Colors of variables: wff set class
This axiom is referenced by:  0cn  9135  1ex  9137  mulid1  9139  mulid2  9140  1re  9141  muladd11  9287  1p1times  9288  peano2cn  9289  mul02lem2  9294  addid1  9297  cnegex2  9299  addcom  9303  addcomd  9319  0reALT  9448  ine0  9520  mulm1  9526  0lt1  9601  ixi  9702  muleqadd  9717  reccl  9736  recne0  9742  recid  9743  recid2  9744  div1  9758  diveq1  9759  recrec  9762  rec11  9763  rec11r  9764  recdiv  9771  divdiv1  9776  divdiv2  9777  recdiv2  9778  conjmul  9782  rereccl  9783  eqneg  9785  div2neg  9788  subrec  9894  reclt1  9956  recgt1  9957  recp1lt1  9959  recreclt  9960  recgt0ii  9967  inelr  10041  ofnegsub  10049  peano5nni  10054  nn1m1nn  10071  nn1suc  10072  nnaddcl  10073  nnmulcl  10074  nnsub  10089  neg1cn  10118  1m1e0  10119  0p1e1  10144  2m1e1  10146  3m1e2  10147  3m1e2OLD  10148  2p2e4  10149  2times  10150  3p2e5  10162  3p3e6  10163  4p2e6  10164  4p3e7  10165  4p4e8  10166  5p2e7  10167  5p3e8  10168  5p4e9  10169  5p5e10  10170  6p2e8  10171  6p3e9  10172  6p4e10  10173  7p2e9  10174  7p3e10  10175  8p2e10  10176  1t1e1  10177  3t3e9  10180  halflt1  10240  1mhlfehlf  10241  8th4div3  10242  halfpm6th  10243  addltmul  10254  elnn0nn  10313  elnnnn0  10314  nn0n0n1ge2  10331  elz2  10349  zlem1lt  10378  zltlem1  10379  nnaddm1cl  10382  zextlt  10395  zneo  10403  nneo  10404  zeo  10406  peano5uzi  10409  uzindOLD  10415  numsuc  10445  numltc  10453  numsucc  10459  numaddc  10468  6p5lem  10482  4t3lem  10504  7t4e28  10517  decbin2  10537  uzp1  10570  peano2uzr  10583  uzaddcl  10584  rebtwnz  10624  rpnnen1lem5  10655  qbtwnre  10836  lincmb01cmp  11089  iccf1o  11090  xov1plusxeqvd  11092  fz01en  11130  fztp  11153  fzsuc2  11155  fztpval  11158  fseq1m1p1  11174  fzm1  11178  fzoss2  11214  fzval3  11231  fzo0to42pr  11237  fladdz  11278  ceim1l  11285  fldiv  11292  modnegd  11332  uzrdgxfr  11357  fzen2  11359  nn0ennn  11369  seqm1  11391  seqshft2  11400  monoord2  11405  sermono  11406  seqf1olem1  11413  seqf1olem2  11414  seqz  11422  ser1const  11430  expneg  11440  expcl  11450  m1expcl2  11454  expclzlem  11456  expm1t  11459  1exp  11460  mulexpz  11471  expadd  11473  expaddz  11475  expmul  11476  expubnd  11491  sqrecii  11515  irec  11531  i4  11534  binom21  11548  binom3  11551  sq01  11552  zesq  11553  crreczi  11555  bernneq  11556  bernneq2  11557  nn0opthlem1  11612  facnn2  11626  facndiv  11630  faclbnd4lem1  11635  faclbnd6  11641  bcnp1n  11656  bcm1k  11657  bcp1n  11658  bcp1nk  11659  bcn2  11661  bcp1m1  11662  bcpasc  11663  bcn2m1  11666  hashgadd  11702  hashfz  11743  hashfzo  11745  hashxplem  11747  hashbclem  11752  hashf1lem2  11756  hashf1  11757  fz1isolem  11761  seqcoll  11763  brfi1indlem  11765  swrds1  11838  wrdeqcats1  11839  wrdind  11842  revccat  11849  swrds2  11931  rei  12012  imi  12013  resqrex  12107  absi  12142  absexpz  12161  recan  12191  reccn2  12441  iserex  12501  isercolllem1  12509  isercoll2  12513  serf0  12525  iseraltlem2  12527  iseraltlem3  12528  iseralt  12529  sumrblem  12556  fsumm1  12588  fsump1  12591  fsumtscopo  12632  fsumparts  12636  hashiun  12652  binomlem  12659  binom  12660  binom1p  12661  binom11  12662  binom1dif  12663  bcxmas  12666  incexc  12668  incexc2  12669  isumsplit  12671  isum1p  12672  climcndslem1  12680  supcvg  12686  harmonic  12689  arisum  12690  arisum2  12691  trireciplem  12692  geoserg  12696  geolim  12698  geolim2  12699  georeclim  12700  geo2sum  12701  geo2sum2  12702  geoisum1c  12708  0.999...  12709  geoihalfsum  12710  cvgrat  12711  mertenslem1  12712  mertenslem2  12713  mertens  12714  ef0lem  12732  esum  12734  ege2le3  12743  efsub  12752  efexp  12753  efzval  12754  eftlub  12761  effsumlt  12763  eft0val  12764  ef4p  12765  tanval3  12786  efi4p  12789  tan0  12803  efival  12804  sinhval  12806  coshval  12807  tanaddlem  12818  tanadd  12819  cos2t  12830  cos2tsin  12831  ef01bndlem  12836  cos01bnd  12838  cos1bnd  12839  cos2bnd  12840  demoivreALT  12853  eirrlem  12854  rpnnen2lem3  12867  rpnnen2lem11  12875  ruclem12  12891  odd2np1lem  12958  odd2np1  12959  oddm1even  12960  oddp1even  12961  oexpneg  12962  3dvds  12963  bitsp1o  12996  bitsfzo  12998  bitsf1  13009  sadcp1  13018  gcdmultiple  13101  sqgcd  13109  nn0seqcvgd  13112  prmind2  13141  qredeu  13158  hashdvds  13215  phiprmpw  13216  phiprm  13217  eulerthlem2  13222  prmdiv  13225  prmdiveq  13226  opoe  13236  omoe  13237  opeo  13238  omeo  13239  iserodd  13260  pcexp  13284  pc2dvds  13303  sumhash  13316  fldivp1  13317  prmpwdvds  13323  pockthlem  13324  pockthi  13326  prmreclem2  13336  prmreclem4  13338  prmreclem6  13340  4sqlem11  13374  4sqlem12  13375  4sqlem19  13382  vdwapun  13393  vdwapid1  13394  vdwlem3  13402  vdwlem5  13404  vdwlem6  13405  vdwlem8  13407  vdwlem9  13408  vdwnnlem2  13415  ramub1lem1  13445  ramub1lem2  13446  ramcl  13448  dec5nprm  13453  decexp2  13462  2exp16  13475  prmlem0  13479  prmlem1a  13480  23prm  13492  prmlem2  13493  43prm  13495  83prm  13496  139prm  13497  163prm  13498  317prm  13499  631prm  13500  1259lem1  13501  1259lem2  13502  1259lem3  13503  1259lem4  13504  1259lem5  13505  1259prm  13506  2503lem1  13507  2503lem2  13508  2503lem3  13509  2503prm  13510  4001lem1  13511  4001lem2  13512  4001lem3  13513  4001lem4  13514  4001prm  13515  gsumccat  14838  mulgnndir  14963  mulgneg2  14968  mulgnnass  14969  sylow1lem1  15283  sylow2a  15304  efgsval2  15416  efgsrel  15417  efgsres  15421  efgredlemc  15428  odadd2  15515  cncrng  16773  cnfld1  16777  cnfldmulg  16784  zsssubrg  16808  gzrngunit  16815  zrngunit  16816  zcyg  16823  prmirredlem  16824  mulgrhm2  16839  nminvr  18756  blcvx  18880  expcn  18953  iirevcn  19006  iihalf2  19009  icchmeo  19017  icopnfcnv  19018  icopnfhmeo  19019  iccpnfhmeo  19021  xrhmeo  19022  icccvx  19026  evth  19035  lebnumii  19042  htpycom  19052  reparphti  19073  pcoass  19100  pcorevcl  19101  pcorevlem  19102  pcorev2  19104  pi1xfrcnv  19133  pjthlem1  19389  ovolunlem1a  19443  ovolunlem1  19444  ovolicc2lem4  19467  uniioombllem3  19528  uniioombllem4  19529  dyadovol  19536  opnmbllem  19544  vitalilem4  19554  vitalilem5  19555  vitali  19556  mbfi1fseqlem6  19661  iblitg  19709  iblcnlem1  19728  itgcnlem  19730  bddibl  19780  dvid  19855  dvnadd  19866  dvexp  19890  dvexp2  19891  dvmptid  19894  dvcnvlem  19911  dvexp3  19913  dveflem  19914  dvef  19915  dvsincos  19916  dvlipcn  19929  dvivthlem1  19943  lhop2  19950  dvcvx  19955  dvfsumle  19956  dvfsumabs  19958  dvfsumlem1  19961  dvfsumlem2  19962  degltp1le  20047  ply1divex  20110  fta1glem1  20139  plyaddlem1  20183  plymullem1  20184  coeidp  20232  dgrid  20233  dgrsub  20241  dgrcolem1  20242  dgrcolem2  20243  dvply1  20252  dvply2g  20253  plydivlem1  20261  plyremlem  20272  fta1lem  20275  vieta1lem1  20278  vieta1lem2  20279  qaa  20291  iaa  20293  aalioulem3  20302  geolim3  20307  aaliou3lem2  20311  aaliou3lem8  20313  aaliou3lem7  20317  taylply2  20335  dvtaylp  20337  dvntaylp  20338  taylthlem1  20340  taylthlem2  20341  dvradcnv  20388  pserdvlem2  20395  pserdv2  20397  abelthlem1  20398  abelthlem2  20399  abelthlem6  20403  abelthlem7  20405  abelth  20408  reeff1olem  20413  reeff1o  20414  efcvx  20416  sinhalfpilem  20425  eulerid  20433  cos2pi  20435  ef2pi  20436  sincosq3sgn  20459  sincosq4sgn  20460  coseq00topi  20461  tangtx  20464  sincos4thpi  20472  sincos6thpi  20474  pige3  20476  abssinper  20477  coskpi  20479  coseq1  20481  efeq1  20482  tanregt0  20492  logneg2  20561  logdivlti  20566  logcnlem4  20587  dvlog2lem  20594  dvlog2  20595  advlog  20596  advlogexp  20597  logtayllem  20601  logtayl  20602  logtayl2  20604  logccv  20605  cxpval  20606  1cxp  20614  cxpcl  20616  cxpp1  20622  cxpmul2  20631  cxpsqr  20645  dvcxp1  20677  dvcxp2  20678  dvsqr  20679  resqrcn  20684  sqrcn  20685  cxpaddlelem  20686  root1id  20689  root1eq1  20690  root1cj  20691  cxpeq  20692  loglesqr  20693  angneg  20696  ang180lem1  20702  ang180lem2  20703  ang180lem3  20704  ang180lem4  20705  ang180lem5  20706  logrec  20712  isosctrlem1  20713  isosctrlem2  20714  isosctrlem3  20715  affineequiv  20718  affineequiv2  20719  angpieqvdlem  20720  chordthmlem2  20725  chordthmlem3  20726  chordthmlem5  20728  1cubrlem  20732  1cubr  20733  dcubic2  20735  dcubic  20737  mcubic  20738  binom4  20741  dquartlem1  20742  quart1lem  20746  quart1  20747  quartlem1  20748  quart  20752  asinlem  20759  asinlem2  20760  asinlem3a  20761  asinlem3  20762  asinf  20763  atandm2  20768  atandm4  20770  atanf  20771  asinneg  20777  efiasin  20779  sinasin  20780  asinsinlem  20782  asinsin  20783  asin1  20785  acos1  20786  reasinsin  20787  asinbnd  20790  cosasin  20795  atanneg  20798  atancj  20801  efiatan  20803  atanlogaddlem  20804  atanlogadd  20805  atanlogsublem  20806  atanlogsub  20807  efiatan2  20808  2efiatan  20809  tanatan  20810  cosatan  20812  cosatanne0  20813  atantan  20814  atanbndlem  20816  bndatandm  20820  atans2  20822  atansopn  20823  dvatan  20826  atantayl  20828  atantayl2  20829  atantayl3  20830  leibpilem1  20831  leibpilem2  20832  leibpi  20833  log2cnv  20835  log2tlbnd  20836  log2ublem3  20839  log2ub  20840  birthdaylem2  20842  birthday  20844  efrlim  20859  dfef2  20860  cxplim  20861  divsqrsumlem  20869  cvxcl  20874  scvxcvx  20875  logdifbnd  20883  emcllem2  20886  emcllem3  20887  emcllem4  20888  emcllem5  20889  emcllem7  20891  harmonicbnd4  20900  fsumharmonic  20901  wilthlem1  20902  wilthlem2  20903  wilthlem3  20904  ftalem5  20910  basellem2  20915  basellem3  20916  basellem5  20918  basellem6  20919  basellem7  20920  basellem8  20921  basellem9  20922  isnsqf  20969  0sgm  20978  mule1  20982  ppiprm  20985  ppinprm  20986  chtprm  20987  chtnprm  20988  chpp1  20989  mumullem2  21014  sqff1o  21016  musum  21027  muinv  21029  1sgmprm  21034  1sgm2ppw  21035  ppiublem2  21038  ppiub  21039  chtublem  21046  chtub  21047  logfaclbnd  21057  logfacbnd3  21058  logfacrlim  21059  logexprlim  21060  mersenne  21062  perfect1  21063  perfectlem1  21064  perfectlem2  21065  perfect  21066  dchrelbasd  21074  dchr1cl  21086  dchrmulid2  21087  dchrinvcl  21088  dchrfi  21090  dchr1  21092  dchrptlem1  21099  dchrptlem2  21100  dchrsum2  21103  sumdchr2  21105  bcmono  21112  bcp1ctr  21114  bclbnd  21115  bposlem1  21119  bposlem8  21126  bposlem9  21127  lgslem1  21131  lgslem2  21132  lgsfcl2  21137  lgsvalmod  21150  lgsneg  21154  lgsdilem  21157  lgsdir2lem1  21158  lgsdir2lem2  21159  lgsdir2lem3  21160  lgsdir2lem4  21161  lgsdir2lem5  21162  lgsdir2  21163  lgsdir  21165  lgsdi  21167  lgsne0  21168  lgseisenlem1  21184  lgseisenlem2  21185  lgseisenlem4  21187  lgseisen  21188  lgsquadlem1  21189  lgsquadlem2  21190  lgsquad2lem1  21193  lgsquad2  21195  lgsquad3  21196  m1lgs  21197  2sqlem8  21207  2sqlem10  21209  2sqlem11  21210  2sqblem  21212  chtppilimlem2  21219  chtppilim  21220  chebbnd2  21222  chto1lb  21223  chpchtlim  21224  rplogsumlem1  21229  rpvmasumlem  21232  dchrisumlem1  21234  dchrmusumlema  21238  dchrmusum2  21239  dchrvmasum2lem  21241  dchrisum0flblem1  21253  rpvmasum2  21257  dchrisum0re  21258  dchrisum0lem2a  21262  rpvmasum  21271  mudivsum  21275  mulogsumlem  21276  mulogsum  21277  vmalogdivsum2  21283  selberg2lem  21295  logdivbnd  21301  pntrmax  21309  pntrsumo1  21310  pntrsumbnd2  21312  selberg34r  21316  pntrlog2bndlem2  21323  pntrlog2bndlem4  21325  pntrlog2bndlem5  21326  pntrlog2bndlem6  21328  pntpbnd1a  21330  pntpbnd2  21332  pntibndlem2  21336  pntlemd  21339  pntlemc  21340  pntlemg  21343  pntlemr  21347  pntlemf  21350  pntlemk  21351  pntlemo  21352  pntlem3  21354  pnt2  21358  pnt  21359  ostth2lem2  21379  usgraexvlem  21465  cusgrasizeinds  21536  cusgrasize2inds  21537  wlkdvspthlem  21658  fargshiftf1  21675  fargshiftfo  21676  vdgr1b  21726  eupatrl  21741  eupares  21748  eupap1  21749  eupath2lem3  21752  ex-pr  21789  1kp2ke3k  21805  ex-fl  21806  gxsuc  21911  gxnn0add  21913  gxnn0mul  21916  ablomul  21994  mulid  21995  cnrngo  22042  vc2  22085  vc0  22099  vcm  22101  vcnegneg  22104  vcoprne  22109  nvnncan  22195  nvm1  22204  nvpi  22206  nvmtri  22211  nvge0  22214  smcnlem  22244  ipval2lem3  22252  ipval2lem6  22258  ipidsq  22260  lnoadd  22310  ip1ilem  22378  ip1i  22379  ip2i  22380  ipdirilem  22381  ipasslem1  22383  ipasslem2  22384  ipasslem10  22391  minvecolem2  22428  hvsubid  22579  hvaddsubval  22586  hv2times  22614  hvnegdii  22615  hvsubcan  22627  hvsubcan2  22628  hisubcomi  22657  normlem9  22671  normlem7tALT  22672  norm-ii-i  22690  normsubi  22694  polid2i  22710  hhssnv  22815  pjhthlem1  22944  h1de2bi  23107  homulid2  23354  honegneg  23360  ho2times  23373  lnop0  23520  lnopaddi  23525  lnophmlem2  23571  lnfn0i  23596  lnfnaddi  23597  hst1h  23781  sto2i  23791  stadd3i  23802  superpos  23908  addltmulALT  24000  bcm1n  24200  ltesubnnd  24211  qqhval2lem  24414  qqh1  24418  logb1  24452  dya2ub  24669  dya2icoseg  24676  eulerpartlemgs2  24766  ballotlem2  24850  ballotlemfp1  24853  ballotlemfc0  24854  ballotlemfcc  24855  ballotlemic  24868  ballotlem1c  24869  ballotlemsgt1  24872  ballotlemsdom  24873  ballotlemsel1i  24874  ballotlemsi  24876  ballotlemsima  24877  ballotlem1ri  24896  zetacvg  24903  lgamgulmlem2  24918  lgamgulmlem3  24919  lgamgulmlem4  24920  lgamgulmlem5  24921  lgamgulmlem6  24922  lgamgulm2  24924  lgamcvg2  24943  gamcvg  24944  gamcvg2lem  24947  lgam1  24952  gam1  24953  gamfac  24955  subfacp1lem1  24969  subfacp1lem5  24974  subfacp1lem6  24975  subfacval2  24977  subfaclim  24978  subfacval3  24979  m1expevenALT  25009  cvxpcon  25033  cvxscon  25034  rescon  25037  cvmliftlem7  25082  cvmliftlem10  25085  sinccvglem  25213  elfzp1b  25220  relexpadd  25242  sqdivzi  25288  4bc3eq4  25307  halfthird  25309  5recm6rec  25310  divcnvlin  25316  muls1d  25317  prodf1  25323  prodfclim1  25325  prodfrec  25327  ntrivcvg  25329  ntrivcvgtail  25332  prodrblem  25359  fprodcvg  25360  prodmolem2a  25364  zprod  25367  fprodntriv  25372  prod1  25374  prodss  25377  fprodss  25378  fprodser  25379  fprodcl  25382  fproddiv  25389  fprodsplit  25393  fprodm1  25394  fprodp1  25396  iprodgam  25423  risefacval2  25430  fallfacval2  25431  risefaccl  25435  fallfaccl  25436  risefacp1  25449  fallfacp1  25450  risefacfac  25455  fallfacfwd  25456  binomfallfaclem2  25460  binomfallfac  25461  fallfacval4  25463  faclimlem1  25466  faclimlem2  25467  faclimlem3  25468  faclim  25469  iprodfac  25470  faclim2  25471  predfz  25582  brbtwn2  25948  colinearalglem4  25952  axsegconlem1  25960  ax5seglem1  25971  ax5seglem2  25972  ax5seglem3  25974  ax5seglem4  25975  ax5seglem5  25976  ax5seglem7  25978  ax5seglem9  25980  axbtwnid  25982  axpaschlem  25983  axlowdimlem6  25990  axlowdimlem13  25997  axlowdimlem14  25998  axlowdimlem16  26000  axeuclidlem  26005  axeuclid  26006  axcontlem2  26008  axcontlem4  26010  axcontlem7  26013  axcontlem8  26014  bpoly0  26200  bpoly1  26201  bpolycl  26202  bpolysum  26203  bpolydiflem  26204  fsumkthpow  26206  bpoly2  26207  bpoly3  26208  bpoly4  26209  fsumcube  26210  ltflcei  26344  sin2h  26347  cos2h  26348  tan2h  26349  opnmbllem0  26351  mblfinlem2  26353  mblfinlem3  26354  0mbf  26361  dvtan  26366  itg2addnclem2  26368  itg2addnclem3  26369  dvreasin  26401  dvreacos  26402  areacirclem1  26403  areacirclem4  26406  areacirc  26408  fdc  26560  mettrifi  26574  heiborlem4  26634  heiborlem6  26636  bfp  26644  eldioph2lem1  26999  lzenom  27009  rabren3dioph  27055  irrapxlem1  27064  irrapxlem2  27065  pellexlem2  27072  pell1qrge1  27112  pell1qr1  27113  elpell1qr2  27114  pell1qrgaplem  27115  rmspecsqrnq  27148  rmspecfund  27151  rmxy0  27165  rmxm1  27176  rmym1  27177  2nn0ind  27187  jm2.24nn  27203  jm2.17a  27204  jm2.17b  27205  jm2.17c  27206  jm2.24  27207  acongeq  27227  jm2.18  27238  jm2.19lem3  27241  jm2.25  27249  jm2.16nn0  27254  jm2.27c  27257  jm3.1lem1  27267  jm3.1lem2  27268  rngunsnply  27534  flcidc  27535  psgnunilem5  27573  psgnunilem2  27574  psgnunilem4  27576  m1expaddsub  27577  psgnuni  27578  cnmsgnsubg  27590  cnmsgnbas  27591  cnmsgngrp  27592  proot1ex  27676  ofdivrec  27699  lhe4.4ex1a  27702  expgrowthi  27706  expgrowth  27708  refsum2cnlem1  27862  fmul01lt1lem2  27869  m1expeven  27879  clim1fr1  27881  isumneg  27882  climneg  27890  itgsin0pilem1  27898  itgsinexp  27903  stoweidlem1  27904  stoweidlem7  27910  stoweidlem10  27913  stoweidlem11  27914  stoweidlem13  27916  stoweidlem14  27917  stoweidlem17  27920  stoweidlem26  27929  stoweidlem34  27937  stoweidlem38  27941  stoweidlem41  27944  stoweidlem42  27945  stoweidlem45  27948  wallispilem2  27969  wallispilem3  27970  wallispilem4  27971  wallispilem5  27972  wallispi  27973  wallispi2lem1  27974  wallispi2lem2  27975  wallispi2  27976  stirlinglem1  27977  stirlinglem3  27979  stirlinglem4  27980  stirlinglem5  27981  stirlinglem6  27982  stirlinglem7  27983  stirlinglem8  27984  stirlinglem10  27986  stirlinglem11  27987  stirlinglem12  27988  stirlinglem13  27989  stirlinglem15  27991  sigaradd  28010  cnm1cn  28275  kcnktkm1cn  28276  ubmelm1fzo  28314  fzosplitsnm1  28318  ltdifltdiv  28335  modvalp1  28338  wrdlenccats1lenm1  28376  cshwidxm1  28443  cshwidxn  28445  swrdtrcfvl  28463  cshweqrep  28472  cshwssizensame  28487  wlklenfislenpm1  28501  wwlknimp  28533  wlkiswwlk1  28536  wlklniswwlkn2  28546  nbhashuvtx1  28595  frghash2spot  28690  usgreghash2spotv  28693  frgregordn0  28697  sec0  28741  onetansqsecsq  28742  cotsqcscsq  28743  5m4e1  28773  isosctrlem1ALT  29287
  Copyright terms: Public domain W3C validator