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

Theorem zcnd 10134
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 10133 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 8877 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   CCcc 8751   ZZcz 10040
This theorem is referenced by:  uzp1  10277  peano2uzr  10290  uzaddcl  10291  zsupss  10323  rpnnen1lem5  10362  fzm1  10878  fzrevral  10882  fzshftral  10885  fzoss2  10913  fzosubel  10924  fzosubel3  10926  quoremz  10975  intfrac2  10978  intfracq  10979  moddiffl  10998  modmul1  11018  modmul12d  11019  uzrdgxfr  11045  fzen2  11047  seqm1  11079  monoord2  11093  seqf1olem1  11101  seqf1olem2  11102  seqz  11110  expaddzlem  11161  modexp  11252  bcm1k  11343  bcp1nk  11345  bcval5  11346  bcpasc  11349  hashfz  11397  hashfzo  11399  hashbclem  11406  seqcoll  11417  ccatval3  11449  ccatlid  11450  ccatass  11452  swrd0val  11470  swrdid  11474  ccatswrd  11475  spllen  11485  splfv1  11486  splfv2a  11487  swrds1  11489  revccat  11500  revrev  11501  shftuz  11580  seqshft  11596  fzomaxdif  11843  climshftlem  12064  climshft  12066  climshft2  12072  iserex  12146  isercoll2  12158  serf0  12169  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  sumrblem  12200  fsumm1  12232  fsump1  12235  fsumshftm  12259  fsumrev2  12260  fsumtscopo  12276  fsumparts  12280  binomlem  12303  isumshft  12314  isumsplit  12315  isum1p  12316  arisum  12334  cvgrat  12355  mertenslem1  12356  eirrlem  12498  sqr2irrlem  12542  dvds2ln  12575  dvdsadd2b  12587  fsumdvds  12588  fzocongeq  12598  dvdsexp  12600  dvdsmod  12601  oddm1even  12604  oexpneg  12606  3dvds  12607  divalglem0  12608  divalglem4  12611  divalglem8  12615  divalgb  12619  divalgmod  12621  bitsp1e  12639  bitsfzo  12642  bitsmod  12643  bitsinv1lem  12648  bitsf1  12653  sadaddlem  12673  bitsres  12680  bitsuz  12681  bitsshft  12682  smumullem  12699  modgcd  12731  bezoutlem1  12733  bezoutlem2  12734  bezoutlem3  12735  bezoutlem4  12736  dvdsmulgcd  12749  rplpwr  12751  mulgcddvds  12799  rpexp  12815  qmuldeneqnum  12834  numdensq  12841  qden1elz  12844  hashdvds  12859  phiprm  12861  eulerthlem2  12866  fermltl  12868  prmdiv  12869  prmdiveq  12870  odzdvds  12876  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem15  12898  pclem  12907  pcpremul  12912  pceulem  12914  pczpre  12916  pcdiv  12921  pcqmul  12922  pcqdiv  12926  pcexp  12928  pcaddlem  12952  pcadd  12953  fldivp1  12961  pcfac  12963  pcbc  12964  prmpwdvds  12967  prmreclem4  12982  4sqlem5  13005  4sqlem8  13008  4sqlem9  13009  4sqlem10  13010  4sqlem11  13018  4sqlem14  13021  4sqlem16  13023  4sqlem17  13024  vdwapun  13037  vdwnnlem2  13059  prmlem0  13123  mulgsubcl  14597  mulgdirlem  14607  mulgdir  14608  mulgass  14613  mulgsubdir  14614  odnncl  14876  odmulg  14885  odbezout  14887  sylow1lem1  14925  sylow2alem2  14945  efgtlen  15051  efgsres  15063  efgredleme  15068  efgredlemc  15070  odadd1  15156  odadd2  15157  cyggeninv  15186  ablfacrp  15317  pgpfac1lem3  15328  zlpirlem1  16457  zlpirlem3  16459  prmirredlem  16462  zndvds0  16520  znf1o  16521  znunit  16533  tgpmulg  17792  zdis  18338  uniioombllem3  18956  mbfi1fseqlem4  19089  dvexp3  19341  aareccl  19722  aalioulem1  19728  geolim3  19735  aaliou3lem2  19739  aaliou3lem6  19744  ulmshft  19785  dvradcnv  19813  sineq0  19905  efif1olem2  19921  wilthlem1  20322  wilthlem2  20323  basellem3  20336  mumul  20435  musum  20447  musumsum  20448  muinv  20449  ppiub  20459  chtub  20467  logfac2  20472  chpchtsum  20474  dchrptlem1  20519  pcbcctr  20531  bcmono  20532  bposlem5  20543  bposlem6  20544  lgslem1  20551  lgsval2lem  20561  lgsval4a  20573  lgsneg  20574  lgsneg1  20575  lgsmod  20576  lgsdirprm  20584  lgsdir  20585  lgsdilem2  20586  lgsdi  20587  lgsne0  20588  lgsabs1  20589  lgssq  20590  lgssq2  20591  lgsdirnn0  20594  lgsdinn0  20595  lgsqrlem1  20596  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquad2lem1  20613  lgsquad3  20616  2sqlem3  20621  2sqlem4  20622  2sqlem8a  20626  2sqlem8  20627  2sqlem11  20630  2sqblem  20632  dchrisumlem1  20654  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  mudivsum  20695  mulogsum  20697  mulog2sumlem2  20700  selberglem1  20710  selberglem3  20712  selberg  20713  pntpbnd2  20752  pntlemf  20770  padicabvcxp  20797  gxmodid  20962  fzspl  23046  bcm1n  23048  ltesubnnd  23049  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemic  23081  ballotlem1c  23082  ballotlemsdom  23086  ballotlemsf1o  23088  ballotlemsima  23090  ballotlemfrceq  23103  ballotlemfrcn0  23104  ballotlem1ri  23109  prodrblem  24152  predfz  24274  axlowdimlem14  24655  axlowdimlem16  24657  fsumkthpow  24863  ltflcei  24998  rdr  26538  fdc  26558  mettrifi  26576  caushft  26580  cntotbnd  26623  mzpsubmpt  26924  lzenom  26952  diophun  26956  eqrabdioph  26960  irrapxlem2  27011  irrapxlem3  27012  pellexlem6  27022  pell1234qrreccl  27042  pellfund14  27086  rmspecsqrnq  27094  rmxyneg  27108  rmxyadd  27109  rmxp1  27120  rmxm1  27122  rmym1  27123  rmxluc  27124  rmyluc  27125  rmyluc2  27126  rmxdbl  27127  rmydbl  27128  jm2.17a  27150  congadd  27156  congsub  27160  congabseq  27164  acongrep  27170  acongeq  27173  jm2.18  27184  jm2.19lem1  27185  jm2.19lem2  27186  jm2.19lem3  27187  jm2.22  27191  jm2.23  27192  jm2.20nn  27193  jm2.25  27195  jm2.26lem3  27197  jm2.27c  27203  psgnunilem5  27520  psgnunilem2  27521  psgnunilem4  27523  m1expaddsub  27524  psgnuni  27525  hashgcdlem  27619  clim1fr1  27830  wallispilem5  27921  wlkdvspthlem  28365  fargshiftf1  28382  fargshiftfo  28383  eupatrl  28385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810
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 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-neg 9056  df-z 10041
  Copyright terms: Public domain W3C validator