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

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

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 9793 . 2 class 1
2 cc 9790 . 2 class
31, 2wcel 1976 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  9888  1ex  9891  mulid1  9893  mulid2  9894  1re  9895  1cnd  9912  muladd11  10057  peano2cn  10059  mul02lem2  10064  addid1  10067  cnegex2  10069  peano2cnm  10198  0reALT  10229  ine0  10316  mulm1  10322  0lt1  10401  ixi  10507  muleqadd  10522  reccl  10543  recne0  10549  recid  10550  recid2  10551  div1  10567  1div1e1  10568  diveq1  10569  recdiv  10582  divdiv1  10587  divdiv2  10588  recdiv2  10589  conjmul  10593  eqneg  10596  div2neg  10599  recp1lt1  10772  recreclt  10773  recgt0ii  10780  inelr  10859  ofnegsub  10867  peano5nni  10872  nn1m1nn  10889  nn1suc  10890  nnaddcl  10891  nnmulcl  10892  nnsub  10908  1m1e0  10938  neg1cn  10973  neg1ne0  10975  negneg1e1  10977  1pneg1e0  10978  1m0e1  10980  0p1e1  10981  1p0e1  10982  2m1e1  10984  3m1e2  10986  4m1e3  10987  5m1e4  10988  6m1e5  10989  7m1e6  10990  8m1e7  10991  9m1e8  10992  2p2e4  10993  1p2e3  11001  3p2e5  11009  3p3e6  11010  4p2e6  11011  4p3e7  11012  4p4e8  11013  5p2e7  11014  5p3e8  11015  5p4e9  11016  5p5e10OLD  11017  6p2e8  11018  6p3e9  11019  6p4e10OLD  11020  7p2e9  11021  7p3e10OLD  11022  8p2e10OLD  11023  1t1e1  11024  3t3e9  11029  neg1mulneg1e1  11094  1mhlfehlf  11100  8th4div3  11101  halfpm6th  11102  addltmul  11117  elnn0nn  11184  elz2  11229  zlem1lt  11264  zltlem1  11265  nnaddm1cl  11269  zextlt  11285  zeo  11297  peano5uzi  11300  numsuc  11345  numltc  11362  numsucc  11383  numaddc  11395  6p5lem  11429  5p5e10  11430  6p4e10  11432  7p3e10  11437  8p2e10  11444  10m1e9  11464  4t3lem  11465  7t4e28  11484  9t11e99  11505  9t11e99OLD  11506  decbin2  11517  halfthird  11519  5recm6rec  11520  uzp1  11555  peano2uzr  11577  uzaddcl  11578  rebtwnz  11621  qbtwnre  11865  iccf1o  12145  fz01en  12197  fztp  12224  fzsuc2  12225  fztpval  12229  fseq1m1p1  12241  elfzp1b  12243  fz0to4untppr  12268  predfz  12290  fzoss2  12322  fzval3  12361  fzosplitsnm1  12366  fzo0to42pr  12379  fzo1to4tp  12380  fzosplitprm1  12400  fldiv4p1lem1div2  12455  ceim1l  12465  fldiv  12478  uzrdgxfr  12585  fzen2  12587  nn0ennn  12597  seqm1  12637  seqshft2  12646  monoord2  12651  sermono  12652  seqf1olem1  12659  seqf1olem2  12660  seqz  12668  ser1const  12676  expcl  12697  m1expcl2  12701  expclzlem  12703  expm1t  12707  1exp  12708  mulexpz  12719  expadd  12721  expaddz  12723  expmul  12724  expubnd  12740  sqrecii  12765  neg1sqe1  12778  irec  12783  i4  12786  binom21  12799  sq01  12805  crreczi  12808  bernneq  12809  bernneq2  12810  nn0opthlem1  12874  facndiv  12894  faclbnd4lem1  12899  faclbnd6  12905  bcnp1n  12920  bcm1k  12921  bcp1nk  12923  bcn2  12925  bcp1m1  12926  bcpasc  12927  4bc3eq4  12934  hashgadd  12981  hashfz  13028  hashfzo  13030  hashxplem  13034  hashbclem  13047  hashf1  13052  seqcoll  13059  swrds1  13251  swrdlsw  13252  wrdind  13276  wrd2ind  13277  swrds2  13481  relexpaddg  13589  rei  13692  imi  13693  recan  13872  iserex  14183  isercoll2  14195  serf0  14207  iseraltlem2  14209  iseraltlem3  14210  iseralt  14211  sumrblem  14237  fsumm1  14272  fsump1  14277  telfsumo  14323  fsumparts  14327  hashiun  14343  binomlem  14348  binom  14349  binom1p  14350  binom11  14351  binom1dif  14352  bcxmas  14354  isumsplit  14359  isum1p  14360  climcndslem1  14368  supcvg  14375  harmonic  14378  arisum  14379  arisum2  14380  trireciplem  14381  geoserg  14385  geolim  14388  geolim2  14389  georeclim  14390  geo2sum  14391  geo2sum2  14392  geoisum1c  14398  0.999...  14399  0.999...OLD  14400  geoihalfsum  14401  cvgrat  14402  mertenslem1  14403  mertenslem2  14404  mertens  14405  prodf1  14410  prodfclim1  14412  prodrblem  14446  fprodcvg  14447  prodmolem2a  14451  zprod  14454  fprodntriv  14459  prodss  14464  fprodss  14465  fprodsplit  14483  fprodn0f  14509  fprodclf  14510  risefaccl  14533  fallfaccl  14534  risefacfac  14553  binomfallfac  14559  bpolycl  14570  bpolysum  14571  bpolydiflem  14572  fsumkthpow  14574  bpoly2  14575  bpoly3  14576  bpoly4  14577  fsumcube  14578  esum  14598  ege2le3  14607  efsub  14617  efexp  14618  efzval  14619  eftlub  14626  effsumlt  14628  ef4p  14630  tanval3  14651  efi4p  14654  tan0  14668  efival  14669  tanadd  14684  cos2t  14695  cos2tsin  14696  ef01bndlem  14701  cos1bnd  14704  cos2bnd  14705  demoivreALT  14718  eirrlem  14719  rpnnen2lem3  14732  rpnnen2lem11  14740  ruclem12  14757  3dvds  14838  3dvdsOLD  14839  3dvdsdec  14840  3dvdsdecOLD  14841  3dvds2dec  14842  3dvds2decOLD  14843  odd2np1lem  14850  odd2np1  14851  opoe  14873  omoe  14874  opeo  14875  omeo  14876  m1exp1  14879  n2dvdsm1  14891  flodddiv4  14923  bitsfzo  14943  gcdmultiple  15055  sqgcd  15064  nn0seqcvgd  15069  prmind2  15184  hashdvds  15266  phiprmpw  15267  phiprm  15268  eulerthlem2  15273  iserodd  15326  sumhash  15386  fldivp1  15387  prmpwdvds  15394  pockthlem  15395  pockthi  15397  prmreclem4  15409  prmreclem6  15411  4sqlem11  15445  4sqlem19  15453  vdwapun  15464  vdwapid1  15465  vdwlem3  15473  vdwlem5  15475  vdwlem6  15476  vdwlem8  15478  vdwlem9  15479  vdwnnlem2  15486  ramub1lem1  15516  ramub1lem2  15517  ramcl  15519  prmo1  15527  dec5nprm  15556  decexp2  15565  prmlem0  15598  43prm  15615  83prm  15616  139prm  15617  163prm  15618  317prm  15619  631prm  15620  prmo4  15621  prmo5  15622  prmo6  15623  1259lem2  15625  1259lem3  15626  1259lem4  15627  1259lem5  15628  1259prm  15629  2503lem1  15630  2503lem2  15631  2503lem3  15632  2503prm  15633  4001lem1  15634  4001lem2  15635  4001lem3  15636  4001lem4  15637  4001prm  15638  gsumccat  17149  mulgnndir  17340  mulgnndirOLD  17341  mulgneg2  17346  m1expaddsub  17689  sylow1lem1  17784  sylow2a  17805  efgsval2  17917  efgsrel  17918  efgsres  17922  cnfld1  19538  zsssubrg  19571  cnmgpid  19575  zringcyg  19603  mulgrhm2  19613  cnmsgnsubg  19689  cnmsgnbas  19690  cnmsgngrp  19691  psgninv  19694  evpmodpmf1o  19708  blcvx  22356  iihalf2  22487  icopnfcnv  22496  iccpnfhmeo  22499  xrhmeo  22500  icccvx  22504  lebnumii  22520  reparphti  22552  pcoass  22579  pcorevlem  22581  pcorev2  22583  pi1xfrcnv  22612  cnstrcvs  22696  cncvs  22700  ncvsm1  22706  pjthlem1  22960  ovolunlem1a  23015  ovolunlem1  23016  ovolicc2lem4  23039  uniioombllem3  23103  uniioombllem4  23104  dyadovol  23111  vitalilem4  23130  iblitg  23285  iblcnlem1  23304  itgcnlem  23306  dvid  23431  dvexp  23466  dvexp2  23467  dvexp3  23489  dveflem  23490  dvef  23491  dvlipcn  23505  dvcvx  23531  dvfsumle  23532  dvfsumlem1  23537  degltp1le  23581  ply1divex  23644  fta1glem1  23673  plyaddlem1  23717  plymullem1  23718  coeidp  23767  dgrid  23768  dvply1  23787  dvply2g  23788  plyremlem  23807  fta1lem  23810  vieta1lem1  23813  vieta1lem2  23814  qaa  23826  iaa  23828  aalioulem3  23837  geolim3  23842  aaliou3lem2  23846  aaliou3lem7  23852  taylply2  23870  dvradcnv  23923  pserdvlem2  23930  pserdv2  23932  abelthlem1  23933  abelthlem2  23934  abelthlem6  23938  abelthlem7  23940  abelth  23943  reeff1olem  23948  reeff1o  23949  efcvx  23951  sinhalfpilem  23963  eulerid  23974  cos2pi  23976  sincosq3sgn  24000  sincosq4sgn  24001  tangtx  24005  sincos4thpi  24013  sincos6thpi  24015  pige3  24017  abssinper  24018  coskpi  24020  coseq1  24022  efeq1  24023  tanregt0  24033  logneg2  24109  logdivlti  24114  logcnlem4  24135  dvlog2lem  24142  dvlog2  24143  advlog  24144  advlogexp  24145  logtayl  24150  logtayl2  24152  logccv  24153  cxpval  24154  1cxp  24162  cxpcl  24164  cxpp1  24170  cxpsqrt  24193  dvsqrt  24227  dvcnsqrt  24229  sqrtcn  24235  cxpaddlelem  24236  root1id  24239  root1cj  24241  logrec  24245  logb1  24251  logbmpt  24270  ang180lem1  24283  ang180lem2  24284  ang180lem3  24285  isosctrlem1  24292  isosctrlem2  24293  1cubrlem  24312  1cubr  24313  mcubic  24318  binom4  24321  dquartlem1  24322  quartlem1  24328  asinlem  24339  asinlem2  24340  asinlem3a  24341  asinlem3  24342  asinf  24343  atandm2  24348  atandm4  24350  atanf  24351  asinneg  24357  efiasin  24359  sinasin  24360  asinsin  24363  asin1  24365  acos1  24366  reasinsin  24367  asinbnd  24370  cosasin  24375  atanneg  24378  atancj  24381  efiatan  24383  atanlogaddlem  24384  atanlogadd  24385  atanlogsublem  24386  atanlogsub  24387  efiatan2  24388  2efiatan  24389  tanatan  24390  cosatan  24392  cosatanne0  24393  atantan  24394  atanbndlem  24396  bndatandm  24400  atans2  24402  dvatan  24406  atantayl  24408  atantayl2  24409  atantayl3  24410  leibpilem1  24411  leibpilem2  24412  leibpi  24413  log2cnv  24415  log2tlbnd  24416  log2ublem3  24419  log2ub  24420  birthdaylem2  24423  birthday  24425  efrlim  24440  dfef2  24441  cvxcl  24455  scvxcvx  24456  emcllem2  24467  emcllem4  24469  emcllem7  24472  harmonicbnd4  24481  fsumharmonic  24482  zetacvg  24485  lgamcvg2  24525  lgam1  24534  gam1  24535  wilthlem1  24538  wilthlem2  24539  wilthlem3  24540  basellem2  24552  basellem5  24555  basellem6  24556  basellem7  24557  basellem8  24558  basellem9  24559  0sgm  24614  mule1  24618  ppiprm  24621  ppinprm  24622  chtprm  24623  chtnprm  24624  chpp1  24625  mumullem2  24650  1sgmprm  24668  1sgm2ppw  24669  ppiublem2  24672  ppiub  24673  chtublem  24680  chtub  24681  logfaclbnd  24691  logfacbnd3  24692  logfacrlim  24693  logexprlim  24694  mersenne  24696  perfect1  24697  perfectlem1  24698  perfectlem2  24699  perfect  24700  dchrelbasd  24708  dchrmulid2  24721  dchrfi  24724  dchrsum2  24737  sumdchr2  24739  bcp1ctr  24748  bposlem8  24760  zabsle1  24765  lgslem1  24766  lgslem2  24767  lgsfcl2  24772  lgsvalmod  24785  lgsneg  24790  lgsdilem  24793  lgsdir2lem1  24794  lgsdir2lem2  24795  lgsdir2lem3  24796  lgsdir2lem5  24798  lgsdir2  24799  lgsdir  24801  lgsdi  24803  lgsne0  24804  lgseisenlem1  24844  lgseisenlem2  24845  lgseisen  24848  lgsquadlem1  24849  lgsquadlem2  24850  lgsquad2lem1  24853  lgsquad2  24855  m1lgs  24857  2lgslem3c  24867  2lgsoddprmlem3b  24880  2lgsoddprmlem3c  24881  2lgsoddprmlem3d  24882  2sqlem10  24897  2sqlem11  24898  2sqblem  24900  chtppilimlem2  24907  chebbnd2  24910  chto1lb  24911  rplogsumlem1  24917  rpvmasumlem  24920  dchrmusumlema  24926  dchrmusum2  24927  dchrisum0flblem1  24941  rpvmasum2  24945  mudivsum  24963  mulogsum  24965  vmalogdivsum2  24971  selberg2lem  24983  logdivbnd  24989  pntrmax  24997  pntrsumo1  24998  pntrsumbnd2  25000  pntrlog2bndlem5  25014  pntpbnd1a  25018  pntpbnd2  25020  pntibndlem2  25024  pntlemd  25027  pntlemc  25028  pntlemr  25035  brbtwn2  25530  colinearalglem4  25534  ax5seglem1  25553  ax5seglem2  25554  ax5seglem3  25556  ax5seglem5  25558  ax5seglem7  25560  ax5seglem9  25562  axbtwnid  25564  axpaschlem  25565  axlowdimlem13  25579  axlowdimlem14  25580  axlowdimlem16  25582  axeuclidlem  25587  axcontlem2  25590  axcontlem4  25592  axcontlem7  25595  axcontlem8  25596  wlklenvm1  25853  wlkiswwlk1  26011  wwlknext  26045  clwwlkf1  26117  wwlkext2clwwlk  26124  eupares  26295  eupap1  26296  eupath2lem3  26299  frghash2spot  26383  usgreghash2spotv  26386  extwwlkfablem2  26398  numclwwlkovf2ex  26406  numclwwlk6  26433  ex-fl  26489  ex-ind-dvds  26503  vc2OLD  26600  vc0  26606  vcm  26608  nvm1  26697  nvmtri  26703  nvge0  26705  ipval2lem3  26737  ipidsq  26742  lnoadd  26790  ip1ilem  26858  ip1i  26859  ip2i  26860  ipdirilem  26861  ipasslem1  26863  ipasslem2  26864  ipasslem10  26871  minvecolem2  26908  hvsubid  27060  hv2times  27095  hisubcomi  27138  normlem9  27152  normlem7tALT  27153  norm-ii-i  27171  normsubi  27175  hhssnv  27298  pjhthlem1  27427  h1de2bi  27590  homulid2  27836  ho2times  27855  lnop0  28002  lnopaddi  28007  lnophmlem2  28053  lnfn0i  28078  lnfnaddi  28079  hst1h  28263  sto2i  28273  stadd3i  28284  addltmulALT  28482  isarchi3  28865  archirngz  28867  psgnid  28971  lmatfvlem  29002  qqhval2lem  29146  dya2ub  29452  omssubadd  29482  eulerpartlemgs2  29562  fib5  29587  fib6  29588  ballotlem2  29670  sgnneg  29722  signswch  29757  signlem0  29783  subfacp1lem5  30213  subfacp1lem6  30214  subfacval2  30216  subfaclim  30217  subfacval3  30218  cvxscon  30272  rescon  30275  cvmliftlem7  30320  cvmliftlem10  30323  problem4  30609  sinccvglem  30613  sqdivzi  30656  faclimlem1  30675  dnibndlem5  31435  dnibndlem10  31440  ltflcei  32350  sin2h  32352  cos2h  32353  tan2h  32354  pigt3  32355  poimirlem13  32375  poimirlem16  32378  poimirlem17  32379  poimirlem19  32381  poimirlem20  32382  poimirlem31  32393  mblfinlem2  32400  mblfinlem3  32401  0mbf  32408  dvtan  32413  itg2addnclem3  32416  dvasin  32449  dvacos  32450  areacirc  32458  fdc  32494  mettrifi  32506  heiborlem4  32566  heiborlem6  32568  eldioph2lem1  36124  lzenom  36134  irrapxlem1  36187  rmspecsqrtnq  36271  rmspecsqrtnqOLD  36272  rmxm1  36300  rmym1  36301  2nn0ind  36311  jm2.24nn  36327  jm2.17a  36328  jm2.17b  36329  jm2.17c  36330  jm2.24  36331  acongeq  36351  jm2.18  36356  jm2.27c  36375  jm3.1lem2  36386  rngunsnply  36545  flcidc  36546  inductionexd  37256  unitadd  37303  hashnzfzclim  37326  ofdivrec  37330  lhe4.4ex1a  37333  expgrowth  37339  dvradcnv2  37351  binomcxplemrat  37354  binomcxplemnotnn0  37360  isosctrlem1ALT  37975  divcncf  38552  dvsinax  38584  dvnprodlem3  38621  itgsin0pilem1  38624  itgsbtaddcnst  38657  stoweidlem13  38689  stoweidlem26  38702  stoweidlem34  38710  stoweidlem38  38714  wallispilem2  38742  wallispilem4  38744  wallispi2lem1  38747  stirlinglem1  38750  stirlinglem5  38754  stirlinglem10  38759  dirkerper  38772  dirkertrigeqlem1  38774  dirkertrigeqlem3  38776  dirkertrigeq  38777  dirkercncflem4  38782  fourierdlem24  38807  sqwvfoura  38904  sqwvfourb  38905  fourierswlem  38906  1t10e1p1e11  39721  1t10e1p1e11OLD  39722  fmtnorec3  39782  fmtno5lem4  39790  fmtno5  39791  257prm  39795  fmtno4nprmfac193  39808  m3prm  39828  139prmALT  39833  127prm  39837  m7prm  39838  lighneallem3  39846  proththd  39853  3exp4mod41  39855  41prothprmlem2  39857  perfectALTVlem2  39949  perfectALTV  39950  evengpop3  39998  nnsum4primeseven  40000  nnsum4primesevenALTV  40001  bgoldbtbndlem1  40005  crctcsh1wlkn0lem6  40999  wwlksnext  41080  clwwlksf1  41205  wwlksext2clwwlk  41212  frgrhash2wsp  41478  fusgreghash2wspv  41480  av-numclwwlkovf2ex  41498  0nodd  41581  altgsumbcALT  41905  exple2lt6  41920  nn0sumshdiglemB  42193  onetansqsecsq  42243  cotsqcscsq  42244  5m4e1  42294
  Copyright terms: Public domain W3C validator