MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zcnd Structured version   Visualization version   Unicode version

Theorem zcnd 11041
Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1  |-  ( ph  ->  A  e.  ZZ )
Assertion
Ref Expression
zcnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem zcnd
StepHypRef Expression
1 zred.1 . . 3  |-  ( ph  ->  A  e.  ZZ )
21zred 11040 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9669 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   CCcc 9537   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-resscn 9596
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293  df-neg 9863  df-z 10938
This theorem is referenced by:  zsupss  11253  rpnnen1lem5  11294  fzm1  11874  fzrevral  11879  fzshftral  11882  nn0disj  11907  predfz  11914  fzoss2  11946  fzo0addelr  11969  fzosubel  11973  fzosubel3  11975  fzocatel  11978  fzosplitsnm1  11988  quoremz  12082  intfrac2  12085  intfracq  12086  flpmodeq  12101  moddiffl  12108  modmul1  12143  modmul12d  12144  uzrdgxfr  12180  fzen2  12182  monoord2  12244  seqf1olem1  12252  seqf1olem2  12253  seqz  12261  expaddzlem  12315  modexp  12407  bcm1k  12500  bcp1nk  12502  bcval5  12503  bcpasc  12506  hashfz  12599  hashfzo  12601  hashbclem  12615  seqcoll  12627  ccatval3  12724  ccatlid  12730  ccatass  12732  swrd0val  12777  swrdid  12784  swrd0fv  12795  swrdfv2  12802  swrds1  12807  ccatswrd  12812  swrdswrd0  12818  spllen  12861  splfv1  12862  splfv2a  12863  revccat  12871  revrev  12872  cshwidxmod  12905  cshwidxm1  12908  cshweqrep  12920  2cshwcshw  12924  seqshft  13148  fzomaxdif  13406  climshft2  13646  iserex  13720  isercoll2  13732  serf0  13747  iseraltlem2  13749  iseraltlem3  13750  iseralt  13751  sumrblem  13777  fsumm1  13812  fsumsplitsnun  13816  fsump1  13817  fsumshftm  13842  fsumrev2  13843  telfsumo  13862  fsumparts  13866  binomlem  13887  isumshft  13897  isumsplit  13898  isum1p  13899  arisum  13918  cvgrat  13939  mertenslem1  13940  ntrivcvg  13953  ntrivcvgtail  13956  prodrblem  13983  fprodser  14003  fprodm1  14021  fprodp1  14023  fprodrev  14031  fallfacval3  14065  fallfacfwd  14089  0fallfac  14090  binomfallfaclem2  14093  fallfacval4  14096  fsumkthpow  14109  eirrlem  14256  sqr2irrlem  14300  dvds2ln  14333  dvdsadd2b  14347  fsumdvds  14348  fzocongeq  14359  dvdsexp  14361  dvdsmod  14362  odd2np1  14365  oddm1even  14366  oexpneg  14368  3dvds  14369  divalglem0  14371  divalglem4  14375  divalglem8  14380  divalgb  14385  divalgmod  14387  bitsp1  14404  bitsfzo  14409  bitsmod  14410  bitsinv1lem  14415  bitsf1  14420  sadaddlem  14440  bitsres  14447  bitsuz  14448  bitsshft  14449  smumullem  14466  modgcd  14500  bezoutlem1  14503  bezoutlem2OLD  14504  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem2  14507  bezoutlem3  14508  bezoutlem4  14509  dvdsmulgcd  14522  rplpwr  14524  lcmid  14574  absprodnn  14588  mulgcddvds  14661  rpexp  14672  qmuldeneqnum  14696  numdensq  14703  qden1elz  14706  hashdvds  14723  phiprm  14725  eulerthlem2  14730  fermltl  14732  prmdiv  14733  prmdiveq  14734  odzdvds  14740  odzdvdsOLD  14746  vfermltlALT  14753  modprm0  14756  modprmn0modprm0  14758  pythagtriplem6  14771  pythagtriplem7  14772  pythagtriplem15  14779  pcpremul  14793  pceulem  14795  pczpre  14797  pcdiv  14802  pcqmul  14803  pcqdiv  14807  pcexp  14809  pcaddlem  14833  pcadd  14834  fldivp1  14842  pcfac  14844  pcbc  14845  prmpwdvds  14848  prmreclem4  14863  4sqlem5  14886  4sqlem8  14889  4sqlem9  14890  4sqlem10  14891  4sqlem11  14899  4sqlem14OLD  14902  4sqlem16OLD  14904  4sqlem17OLD  14905  4sqlem14  14908  4sqlem16  14910  4sqlem17  14911  vdwapun  14924  vdwnnlem2  14946  prmop1  14996  prmdvdsprmo  15000  prmdvdsprmorOLD  15015  prmgaplem7  15027  prmlem0  15077  mulgsubcl  16772  mulgdirlem  16782  mulgdir  16783  mulgass  16788  mulgsubdir  16789  psgnunilem5  17135  psgnunilem2  17136  psgnunilem4  17138  m1expaddsub  17139  psgnuni  17140  odnncl  17194  odmulg  17207  odbezout  17209  sylow1lem1  17250  sylow2alem2  17270  efgsres  17388  efgredleme  17393  efgredlemc  17395  odadd1  17486  odadd2  17487  cyggeninv  17518  gsummptshft  17569  ablfacrp  17699  pgpfac1lem3  17710  srgbinomlem3  17775  srgbinomlem4  17776  zringmulg  19047  zringlpirlem1  19053  zringlpirlem3OLD  19055  zringlpirlem3  19057  prmirredlem  19064  zndvds0  19121  znf1o  19122  znunit  19134  cayhamlem1  19890  tgpmulg  21108  zdis  21834  uniioombllem3  22543  mbfi1fseqlem4  22676  dvexp3  22930  aareccl  23282  aalioulem1  23288  geolim3  23295  aaliou3lem2  23299  aaliou3lem6  23304  ulmshft  23345  sineq0  23476  efif1olem2  23492  igamz  23973  wilthlem1  23993  wilthlem2  23994  basellem3  24009  mumul  24108  musum  24120  musumsum  24121  muinv  24122  ppiub  24132  chtub  24140  logfac2  24145  chpchtsum  24147  dchrptlem1  24192  pcbcctr  24204  bcmono  24205  bposlem5  24216  bposlem6  24217  lgslem1  24224  lgsval2lem  24234  lgsval4a  24246  lgsneg  24247  lgsneg1  24248  lgsmod  24249  lgsdirprm  24257  lgsdir  24258  lgsdilem2  24259  lgsdi  24260  lgsne0  24261  lgsabs1  24262  lgssq  24263  lgssq2  24264  lgsdirnn0  24267  lgsdinn0  24268  lgsqrlem1  24269  lgseisenlem1  24277  lgseisenlem2  24278  lgseisenlem3  24279  lgseisenlem4  24280  lgsquadlem1  24282  lgsquad2lem1  24286  lgsquad3  24289  2sqlem3  24294  2sqlem4  24295  2sqlem8a  24299  2sqlem8  24300  2sqlem11  24303  2sqblem  24305  dchrisumlem1  24327  dchrmusum2  24332  dchrvmasumlem1  24333  dchrvmasum2lem  24334  mudivsum  24368  mulogsum  24370  mulog2sumlem2  24373  selberglem1  24383  selberglem3  24385  selberg  24386  pntpbnd2  24425  pntlemf  24443  padicabvcxp  24470  axlowdimlem14  24985  axlowdimlem16  24987  wlkdvspthlem  25337  fargshiftf1  25365  fargshiftfo  25366  clwwisshclww  25535  eupatrl  25696  gxmodid  26007  znsqcld  28323  fzspl  28368  bcm1n  28371  numdenneg  28380  divnumden2  28381  ltesubnnd  28385  2sqn0  28407  2sqmod  28409  archiabllem1  28510  archiabllem2c  28512  zrhnm  28773  cnzh  28774  rezh  28775  qqhval2lem  28785  qqhghm  28792  qqhrhm  28793  qqhnm  28794  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemic  29339  ballotlem1c  29340  ballotlemsgt1  29343  ballotlemsdom  29344  ballotlemsel1i  29345  ballotlemsf1o  29346  ballotlemsima  29348  ballotlemfrceq  29361  ballotlemfrcn0  29362  ballotlem1ri  29367  ballotlemicOLD  29377  ballotlem1cOLD  29378  ballotlemsgt1OLD  29381  ballotlemsdomOLD  29382  ballotlemsel1iOLD  29383  ballotlemsf1oOLD  29384  ballotlemsimaOLD  29386  ballotlemfrceqOLD  29399  ballotlemfrcn0OLD  29400  ballotlem1riOLD  29405  signsplypnf  29439  divcnvlin  30367  fwddifnp1  30932  ltflcei  31933  poimirlem1  31941  poimirlem2  31942  poimirlem7  31947  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem24  31964  poimirlem31  31971  poimirlem32  31972  fdc  32074  mettrifi  32086  caushft  32090  cntotbnd  32128  mzpsubmpt  35585  lzenom  35612  diophun  35616  eqrabdioph  35620  irrapxlem2  35667  irrapxlem3  35668  pellexlem6  35678  pell1234qrreccl  35700  pellfund14  35746  rmxyneg  35768  rmxyadd  35769  rmxp1  35780  rmxm1  35782  rmym1  35783  rmxluc  35784  rmyluc  35785  rmyluc2  35786  rmxdbl  35787  rmydbl  35788  congadd  35816  congsub  35820  congabseq  35824  acongrep  35830  acongeq  35833  jm2.18  35843  jm2.19lem1  35844  jm2.19lem2  35845  jm2.19lem3  35846  jm2.22  35850  jm2.23  35851  jm2.20nn  35852  jm2.25  35854  jm2.26lem3  35856  jm2.27c  35862  hashgcdlem  36074  nzss  36666  hashnzfz  36669  hashnzfz2  36670  hashnzfzclim  36671  uzmptshftfval  36695  sineq0ALT  37334  fzisoeu  37518  fperiodmul  37522  fmul01lt1lem2  37663  sumnnodd  37710  dvdsn1add  37814  dvnmul  37818  dvnprodlem1  37821  stoweidlem11  37871  stoweidlem26  37886  dirkertrigeqlem1  37960  dirkertrigeqlem2  37961  dirkertrigeqlem3  37962  dirkertrigeq  37963  dirkeritg  37964  fourierdlem26  37995  fourierdlem48  38018  fourierdlem49  38019  fourierdlem79  38049  fourierdlem91  38061  fourierdlem103  38073  fourierdlem104  38074  fouriersw  38095  etransclem1  38100  etransclem4  38103  etransclem8  38107  etransclem9  38108  etransclem15  38114  etransclem17  38116  etransclem18  38117  etransclem20  38119  etransclem21  38120  etransclem22  38121  etransclem23  38122  etransclem24  38123  etransclem25  38124  etransclem35  38134  etransclem38  38137  etransclem41  38140  etransclem44  38143  etransclem45  38144  etransclem46  38145  etransclem47  38146  etransclem48OLD  38147  etransclem48  38148  mod2eq1n2dvds  38725  elmod2OLD  38726  iccpartgtprec  38734  zob  38763  dfodd6  38767  onego  38776  m1expoddALTV  38778  zofldiv2ALTV  38791  oddflALTV  38792  oexpnegALTV  38806  omoeALTV  38814  omeoALTV  38815  epoo  38830  emoo  38831  epee  38832  emee  38833  evensumeven  38834  bgoldbst  38879  sgoldbaltlem2  38881  nnsum3primesprm  38885  nnsum4primesodd  38891  nnsum4primesoddALTV  38892  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  bgoldbtbndlem2  38901  bgoldbtbndlem4  38903  bgoldbtbnd  38904  modexp2m1d  38912  pfxfv  38940  ccatpfx  38950  pfxccatin12lem2  38965  2elfz2melfz  39058  fsumsplitsndif  39092  2zrngamnd  39994  2zrngacmnd  39995  2zrngagrp  39996  2zrngALT  40001  2zrngnmlid  40002  2zrngnmlid2  40004  ztprmneprm  40181  altgsumbcALT  40187  fldivmod  40374  m1modmmod  40377  zofldiv2  40391  fllogbd  40424  nnpw2blen  40444  blen1b  40452  blennngt2o2  40456  blennn0e2  40458  dig2nn1st  40469  dignn0flhalflem1  40479
  Copyright terms: Public domain W3C validator