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

Theorem zcnd 10309
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 10308 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9048 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8922   ZZcz 10215
This theorem is referenced by:  uzp1  10452  peano2uzr  10465  uzaddcl  10466  zsupss  10498  rpnnen1lem5  10537  fzm1  11058  fzrevral  11062  fzshftral  11065  fzoss2  11094  fzosubel  11106  fzosubel3  11108  quoremz  11164  intfrac2  11167  intfracq  11168  moddiffl  11187  modmul1  11207  modmul12d  11208  uzrdgxfr  11234  fzen2  11236  seqm1  11268  monoord2  11282  seqf1olem1  11290  seqf1olem2  11291  seqz  11299  expaddzlem  11351  modexp  11442  bcm1k  11534  bcp1nk  11536  bcval5  11537  bcpasc  11540  hashfz  11620  hashfzo  11622  hashbclem  11629  seqcoll  11640  ccatval3  11675  ccatlid  11676  ccatass  11678  swrd0val  11696  swrdid  11700  ccatswrd  11701  spllen  11711  splfv1  11712  splfv2a  11713  swrds1  11715  revccat  11726  revrev  11727  shftuz  11812  seqshft  11828  fzomaxdif  12075  climshftlem  12296  climshft  12298  climshft2  12304  iserex  12378  isercoll2  12390  serf0  12402  iseraltlem2  12404  iseraltlem3  12405  iseralt  12406  sumrblem  12433  fsumm1  12465  fsump1  12468  fsumshftm  12492  fsumrev2  12493  fsumtscopo  12509  fsumparts  12513  binomlem  12536  isumshft  12547  isumsplit  12548  isum1p  12549  arisum  12567  cvgrat  12588  mertenslem1  12589  eirrlem  12731  sqr2irrlem  12775  dvds2ln  12808  dvdsadd2b  12820  fsumdvds  12821  fzocongeq  12831  dvdsexp  12833  dvdsmod  12834  oddm1even  12837  oexpneg  12839  3dvds  12840  divalglem0  12841  divalglem4  12844  divalglem8  12848  divalgb  12852  divalgmod  12854  bitsp1  12871  bitsp1e  12872  bitsfzo  12875  bitsmod  12876  bitsinv1lem  12881  bitsf1  12886  sadaddlem  12906  bitsres  12913  bitsuz  12914  bitsshft  12915  smumullem  12932  modgcd  12964  bezoutlem1  12966  bezoutlem2  12967  bezoutlem3  12968  bezoutlem4  12969  dvdsmulgcd  12982  rplpwr  12984  mulgcddvds  13032  rpexp  13048  qmuldeneqnum  13067  numdensq  13074  qden1elz  13077  hashdvds  13092  phiprm  13094  eulerthlem2  13099  fermltl  13101  prmdiv  13102  prmdiveq  13103  odzdvds  13109  pythagtriplem6  13123  pythagtriplem7  13124  pythagtriplem15  13131  pclem  13140  pcpremul  13145  pceulem  13147  pczpre  13149  pcdiv  13154  pcqmul  13155  pcqdiv  13159  pcexp  13161  pcaddlem  13185  pcadd  13186  fldivp1  13194  pcfac  13196  pcbc  13197  prmpwdvds  13200  prmreclem4  13215  4sqlem5  13238  4sqlem8  13241  4sqlem9  13242  4sqlem10  13243  4sqlem11  13251  4sqlem14  13254  4sqlem16  13256  4sqlem17  13257  vdwapun  13270  vdwnnlem2  13292  prmlem0  13356  mulgsubcl  14832  mulgdirlem  14842  mulgdir  14843  mulgass  14848  mulgsubdir  14849  odnncl  15111  odmulg  15120  odbezout  15122  sylow1lem1  15160  sylow2alem2  15180  efgtlen  15286  efgsres  15298  efgredleme  15303  efgredlemc  15305  odadd1  15391  odadd2  15392  cyggeninv  15421  ablfacrp  15552  pgpfac1lem3  15563  zlpirlem1  16692  zlpirlem3  16694  prmirredlem  16697  zndvds0  16755  znf1o  16756  znunit  16768  tgpmulg  18045  zdis  18719  uniioombllem3  19345  mbfi1fseqlem4  19478  dvexp3  19730  aareccl  20111  aalioulem1  20117  geolim3  20124  aaliou3lem2  20128  aaliou3lem6  20133  ulmshft  20174  dvradcnv  20205  sineq0  20297  efif1olem2  20313  wilthlem1  20719  wilthlem2  20720  basellem3  20733  mumul  20832  musum  20844  musumsum  20845  muinv  20846  ppiub  20856  chtub  20864  logfac2  20869  chpchtsum  20871  dchrptlem1  20916  pcbcctr  20928  bcmono  20929  bposlem5  20940  bposlem6  20941  lgslem1  20948  lgsval2lem  20958  lgsval4a  20970  lgsneg  20971  lgsneg1  20972  lgsmod  20973  lgsdirprm  20981  lgsdir  20982  lgsdilem2  20983  lgsdi  20984  lgsne0  20985  lgsabs1  20986  lgssq  20987  lgssq2  20988  lgsdirnn0  20991  lgsdinn0  20992  lgsqrlem1  20993  lgseisenlem1  21001  lgseisenlem2  21002  lgseisenlem3  21003  lgseisenlem4  21004  lgsquadlem1  21006  lgsquad2lem1  21010  lgsquad3  21013  2sqlem3  21018  2sqlem4  21019  2sqlem8a  21023  2sqlem8  21024  2sqlem11  21027  2sqblem  21029  dchrisumlem1  21051  dchrmusum2  21056  dchrvmasumlem1  21057  dchrvmasum2lem  21058  mudivsum  21092  mulogsum  21094  mulog2sumlem2  21097  selberglem1  21107  selberglem3  21109  selberg  21110  pntpbnd2  21149  pntlemf  21167  padicabvcxp  21194  wlkdvspthlem  21456  fargshiftf1  21473  fargshiftfo  21474  eupatrl  21539  gxmodid  21716  fzspl  23986  bcm1n  23988  numdenneg  23999  divnumden2  24000  ltesubnnd  24001  zzsmulg  24082  zrhnm  24155  qqhval2lem  24165  qqhghm  24172  qqhrhm  24173  qqhnm  24174  ballotlemfc0  24530  ballotlemfcc  24531  ballotlemic  24544  ballotlem1c  24545  ballotlemsgt1  24548  ballotlemsdom  24549  ballotlemsel1i  24550  ballotlemsf1o  24551  ballotlemsima  24553  ballotlemfrceq  24566  ballotlemfrcn0  24567  ballotlem1ri  24572  igamz  24612  divcnvlin  24992  ntrivcvg  25005  ntrivcvgtail  25008  prodrblem  25035  fprodser  25055  fprodm1  25070  fprodp1  25072  fprodshft  25080  fprodrev  25081  fallfacfwd  25120  predfz  25228  axlowdimlem14  25609  axlowdimlem16  25611  fsumkthpow  25817  ltflcei  25951  fdc  26141  mettrifi  26155  caushft  26159  cntotbnd  26197  mzpsubmpt  26492  lzenom  26520  diophun  26524  eqrabdioph  26528  irrapxlem2  26578  irrapxlem3  26579  pellexlem6  26589  pell1234qrreccl  26609  pellfund14  26653  rmspecsqrnq  26661  rmxyneg  26675  rmxyadd  26676  rmxp1  26687  rmxm1  26689  rmym1  26690  rmxluc  26691  rmyluc  26692  rmyluc2  26693  rmxdbl  26694  rmydbl  26695  jm2.17a  26717  congadd  26723  congsub  26727  congabseq  26731  acongrep  26737  acongeq  26740  jm2.18  26751  jm2.19lem1  26752  jm2.19lem2  26753  jm2.19lem3  26754  jm2.22  26758  jm2.23  26759  jm2.20nn  26760  jm2.25  26762  jm2.26lem3  26764  jm2.27c  26770  psgnunilem5  27087  psgnunilem2  27088  psgnunilem4  27090  m1expaddsub  27091  psgnuni  27092  hashgcdlem  27186  fmul01lt1lem2  27384  clim1fr1  27396  stoweidlem11  27429  stoweidlem26  27444  wallispilem5  27487
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 2369  ax-resscn 8981
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 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-neg 9227  df-z 10216
  Copyright terms: Public domain W3C validator