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 10589
Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 10565. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 10532 . 2 class 1
2 cc 10529 . 2 class
31, 2wcel 2107 1 wff 1 ∈ ℂ
Colors of variables: wff setvar class
This axiom is referenced by:  0cn  10627  1cnd  10630  1ex  10631  mulid1  10633  mulid2  10634  1re  10635  0re  10637  muladd11  10804  peano2cn  10806  mul02lem2  10811  addid1  10814  cnegex2  10816  peano2cnm  10946  0reALT  10977  ine0  11069  mulm1  11075  0lt1  11156  ixi  11263  muleqadd  11278  reccl  11299  recne0  11305  recid  11306  recid2  11307  div1  11323  1div1e1  11324  diveq1  11325  recdiv  11340  divdiv1  11345  divdiv2  11346  recdiv2  11347  conjmul  11351  eqneg  11354  div2neg  11357  recp1lt1  11532  recreclt  11533  recgt0ii  11540  inelr  11622  ofnegsub  11630  peano5nni  11635  nnsscn  11637  nn1m1nn  11652  nn1suc  11653  nnaddcl  11654  nnmulcl  11655  nnne0  11665  nnsub  11675  1m1e0  11703  2cn  11706  3cn  11712  4cn  11716  5cn  11719  6cn  11722  7cn  11725  8cn  11728  9cn  11731  neg1cn  11745  neg1ne0  11747  negneg1e1  11749  1pneg1e0  11750  1m0e1  11752  0p1e1  11753  1p0e1  11755  2m1e1  11757  3m1e2  11759  4m1e3  11760  5m1e4  11761  6m1e5  11762  7m1e6  11763  8m1e7  11764  9m1e8  11765  2p2e4  11766  1p2e3  11774  1p2e3ALT  11775  3p2e5  11782  3p3e6  11783  4p2e6  11784  4p3e7  11785  4p4e8  11786  5p2e7  11787  5p3e8  11788  5p4e9  11789  6p2e8  11790  6p3e9  11791  7p2e9  11792  1t1e1  11793  3t3e9  11798  neg1mulneg1e1  11844  1mhlfehlf  11850  8th4div3  11851  halfpm6th  11852  addltmul  11867  elnn0nn  11933  elz2  11993  zlem1lt  12028  zltlem1  12029  nnaddm1cl  12033  zextlt  12050  zeo  12062  peano5uzi  12065  numsuc  12106  numltc  12118  numsucc  12132  numaddc  12140  6p5lem  12162  5p5e10  12163  6p4e10  12164  7p3e10  12167  8p2e10  12172  10m1e9  12188  4t3lem  12189  7t4e28  12203  9t11e99  12222  decbin2  12233  halfthird  12235  5recm6rec  12236  uzp1  12273  peano2uzr  12297  uzaddcl  12298  rebtwnz  12341  qbtwnre  12587  iccf1o  12877  fz01en  12930  fztp  12958  fzsuc2  12960  fztpval  12964  fseq1m1p1  12977  elfzp1b  12979  fz0to4untppr  13005  predfz  13027  fzoss2  13060  fzval3  13101  fzosplitsnm1  13107  fzo1to4tp  13120  fldiv4p1lem1div2  13200  ceim1l  13210  fldiv  13223  uzrdgxfr  13330  fzen2  13332  nn0ennn  13342  seqm1  13382  seqshft2  13391  monoord2  13396  sermono  13397  seqf1olem1  13404  seqf1olem2  13405  seqz  13413  ser1const  13421  expcl  13442  m1expcl2  13446  expclzlem  13448  expm1t  13452  1exp  13453  mulexpz  13464  expadd  13466  expaddz  13468  expmul  13469  expubnd  13536  sqrecii  13541  neg1sqe1  13554  irec  13559  i4  13562  binom21  13575  sq01  13581  crreczi  13584  bernneq  13585  bernneq2  13586  nn0opthlem1  13623  facndiv  13643  faclbnd4lem1  13648  faclbnd6  13654  bcnp1n  13669  bcm1k  13670  bcp1nk  13672  bcn2  13674  bcp1m1  13675  bcpasc  13676  hashgadd  13733  hashfz  13783  hashfzo  13785  hashxplem  13789  hashbclem  13805  hashf1  13810  seqcoll  13817  swrds1  14023  swrdlsw  14024  wrdind  14079  wrd2ind  14080  swrds2  14297  relexpaddg  14407  rei  14510  imi  14511  recan  14691  iserex  15008  isercoll2  15020  serf0  15032  iseraltlem2  15034  iseraltlem3  15035  iseralt  15036  sumrblem  15063  fsumm1  15101  fsump1  15106  telfsumo  15152  fsumparts  15156  hashiun  15172  binomlem  15179  binom  15180  binom1p  15181  binom11  15182  binom1dif  15183  bcxmas  15185  isumsplit  15190  isum1p  15191  climcndslem1  15199  supcvg  15206  harmonic  15209  arisum  15210  arisum2  15211  trireciplem  15212  geoserg  15216  geolim  15221  geolim2  15222  georeclim  15223  geo2sum  15224  geo2sum2  15225  geoisum1c  15231  0.999...  15232  geoihalfsum  15233  cvgrat  15234  mertenslem1  15235  mertenslem2  15236  mertens  15237  prodf1  15242  prodfclim1  15244  prodrblem  15278  fprodcvg  15279  prodmolem2a  15283  zprod  15286  fprodntriv  15291  prodss  15296  fprodss  15297  fprodsplit  15315  fprodn0f  15340  risefaccl  15364  fallfaccl  15365  risefacfac  15384  binomfallfac  15390  bpolycl  15401  bpolysum  15402  bpolydiflem  15403  fsumkthpow  15405  bpoly2  15406  bpoly3  15407  bpoly4  15408  fsumcube  15409  esum  15429  ege2le3  15438  efsub  15448  efexp  15449  efzval  15450  eftlub  15457  effsumlt  15459  ef4p  15461  tanval3  15482  efi4p  15485  tan0  15499  efival  15500  tanadd  15515  cos2t  15526  cos2tsin  15527  ef01bndlem  15532  cos1bnd  15535  cos2bnd  15536  demoivreALT  15549  eirrlem  15552  rpnnen2lem3  15564  rpnnen2lem11  15572  ruclem12  15589  3dvds  15675  3dvdsdec  15676  3dvds2dec  15677  odd2np1lem  15684  odd2np1  15685  opoe  15707  omoe  15708  opeo  15709  omeo  15710  n2dvdsm1  15714  m1exp1  15722  flodddiv4  15759  bitsfzo  15779  gcdmultipleOLD  15895  sqgcd  15904  nn0seqcvgd  15909  prmind2  16024  hashdvds  16107  phiprmpw  16108  phiprm  16109  eulerthlem2  16114  iserodd  16167  sumhash  16227  fldivp1  16228  prmpwdvds  16235  pockthlem  16236  pockthi  16238  prmreclem4  16250  prmreclem6  16252  4sqlem11  16286  4sqlem19  16294  vdwapun  16305  vdwapid1  16306  vdwlem3  16314  vdwlem5  16316  vdwlem6  16317  vdwlem8  16319  vdwlem9  16320  vdwnnlem2  16327  ramub1lem1  16357  ramub1lem2  16358  ramcl  16360  prmo1  16368  dec5nprm  16397  decexp2  16406  prmlem0  16434  43prm  16450  83prm  16451  139prm  16452  163prm  16453  317prm  16454  631prm  16455  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  1259prm  16464  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem3  16471  4001lem4  16472  4001prm  16473  gsumsgrpccat  17999  gsumccatOLD  18000  mulgnndir  18201  mulgneg2  18206  m1expaddsub  18562  sylow1lem1  18659  sylow2a  18680  efgsval2  18795  efgsrel  18796  efgsres  18800  cnfld1  20505  zsssubrg  20538  cnmgpid  20542  zringcyg  20573  mulgrhm2  20581  cnmsgnsubg  20656  cnmsgnbas  20657  cnmsgngrp  20658  psgninv  20661  evpmodpmf1o  20675  blcvx  23340  iihalf2  23471  icopnfcnv  23480  iccpnfhmeo  23483  xrhmeo  23484  icccvx  23488  lebnumii  23504  reparphti  23535  pcoass  23562  pcorevlem  23564  pcorev2  23566  pi1xfrcnv  23595  cnstrcvs  23679  cncvs  23683  ncvsm1  23692  pjthlem1  23974  divcncf  23982  ovolunlem1a  24031  ovolunlem1  24032  ovolicc2lem4  24055  uniioombllem3  24120  uniioombllem4  24121  dyadovol  24128  vitalilem4  24146  mbf0  24169  iblcnlem1  24322  itgcnlem  24324  dvid  24449  dvexp  24484  dvexp2  24485  dvexp3  24509  dveflem  24510  dvlipcn  24525  dvcvx  24551  dvfsumle  24552  dvfsumlem1  24557  degltp1le  24601  ply1divex  24664  fta1glem1  24693  plyaddlem1  24737  plymullem1  24738  coeidp  24787  dgrid  24788  dvply1  24807  dvply2g  24808  plyremlem  24827  fta1lem  24830  vieta1lem1  24833  vieta1lem2  24834  qaa  24846  iaa  24848  aalioulem3  24857  geolim3  24862  aaliou3lem2  24866  aaliou3lem7  24872  taylply2  24890  dvradcnv  24943  pserdvlem2  24950  pserdv2  24952  abelthlem1  24953  abelthlem2  24954  abelthlem6  24958  abelthlem7  24960  abelth  24963  reeff1olem  24968  reeff1o  24969  efcvx  24971  sinhalfpilem  24983  eulerid  24994  cos2pi  24996  sincosq3sgn  25020  sincosq4sgn  25021  tangtx  25025  sincos4thpi  25033  sincos6thpi  25035  pigt3  25037  pige3ALT  25039  abssinper  25040  coskpi  25042  coseq1  25044  efeq1  25045  tanregt0  25055  logneg2  25130  logdivlti  25135  logcnlem4  25160  dvlog2lem  25167  dvlog2  25168  advlog  25169  advlogexp  25170  logtayl  25175  logtayl2  25177  logccv  25178  cxpval  25179  1cxp  25187  cxpcl  25189  cxpp1  25195  cxpsqrt  25218  dvsqrt  25255  dvcnsqrt  25257  sqrtcn  25263  cxpaddlelem  25264  root1id  25267  root1cj  25269  logrec  25273  logb1  25279  logbmpt  25298  ang180lem1  25319  ang180lem2  25320  ang180lem3  25321  isosctrlem1  25328  isosctrlem2  25329  1cubrlem  25351  1cubr  25352  mcubic  25357  binom4  25360  dquartlem1  25361  quartlem1  25367  asinlem  25378  asinlem2  25379  asinlem3a  25380  asinlem3  25381  asinf  25382  atandm2  25387  atandm4  25389  atanf  25390  asinneg  25396  efiasin  25398  sinasin  25399  asinsin  25402  asin1  25404  acos1  25405  reasinsin  25406  asinbnd  25409  cosasin  25414  atanneg  25417  atancj  25420  efiatan  25422  atanlogaddlem  25423  atanlogadd  25424  atanlogsublem  25425  atanlogsub  25426  efiatan2  25427  2efiatan  25428  tanatan  25429  cosatan  25431  cosatanne0  25432  atantan  25433  atanbndlem  25435  bndatandm  25439  atans2  25441  dvatan  25445  atantayl  25447  atantayl2  25448  atantayl3  25449  leibpilem1OLD  25451  leibpilem2  25452  leibpi  25453  log2cnv  25455  log2tlbnd  25456  log2ublem3  25459  log2ub  25460  birthdaylem2  25463  birthday  25465  efrlim  25480  dfef2  25481  cvxcl  25495  scvxcvx  25496  emcllem2  25507  emcllem4  25509  emcllem7  25512  harmonicbnd4  25521  fsumharmonic  25522  zetacvg  25525  lgamcvg2  25565  lgam1  25574  gam1  25575  wilthlem1  25578  wilthlem2  25579  wilthlem3  25580  basellem2  25592  basellem5  25595  basellem6  25596  basellem7  25597  basellem8  25598  basellem9  25599  0sgm  25654  mule1  25658  ppiprm  25661  ppinprm  25662  chtprm  25663  chtnprm  25664  chpp1  25665  mumullem2  25690  1sgmprm  25708  1sgm2ppw  25709  ppiub  25713  chtublem  25720  chtub  25721  logfaclbnd  25731  logfacbnd3  25732  logfacrlim  25733  logexprlim  25734  mersenne  25736  perfect1  25737  perfectlem1  25738  perfectlem2  25739  perfect  25740  dchrelbasd  25748  dchrmulid2  25761  dchrfi  25764  dchrsum2  25777  sumdchr2  25779  bcp1ctr  25788  bposlem8  25800  zabsle1  25805  lgslem1  25806  lgslem2  25807  lgsfcl2  25812  lgsvalmod  25825  lgsneg  25830  lgsdilem  25833  lgsdir2lem1  25834  lgsdir2lem2  25835  lgsdir2lem3  25836  lgsdir2lem5  25838  lgsdir2  25839  lgsdir  25841  lgsdi  25843  lgsne0  25844  lgseisenlem1  25884  lgseisenlem2  25885  lgseisen  25888  lgsquadlem1  25889  lgsquadlem2  25890  lgsquad2lem1  25893  lgsquad2  25895  m1lgs  25897  2lgslem3c  25907  2lgsoddprmlem3c  25921  2lgsoddprmlem3d  25922  2sqlem10  25937  2sqlem11  25938  2sqblem  25940  addsqn2reu  25950  addsqrexnreu  25951  addsqnreup  25952  chtppilimlem2  25983  chebbnd2  25986  chto1lb  25987  rplogsumlem1  25993  rpvmasumlem  25996  dchrmusumlema  26002  dchrmusum2  26003  dchrisum0flblem1  26017  rpvmasum2  26021  mudivsum  26039  mulogsum  26041  vmalogdivsum2  26047  selberg2lem  26059  logdivbnd  26065  pntrmax  26073  pntrsumo1  26074  pntrsumbnd2  26076  pntrlog2bndlem5  26090  pntpbnd1a  26094  pntpbnd2  26096  pntibndlem2  26100  pntlemd  26103  pntlemc  26104  pntlemr  26111  brbtwn2  26624  colinearalglem4  26628  ax5seglem1  26647  ax5seglem2  26648  ax5seglem3  26650  ax5seglem5  26652  ax5seglem7  26654  ax5seglem9  26656  axbtwnid  26658  axpaschlem  26659  axlowdimlem13  26673  axlowdimlem14  26674  axlowdimlem16  26676  axeuclidlem  26681  axcontlem2  26684  axcontlem4  26686  axcontlem7  26689  axcontlem8  26690  crctcshwlkn0lem6  27526  clwwlkf1  27761  clwwlknonex2lem2  27820  ex-fl  28159  ex-ind-dvds  28173  vc2OLD  28278  vc0  28284  vcm  28286  nvm1  28375  nvmtri  28381  nvge0  28383  ipval2lem3  28415  ipidsq  28420  lnoadd  28468  ip1ilem  28536  ip1i  28537  ip2i  28538  ipdirilem  28539  ipasslem1  28541  ipasslem2  28542  ipasslem10  28549  minvecolem2  28585  hvsubid  28736  hv2times  28771  hisubcomi  28814  normlem9  28828  normlem7tALT  28829  norm-ii-i  28847  normsubi  28851  hhssnv  28974  pjhthlem1  29101  h1de2bi  29264  homulid2  29510  ho2times  29529  lnop0  29676  lnopaddi  29681  lnophmlem2  29727  lnfn0i  29752  lnfnaddi  29753  hst1h  29937  sto2i  29947  stadd3i  29958  addltmulALT  30156  dpmul4  30523  psgnid  30672  cnmsgn0g  30721  altgnsg  30724  isarchi3  30749  archirngz  30751  ccfldextdgrr  30962  lmatfvlem  30985  qqhval2lem  31127  dya2ub  31433  omssubadd  31463  eulerpartlemgs2  31543  fib5  31568  fib6  31569  ballotlem2  31651  sgnneg  31703  signswch  31736  signlem0  31762  itgexpif  31782  reprlt  31795  breprexp  31809  breprexpnat  31810  hgt750lem2  31828  subfacp1lem5  32334  subfacp1lem6  32335  subfacval2  32337  subfaclim  32338  subfacval3  32339  cvxsconn  32393  resconn  32396  cvmliftlem7  32441  cvmliftlem10  32444  problem4  32814  sinccvglem  32818  sqdivzi  32862  faclimlem1  32878  dnibndlem5  33724  dnibndlem10  33729  ltflcei  34766  sin2h  34768  cos2h  34769  tan2h  34770  poimirlem13  34791  poimirlem16  34794  poimirlem17  34795  poimirlem19  34797  poimirlem20  34798  poimirlem31  34809  mblfinlem2  34816  mblfinlem3  34817  dvtan  34828  itg2addnclem3  34831  dvasin  34864  dvacos  34865  areacirc  34873  fdc  34907  mettrifi  34919  heiborlem4  34979  heiborlem6  34981  sn-1ne2  39042  sqdeccom12  39059  235t711  39061  expgcd  39067  re1m1e0m0  39111  fltnltalem  39158  3cubeslem3l  39167  3cubeslem3r  39168  eldioph2lem1  39241  lzenom  39251  irrapxlem1  39303  rmspecsqrtnq  39387  rmxm1  39415  rmym1  39416  2nn0ind  39426  jm2.24nn  39440  jm2.17a  39441  jm2.17b  39442  jm2.17c  39443  jm2.24  39444  acongeq  39464  jm2.18  39469  jm2.27c  39488  jm3.1lem2  39499  rngunsnply  39657  flcidc  39658  inductionexd  40389  unitadd  40433  hashnzfzclim  40538  ofdivrec  40542  lhe4.4ex1a  40545  expgrowth  40551  dvradcnv2  40563  binomcxplemrat  40566  binomcxplemnotnn0  40572  isosctrlem1ALT  41152  monoord2xrv  41644  dvsinax  42081  dvnprodlem3  42117  itgsin0pilem1  42119  itgsbtaddcnst  42151  stoweidlem13  42183  stoweidlem26  42196  stoweidlem34  42204  stoweidlem38  42208  wallispilem2  42236  wallispilem4  42238  wallispi2lem1  42241  stirlinglem1  42244  stirlinglem5  42248  stirlinglem10  42253  dirkerper  42266  dirkertrigeqlem1  42268  dirkertrigeqlem3  42270  dirkertrigeq  42271  dirkercncflem4  42276  fourierdlem24  42301  sqwvfoura  42398  sqwvfourb  42399  fourierswlem  42400  1t10e1p1e11  43395  fmtnorec3  43561  fmtno5lem4  43569  fmtno5  43570  257prm  43574  fmtno4nprmfac193  43587  m3prm  43605  139prmALT  43610  127prm  43614  m7prm  43615  lighneallem3  43623  proththd  43630  3exp4mod41  43632  41prothprmlem2  43634  perfectALTVlem2  43738  perfectALTV  43739  11t31e341  43748  evengpop3  43814  nnsum4primeseven  43816  nnsum4primesevenALTV  43817  bgoldbtbndlem1  43821  0nodd  43928  altgsumbcALT  44303  exple2lt6  44314  nn0sumshdiglemB  44582  line2ylem  44640  onetansqsecsq  44762  cotsqcscsq  44763  5m4e1  44800
  Copyright terms: Public domain W3C validator