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

Theorem zcnd 11030
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 11029 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9658 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   CCcc 9526   ZZcz 10926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-resscn 9585
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299  df-neg 9852  df-z 10927
This theorem is referenced by:  zsupss  11242  rpnnen1lem5  11283  fzm1  11861  fzrevral  11866  fzshftral  11869  nn0disj  11894  predfz  11901  fzoss2  11933  fzo0addelr  11955  fzosubel  11959  fzosubel3  11961  fzocatel  11964  fzosplitsnm1  11974  quoremz  12068  intfrac2  12071  intfracq  12072  flpmodeq  12087  moddiffl  12094  modmul1  12129  modmul12d  12130  uzrdgxfr  12166  fzen2  12168  monoord2  12230  seqf1olem1  12238  seqf1olem2  12239  seqz  12247  expaddzlem  12301  modexp  12393  bcm1k  12486  bcp1nk  12488  bcval5  12489  bcpasc  12492  hashfz  12583  hashfzo  12585  hashbclem  12599  seqcoll  12610  ccatval3  12700  ccatlid  12706  ccatass  12708  swrd0val  12751  swrdid  12758  swrd0fv  12769  swrdfv2  12776  swrds1  12781  ccatswrd  12786  swrdswrd0  12792  spllen  12835  splfv1  12836  splfv2a  12837  revccat  12845  revrev  12846  cshwidxmod  12879  cshwidxm1  12882  cshweqrep  12894  2cshwcshw  12898  seqshft  13116  fzomaxdif  13374  climshft2  13613  iserex  13687  isercoll2  13699  serf0  13714  iseraltlem2  13716  iseraltlem3  13717  iseralt  13718  sumrblem  13744  fsumm1  13779  fsumsplitsnun  13783  fsump1  13784  fsumshftm  13809  fsumrev2  13810  telfsumo  13829  fsumparts  13833  binomlem  13854  isumshft  13864  isumsplit  13865  isum1p  13866  arisum  13885  cvgrat  13906  mertenslem1  13907  ntrivcvg  13920  ntrivcvgtail  13923  prodrblem  13950  fprodser  13970  fprodm1  13988  fprodp1  13990  fprodrev  13998  fallfacval3  14032  fallfacfwd  14056  0fallfac  14057  binomfallfaclem2  14060  fallfacval4  14063  fsumkthpow  14076  eirrlem  14223  sqr2irrlem  14267  dvds2ln  14300  dvdsadd2b  14314  fsumdvds  14315  fzocongeq  14326  dvdsexp  14328  dvdsmod  14329  odd2np1  14332  oddm1even  14333  oexpneg  14335  3dvds  14336  divalglem0  14338  divalglem4  14341  divalglem8  14345  divalgb  14349  divalgmod  14351  bitsp1  14368  bitsfzo  14372  bitsmod  14373  bitsinv1lem  14378  bitsf1  14383  sadaddlem  14403  bitsres  14410  bitsuz  14411  bitsshft  14412  smumullem  14429  modgcd  14463  bezoutlem1  14466  bezoutlem2  14467  bezoutlem3  14468  bezoutlem4  14469  dvdsmulgcd  14482  rplpwr  14484  lcmid  14534  absprodnn  14548  mulgcddvds  14621  rpexp  14632  qmuldeneqnum  14656  numdensq  14663  qden1elz  14666  hashdvds  14681  phiprm  14683  eulerthlem2  14688  fermltl  14690  prmdiv  14691  prmdiveq  14692  odzdvds  14698  vfermltlALT  14705  modprm0  14708  modprmn0modprm0  14710  pythagtriplem6  14723  pythagtriplem7  14724  pythagtriplem15  14731  pcpremul  14745  pceulem  14747  pczpre  14749  pcdiv  14754  pcqmul  14755  pcqdiv  14759  pcexp  14761  pcaddlem  14785  pcadd  14786  fldivp1  14794  pcfac  14796  pcbc  14797  prmpwdvds  14800  prmreclem4  14815  4sqlem5  14838  4sqlem8  14841  4sqlem9  14842  4sqlem10  14843  4sqlem11  14851  4sqlem14OLD  14854  4sqlem16OLD  14856  4sqlem17OLD  14857  4sqlem14  14860  4sqlem16  14862  4sqlem17  14863  vdwapun  14876  vdwnnlem2  14898  prmop1  14948  prmdvdsprmo  14952  prmdvdsprmorOLD  14967  prmgaplem7  14979  prmlem0  15029  mulgsubcl  16716  mulgdirlem  16726  mulgdir  16727  mulgass  16732  mulgsubdir  16733  psgnunilem5  17079  psgnunilem2  17080  psgnunilem4  17082  m1expaddsub  17083  psgnuni  17084  odnncl  17129  odmulg  17138  odbezout  17140  sylow1lem1  17178  sylow2alem2  17198  efgsres  17316  efgredleme  17321  efgredlemc  17323  odadd1  17414  odadd2  17415  cyggeninv  17446  gsummptshft  17497  ablfacrp  17627  pgpfac1lem3  17638  srgbinomlem3  17703  srgbinomlem4  17704  zringmulg  18974  zringlpirlem1  18980  zringlpirlem3  18982  prmirredlem  18988  zndvds0  19045  znf1o  19046  znunit  19058  cayhamlem1  19814  tgpmulg  21032  zdis  21738  uniioombllem3  22417  mbfi1fseqlem4  22550  dvexp3  22804  aareccl  23144  aalioulem1  23150  geolim3  23157  aaliou3lem2  23161  aaliou3lem6  23166  ulmshft  23207  sineq0  23338  efif1olem2  23354  igamz  23835  wilthlem1  23855  wilthlem2  23856  basellem3  23869  mumul  23968  musum  23980  musumsum  23981  muinv  23982  ppiub  23992  chtub  24000  logfac2  24005  chpchtsum  24007  dchrptlem1  24052  pcbcctr  24064  bcmono  24065  bposlem5  24076  bposlem6  24077  lgslem1  24084  lgsval2lem  24094  lgsval4a  24106  lgsneg  24107  lgsneg1  24108  lgsmod  24109  lgsdirprm  24117  lgsdir  24118  lgsdilem2  24119  lgsdi  24120  lgsne0  24121  lgsabs1  24122  lgssq  24123  lgssq2  24124  lgsdirnn0  24127  lgsdinn0  24128  lgsqrlem1  24129  lgseisenlem1  24137  lgseisenlem2  24138  lgseisenlem3  24139  lgseisenlem4  24140  lgsquadlem1  24142  lgsquad2lem1  24146  lgsquad3  24149  2sqlem3  24154  2sqlem4  24155  2sqlem8a  24159  2sqlem8  24160  2sqlem11  24163  2sqblem  24165  dchrisumlem1  24187  dchrmusum2  24192  dchrvmasumlem1  24193  dchrvmasum2lem  24194  mudivsum  24228  mulogsum  24230  mulog2sumlem2  24233  selberglem1  24243  selberglem3  24245  selberg  24246  pntpbnd2  24285  pntlemf  24303  padicabvcxp  24330  axlowdimlem14  24828  axlowdimlem16  24830  wlkdvspthlem  25179  fargshiftf1  25207  fargshiftfo  25208  clwwisshclww  25377  eupatrl  25538  gxmodid  25849  znsqcld  28163  fzspl  28201  bcm1n  28204  numdenneg  28215  divnumden2  28216  ltesubnnd  28220  2sqn0  28242  2sqmod  28244  archiabllem1  28345  archiabllem2c  28347  zrhnm  28609  cnzh  28610  rezh  28611  qqhval2lem  28621  qqhghm  28628  qqhrhm  28629  qqhnm  28630  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemic  29162  ballotlem1c  29163  ballotlemsgt1  29166  ballotlemsdom  29167  ballotlemsel1i  29168  ballotlemsf1o  29169  ballotlemsima  29171  ballotlemfrceq  29184  ballotlemfrcn0  29185  ballotlem1ri  29190  signsplypnf  29224  divcnvlin  30151  fwddifnp1  30714  ltflcei  31637  poimirlem1  31645  poimirlem2  31646  poimirlem7  31651  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem24  31668  poimirlem31  31675  poimirlem32  31676  fdc  31778  mettrifi  31790  caushft  31794  cntotbnd  31832  mzpsubmpt  35294  lzenom  35321  diophun  35325  eqrabdioph  35329  irrapxlem2  35377  irrapxlem3  35378  pellexlem6  35388  pell1234qrreccl  35410  pellfund14  35456  rmxyneg  35478  rmxyadd  35479  rmxp1  35490  rmxm1  35492  rmym1  35493  rmxluc  35494  rmyluc  35495  rmyluc2  35496  rmxdbl  35497  rmydbl  35498  congadd  35526  congsub  35530  congabseq  35534  acongrep  35540  acongeq  35543  jm2.18  35553  jm2.19lem1  35554  jm2.19lem2  35555  jm2.19lem3  35556  jm2.22  35560  jm2.23  35561  jm2.20nn  35562  jm2.25  35564  jm2.26lem3  35566  jm2.27c  35572  hashgcdlem  35777  nzss  36307  hashnzfz  36310  hashnzfz2  36311  hashnzfzclim  36312  uzmptshftfval  36336  sineq0ALT  36978  fzisoeu  37131  fperiodmul  37135  fmul01lt1lem2  37239  sumnnodd  37286  dvdsn1add  37387  dvnmul  37391  dvnprodlem1  37394  stoweidlem11  37444  stoweidlem26  37459  dirkertrigeqlem1  37533  dirkertrigeqlem2  37534  dirkertrigeqlem3  37535  dirkertrigeq  37536  dirkeritg  37537  fourierdlem26  37568  fourierdlem48  37590  fourierdlem49  37591  fourierdlem79  37621  fourierdlem91  37633  fourierdlem103  37645  fourierdlem104  37646  fouriersw  37667  etransclem1  37671  etransclem4  37674  etransclem8  37678  etransclem9  37679  etransclem15  37685  etransclem17  37687  etransclem18  37688  etransclem20  37690  etransclem21  37691  etransclem22  37692  etransclem23  37693  etransclem24  37694  etransclem25  37695  etransclem35  37705  etransclem38  37708  etransclem41  37711  etransclem44  37714  etransclem45  37715  etransclem46  37716  etransclem47  37717  etransclem48  37718  mod2eq1n2dvds  38128  elmod2OLD  38129  iccpartgtprec  38137  zob  38166  dfodd6  38170  onego  38179  m1expoddALTV  38181  zofldiv2ALTV  38194  oddflALTV  38195  oexpnegALTV  38209  omoeALTV  38217  omeoALTV  38218  epoo  38233  emoo  38234  epee  38235  emee  38236  evensumeven  38237  bgoldbst  38282  sgoldbaltlem2  38284  nnsum3primesprm  38288  nnsum4primesodd  38294  nnsum4primesoddALTV  38295  nnsum4primeseven  38298  nnsum4primesevenALTV  38299  bgoldbtbndlem2  38304  bgoldbtbndlem4  38306  bgoldbtbnd  38307  modexp2m1d  38315  pfxfv  38343  ccatpfx  38353  pfxccatin12lem2  38368  2elfz2melfz  38420  fsumsplitsndif  38429  2zrngamnd  38712  2zrngacmnd  38713  2zrngagrp  38714  2zrngALT  38719  2zrngnmlid  38720  2zrngnmlid2  38722  ztprmneprm  38901  altgsumbcALT  38907  fldivmod  39095  m1modmmod  39098  zofldiv2  39112  fllogbd  39145  nnpw2blen  39165  blen1b  39173  blennngt2o2  39177  blennn0e2  39179  dig2nn1st  39190  dignn0flhalflem1  39200
  Copyright terms: Public domain W3C validator