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

Theorem zcnd 10120
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 10119 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 8863 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   CCcc 8737   ZZcz 10026
This theorem is referenced by:  uzp1  10263  peano2uzr  10276  uzaddcl  10277  zsupss  10309  rpnnen1lem5  10348  fzm1  10864  fzrevral  10868  fzshftral  10871  fzoss2  10899  fzosubel  10910  fzosubel3  10912  quoremz  10961  intfrac2  10964  intfracq  10965  moddiffl  10984  modmul1  11004  modmul12d  11005  uzrdgxfr  11031  fzen2  11033  seqm1  11065  monoord2  11079  seqf1olem1  11087  seqf1olem2  11088  seqz  11096  expaddzlem  11147  modexp  11238  bcm1k  11329  bcp1nk  11331  bcval5  11332  bcpasc  11335  hashfz  11383  hashfzo  11385  hashbclem  11392  seqcoll  11403  ccatval3  11435  ccatlid  11436  ccatass  11438  swrd0val  11456  swrdid  11460  ccatswrd  11461  spllen  11471  splfv1  11472  splfv2a  11473  swrds1  11475  revccat  11486  revrev  11487  shftuz  11566  seqshft  11582  fzomaxdif  11829  climshftlem  12050  climshft  12052  climshft2  12058  iserex  12132  isercoll2  12144  serf0  12155  iseraltlem2  12157  iseraltlem3  12158  iseralt  12159  sumrblem  12186  fsumm1  12218  fsump1  12221  fsumshftm  12245  fsumrev2  12246  fsumtscopo  12262  fsumparts  12266  binomlem  12289  isumshft  12300  isumsplit  12301  isum1p  12302  arisum  12320  cvgrat  12341  mertenslem1  12342  eirrlem  12484  sqr2irrlem  12528  dvds2ln  12561  dvdsadd2b  12573  fsumdvds  12574  fzocongeq  12584  dvdsexp  12586  dvdsmod  12587  oddm1even  12590  oexpneg  12592  3dvds  12593  divalglem0  12594  divalglem4  12597  divalglem8  12601  divalgb  12605  divalgmod  12607  bitsp1e  12625  bitsfzo  12628  bitsmod  12629  bitsinv1lem  12634  bitsf1  12639  sadaddlem  12659  bitsres  12666  bitsuz  12667  bitsshft  12668  smumullem  12685  modgcd  12717  bezoutlem1  12719  bezoutlem2  12720  bezoutlem3  12721  bezoutlem4  12722  dvdsmulgcd  12735  rplpwr  12737  mulgcddvds  12785  rpexp  12801  qmuldeneqnum  12820  numdensq  12827  qden1elz  12830  hashdvds  12845  phiprm  12847  eulerthlem2  12852  fermltl  12854  prmdiv  12855  prmdiveq  12856  odzdvds  12862  pythagtriplem6  12876  pythagtriplem7  12877  pythagtriplem15  12884  pclem  12893  pcpremul  12898  pceulem  12900  pczpre  12902  pcdiv  12907  pcqmul  12908  pcqdiv  12912  pcexp  12914  pcaddlem  12938  pcadd  12939  fldivp1  12947  pcfac  12949  pcbc  12950  prmpwdvds  12953  prmreclem4  12968  4sqlem5  12991  4sqlem8  12994  4sqlem9  12995  4sqlem10  12996  4sqlem11  13004  4sqlem14  13007  4sqlem16  13009  4sqlem17  13010  vdwapun  13023  vdwnnlem2  13045  prmlem0  13109  mulgsubcl  14583  mulgdirlem  14593  mulgdir  14594  mulgass  14599  mulgsubdir  14600  odnncl  14862  odmulg  14871  odbezout  14873  sylow1lem1  14911  sylow2alem2  14931  efgtlen  15037  efgsres  15049  efgredleme  15054  efgredlemc  15056  odadd1  15142  odadd2  15143  cyggeninv  15172  ablfacrp  15303  pgpfac1lem3  15314  zlpirlem1  16443  zlpirlem3  16445  prmirredlem  16448  zndvds0  16506  znf1o  16507  znunit  16519  tgpmulg  17778  zdis  18324  uniioombllem3  18942  mbfi1fseqlem4  19075  dvexp3  19327  aareccl  19708  aalioulem1  19714  geolim3  19721  aaliou3lem2  19725  aaliou3lem6  19730  ulmshft  19771  dvradcnv  19799  sineq0  19891  efif1olem2  19907  wilthlem1  20308  wilthlem2  20309  basellem3  20322  mumul  20421  musum  20433  musumsum  20434  muinv  20435  ppiub  20445  chtub  20453  logfac2  20458  chpchtsum  20460  dchrptlem1  20505  pcbcctr  20517  bcmono  20518  bposlem5  20529  bposlem6  20530  lgslem1  20537  lgsval2lem  20547  lgsval4a  20559  lgsneg  20560  lgsneg1  20561  lgsmod  20562  lgsdirprm  20570  lgsdir  20571  lgsdilem2  20572  lgsdi  20573  lgsne0  20574  lgsabs1  20575  lgssq  20576  lgssq2  20577  lgsdirnn0  20580  lgsdinn0  20581  lgsqrlem1  20582  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem3  20592  lgseisenlem4  20593  lgsquadlem1  20595  lgsquad2lem1  20599  lgsquad3  20602  2sqlem3  20607  2sqlem4  20608  2sqlem8a  20612  2sqlem8  20613  2sqlem11  20616  2sqblem  20618  dchrisumlem1  20640  dchrmusum2  20645  dchrvmasumlem1  20646  dchrvmasum2lem  20647  mudivsum  20681  mulogsum  20683  mulog2sumlem2  20686  selberglem1  20696  selberglem3  20698  selberg  20699  pntpbnd2  20738  pntlemf  20756  padicabvcxp  20783  gxmodid  20948  fzspl  23032  bcm1n  23034  ltesubnnd  23035  ballotlemfc0  23053  ballotlemfcc  23054  ballotlemic  23067  ballotlem1c  23068  ballotlemsdom  23072  ballotlemsf1o  23074  ballotlemsima  23076  ballotlemfrceq  23089  ballotlemfrcn0  23090  ballotlem1ri  23095  predfz  24205  axlowdimlem14  24585  axlowdimlem16  24587  fsumkthpow  24793  ltflcei  24930  rdr  26446  fdc  26466  mettrifi  26484  caushft  26488  cntotbnd  26531  mzpsubmpt  26832  lzenom  26860  diophun  26864  eqrabdioph  26868  irrapxlem2  26919  irrapxlem3  26920  pellexlem6  26930  pell1234qrreccl  26950  pellfund14  26994  rmspecsqrnq  27002  rmxyneg  27016  rmxyadd  27017  rmxp1  27028  rmxm1  27030  rmym1  27031  rmxluc  27032  rmyluc  27033  rmyluc2  27034  rmxdbl  27035  rmydbl  27036  jm2.17a  27058  congadd  27064  congsub  27068  congabseq  27072  acongrep  27078  acongeq  27081  jm2.18  27092  jm2.19lem1  27093  jm2.19lem2  27094  jm2.19lem3  27095  jm2.22  27099  jm2.23  27100  jm2.20nn  27101  jm2.25  27103  jm2.26lem3  27105  jm2.27c  27111  psgnunilem5  27428  psgnunilem2  27429  psgnunilem4  27431  m1expaddsub  27432  psgnuni  27433  hashgcdlem  27527  clim1fr1  27738  wallispilem5  27829
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-resscn 8796
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-neg 9042  df-z 10027
  Copyright terms: Public domain W3C validator