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

Theorem zcnd 10310
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 10309 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9049 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8923   ZZcz 10216
This theorem is referenced by:  uzp1  10453  peano2uzr  10466  uzaddcl  10467  zsupss  10499  rpnnen1lem5  10538  fzm1  11059  fzrevral  11063  fzshftral  11066  fzoss2  11095  fzosubel  11107  fzosubel3  11109  quoremz  11165  intfrac2  11168  intfracq  11169  moddiffl  11188  modmul1  11208  modmul12d  11209  uzrdgxfr  11235  fzen2  11237  seqm1  11269  monoord2  11283  seqf1olem1  11291  seqf1olem2  11292  seqz  11300  expaddzlem  11352  modexp  11443  bcm1k  11535  bcp1nk  11537  bcval5  11538  bcpasc  11541  hashfz  11621  hashfzo  11623  hashbclem  11630  seqcoll  11641  ccatval3  11676  ccatlid  11677  ccatass  11679  swrd0val  11697  swrdid  11701  ccatswrd  11702  spllen  11712  splfv1  11713  splfv2a  11714  swrds1  11716  revccat  11727  revrev  11728  shftuz  11813  seqshft  11829  fzomaxdif  12076  climshftlem  12297  climshft  12299  climshft2  12305  iserex  12379  isercoll2  12391  serf0  12403  iseraltlem2  12405  iseraltlem3  12406  iseralt  12407  sumrblem  12434  fsumm1  12466  fsump1  12469  fsumshftm  12493  fsumrev2  12494  fsumtscopo  12510  fsumparts  12514  binomlem  12537  isumshft  12548  isumsplit  12549  isum1p  12550  arisum  12568  cvgrat  12589  mertenslem1  12590  eirrlem  12732  sqr2irrlem  12776  dvds2ln  12809  dvdsadd2b  12821  fsumdvds  12822  fzocongeq  12832  dvdsexp  12834  dvdsmod  12835  oddm1even  12838  oexpneg  12840  3dvds  12841  divalglem0  12842  divalglem4  12845  divalglem8  12849  divalgb  12853  divalgmod  12855  bitsp1  12872  bitsp1e  12873  bitsfzo  12876  bitsmod  12877  bitsinv1lem  12882  bitsf1  12887  sadaddlem  12907  bitsres  12914  bitsuz  12915  bitsshft  12916  smumullem  12933  modgcd  12965  bezoutlem1  12967  bezoutlem2  12968  bezoutlem3  12969  bezoutlem4  12970  dvdsmulgcd  12983  rplpwr  12985  mulgcddvds  13033  rpexp  13049  qmuldeneqnum  13068  numdensq  13075  qden1elz  13078  hashdvds  13093  phiprm  13095  eulerthlem2  13100  fermltl  13102  prmdiv  13103  prmdiveq  13104  odzdvds  13110  pythagtriplem6  13124  pythagtriplem7  13125  pythagtriplem15  13132  pclem  13141  pcpremul  13146  pceulem  13148  pczpre  13150  pcdiv  13155  pcqmul  13156  pcqdiv  13160  pcexp  13162  pcaddlem  13186  pcadd  13187  fldivp1  13195  pcfac  13197  pcbc  13198  prmpwdvds  13201  prmreclem4  13216  4sqlem5  13239  4sqlem8  13242  4sqlem9  13243  4sqlem10  13244  4sqlem11  13252  4sqlem14  13255  4sqlem16  13257  4sqlem17  13258  vdwapun  13271  vdwnnlem2  13293  prmlem0  13357  mulgsubcl  14833  mulgdirlem  14843  mulgdir  14844  mulgass  14849  mulgsubdir  14850  odnncl  15112  odmulg  15121  odbezout  15123  sylow1lem1  15161  sylow2alem2  15181  efgtlen  15287  efgsres  15299  efgredleme  15304  efgredlemc  15306  odadd1  15392  odadd2  15393  cyggeninv  15422  ablfacrp  15553  pgpfac1lem3  15564  zlpirlem1  16693  zlpirlem3  16695  prmirredlem  16698  zndvds0  16756  znf1o  16757  znunit  16769  tgpmulg  18046  zdis  18720  uniioombllem3  19346  mbfi1fseqlem4  19479  dvexp3  19731  aareccl  20112  aalioulem1  20118  geolim3  20125  aaliou3lem2  20129  aaliou3lem6  20134  ulmshft  20175  dvradcnv  20206  sineq0  20298  efif1olem2  20314  wilthlem1  20720  wilthlem2  20721  basellem3  20734  mumul  20833  musum  20845  musumsum  20846  muinv  20847  ppiub  20857  chtub  20865  logfac2  20870  chpchtsum  20872  dchrptlem1  20917  pcbcctr  20929  bcmono  20930  bposlem5  20941  bposlem6  20942  lgslem1  20949  lgsval2lem  20959  lgsval4a  20971  lgsneg  20972  lgsneg1  20973  lgsmod  20974  lgsdirprm  20982  lgsdir  20983  lgsdilem2  20984  lgsdi  20985  lgsne0  20986  lgsabs1  20987  lgssq  20988  lgssq2  20989  lgsdirnn0  20992  lgsdinn0  20993  lgsqrlem1  20994  lgseisenlem1  21002  lgseisenlem2  21003  lgseisenlem3  21004  lgseisenlem4  21005  lgsquadlem1  21007  lgsquad2lem1  21011  lgsquad3  21014  2sqlem3  21019  2sqlem4  21020  2sqlem8a  21024  2sqlem8  21025  2sqlem11  21028  2sqblem  21030  dchrisumlem1  21052  dchrmusum2  21057  dchrvmasumlem1  21058  dchrvmasum2lem  21059  mudivsum  21093  mulogsum  21095  mulog2sumlem2  21098  selberglem1  21108  selberglem3  21110  selberg  21111  pntpbnd2  21150  pntlemf  21168  padicabvcxp  21195  wlkdvspthlem  21457  fargshiftf1  21474  fargshiftfo  21475  eupatrl  21540  gxmodid  21717  fzspl  23987  bcm1n  23989  numdenneg  24000  divnumden2  24001  ltesubnnd  24002  zzsmulg  24083  zrhnm  24156  qqhval2lem  24166  qqhghm  24173  qqhrhm  24174  qqhnm  24175  ballotlemfc0  24531  ballotlemfcc  24532  ballotlemic  24545  ballotlem1c  24546  ballotlemsgt1  24549  ballotlemsdom  24550  ballotlemsel1i  24551  ballotlemsf1o  24552  ballotlemsima  24554  ballotlemfrceq  24567  ballotlemfrcn0  24568  ballotlem1ri  24573  igamz  24613  divcnvlin  24993  ntrivcvg  25006  ntrivcvgtail  25009  prodrblem  25036  fprodser  25056  fprodm1  25071  fprodp1  25073  fprodshft  25081  fprodrev  25082  fallfacfwd  25121  predfz  25229  axlowdimlem14  25610  axlowdimlem16  25612  fsumkthpow  25818  ltflcei  25952  fdc  26142  mettrifi  26156  caushft  26160  cntotbnd  26198  mzpsubmpt  26493  lzenom  26521  diophun  26525  eqrabdioph  26529  irrapxlem2  26579  irrapxlem3  26580  pellexlem6  26590  pell1234qrreccl  26610  pellfund14  26654  rmspecsqrnq  26662  rmxyneg  26676  rmxyadd  26677  rmxp1  26688  rmxm1  26690  rmym1  26691  rmxluc  26692  rmyluc  26693  rmyluc2  26694  rmxdbl  26695  rmydbl  26696  jm2.17a  26718  congadd  26724  congsub  26728  congabseq  26732  acongrep  26738  acongeq  26741  jm2.18  26752  jm2.19lem1  26753  jm2.19lem2  26754  jm2.19lem3  26755  jm2.22  26759  jm2.23  26760  jm2.20nn  26761  jm2.25  26763  jm2.26lem3  26765  jm2.27c  26771  psgnunilem5  27088  psgnunilem2  27089  psgnunilem4  27091  m1expaddsub  27092  psgnuni  27093  hashgcdlem  27187  fmul01lt1lem2  27385  clim1fr1  27397  stoweidlem11  27430  stoweidlem26  27445  wallispilem5  27488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-resscn 8982
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rex 2657  df-rab 2660  df-v 2903  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-iota 5360  df-fv 5404  df-ov 6025  df-neg 9228  df-z 10217
  Copyright terms: Public domain W3C validator