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

Theorem zcnd 10332
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 10331 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9070 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   CCcc 8944   ZZcz 10238
This theorem is referenced by:  uzp1  10475  peano2uzr  10488  uzaddcl  10489  zsupss  10521  rpnnen1lem5  10560  fzm1  11082  fzrevral  11086  fzshftral  11089  fzoss2  11118  fzosubel  11132  fzosubel3  11134  quoremz  11191  intfrac2  11194  intfracq  11195  moddiffl  11214  modmul1  11234  modmul12d  11235  uzrdgxfr  11261  fzen2  11263  seqm1  11295  monoord2  11309  seqf1olem1  11317  seqf1olem2  11318  seqz  11326  expaddzlem  11378  modexp  11469  bcm1k  11561  bcp1nk  11563  bcval5  11564  bcpasc  11567  hashfz  11647  hashfzo  11649  hashbclem  11656  seqcoll  11667  ccatval3  11702  ccatlid  11703  ccatass  11705  swrd0val  11723  swrdid  11727  ccatswrd  11728  spllen  11738  splfv1  11739  splfv2a  11740  swrds1  11742  revccat  11753  revrev  11754  shftuz  11839  seqshft  11855  fzomaxdif  12102  climshftlem  12323  climshft  12325  climshft2  12331  iserex  12405  isercoll2  12417  serf0  12429  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  sumrblem  12460  fsumm1  12492  fsump1  12495  fsumshftm  12519  fsumrev2  12520  fsumtscopo  12536  fsumparts  12540  binomlem  12563  isumshft  12574  isumsplit  12575  isum1p  12576  arisum  12594  cvgrat  12615  mertenslem1  12616  eirrlem  12758  sqr2irrlem  12802  dvds2ln  12835  dvdsadd2b  12847  fsumdvds  12848  fzocongeq  12858  dvdsexp  12860  dvdsmod  12861  oddm1even  12864  oexpneg  12866  3dvds  12867  divalglem0  12868  divalglem4  12871  divalglem8  12875  divalgb  12879  divalgmod  12881  bitsp1  12898  bitsp1e  12899  bitsfzo  12902  bitsmod  12903  bitsinv1lem  12908  bitsf1  12913  sadaddlem  12933  bitsres  12940  bitsuz  12941  bitsshft  12942  smumullem  12959  modgcd  12991  bezoutlem1  12993  bezoutlem2  12994  bezoutlem3  12995  bezoutlem4  12996  dvdsmulgcd  13009  rplpwr  13011  mulgcddvds  13059  rpexp  13075  qmuldeneqnum  13094  numdensq  13101  qden1elz  13104  hashdvds  13119  phiprm  13121  eulerthlem2  13126  fermltl  13128  prmdiv  13129  prmdiveq  13130  odzdvds  13136  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem15  13158  pclem  13167  pcpremul  13172  pceulem  13174  pczpre  13176  pcdiv  13181  pcqmul  13182  pcqdiv  13186  pcexp  13188  pcaddlem  13212  pcadd  13213  fldivp1  13221  pcfac  13223  pcbc  13224  prmpwdvds  13227  prmreclem4  13242  4sqlem5  13265  4sqlem8  13268  4sqlem9  13269  4sqlem10  13270  4sqlem11  13278  4sqlem14  13281  4sqlem16  13283  4sqlem17  13284  vdwapun  13297  vdwnnlem2  13319  prmlem0  13383  mulgsubcl  14859  mulgdirlem  14869  mulgdir  14870  mulgass  14875  mulgsubdir  14876  odnncl  15138  odmulg  15147  odbezout  15149  sylow1lem1  15187  sylow2alem2  15207  efgtlen  15313  efgsres  15325  efgredleme  15330  efgredlemc  15332  odadd1  15418  odadd2  15419  cyggeninv  15448  ablfacrp  15579  pgpfac1lem3  15590  zlpirlem1  16723  zlpirlem3  16725  prmirredlem  16728  zndvds0  16786  znf1o  16787  znunit  16799  tgpmulg  18076  zdis  18800  uniioombllem3  19430  mbfi1fseqlem4  19563  dvexp3  19815  aareccl  20196  aalioulem1  20202  geolim3  20209  aaliou3lem2  20213  aaliou3lem6  20218  ulmshft  20259  dvradcnv  20290  sineq0  20382  efif1olem2  20398  wilthlem1  20804  wilthlem2  20805  basellem3  20818  mumul  20917  musum  20929  musumsum  20930  muinv  20931  ppiub  20941  chtub  20949  logfac2  20954  chpchtsum  20956  dchrptlem1  21001  pcbcctr  21013  bcmono  21014  bposlem5  21025  bposlem6  21026  lgslem1  21033  lgsval2lem  21043  lgsval4a  21055  lgsneg  21056  lgsneg1  21057  lgsmod  21058  lgsdirprm  21066  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgsabs1  21071  lgssq  21072  lgssq2  21073  lgsdirnn0  21076  lgsdinn0  21077  lgsqrlem1  21078  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquad2lem1  21095  lgsquad3  21098  2sqlem3  21103  2sqlem4  21104  2sqlem8a  21108  2sqlem8  21109  2sqlem11  21112  2sqblem  21114  dchrisumlem1  21136  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  selberglem1  21192  selberglem3  21194  selberg  21195  pntpbnd2  21234  pntlemf  21252  padicabvcxp  21279  wlkdvspthlem  21560  fargshiftf1  21577  fargshiftfo  21578  eupatrl  21643  gxmodid  21820  fzspl  24102  bcm1n  24104  numdenneg  24113  divnumden2  24114  ltesubnnd  24115  zzsmulg  24218  zrhnm  24306  qqhval2lem  24318  qqhghm  24325  qqhrhm  24326  qqhnm  24327  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemic  24717  ballotlem1c  24718  ballotlemsgt1  24721  ballotlemsdom  24722  ballotlemsel1i  24723  ballotlemsf1o  24724  ballotlemsima  24726  ballotlemfrceq  24739  ballotlemfrcn0  24740  ballotlem1ri  24745  igamz  24785  divcnvlin  25165  ntrivcvg  25178  ntrivcvgtail  25181  prodrblem  25208  fprodser  25228  fprodm1  25243  fprodp1  25245  fprodshft  25253  fprodrev  25254  fallfacfwd  25303  0fallfac  25304  binomfallfaclem2  25307  predfz  25417  axlowdimlem14  25798  axlowdimlem16  25800  fsumkthpow  26006  ltflcei  26140  fdc  26339  mettrifi  26353  caushft  26357  cntotbnd  26395  mzpsubmpt  26690  lzenom  26718  diophun  26722  eqrabdioph  26726  irrapxlem2  26776  irrapxlem3  26777  pellexlem6  26787  pell1234qrreccl  26807  pellfund14  26851  rmspecsqrnq  26859  rmxyneg  26873  rmxyadd  26874  rmxp1  26885  rmxm1  26887  rmym1  26888  rmxluc  26889  rmyluc  26890  rmyluc2  26891  rmxdbl  26892  rmydbl  26893  jm2.17a  26915  congadd  26921  congsub  26925  congabseq  26929  acongrep  26935  acongeq  26938  jm2.18  26949  jm2.19lem1  26950  jm2.19lem2  26951  jm2.19lem3  26952  jm2.22  26956  jm2.23  26957  jm2.20nn  26958  jm2.25  26960  jm2.26lem3  26962  jm2.27c  26968  psgnunilem5  27285  psgnunilem2  27286  psgnunilem4  27288  m1expaddsub  27289  psgnuni  27290  hashgcdlem  27384  fmul01lt1lem2  27582  clim1fr1  27594  stoweidlem11  27627  stoweidlem26  27642  wallispilem5  27685  fzosplitsnm1  27991  swrdswrd0  28013  swrdccatin12c  28028
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239
  Copyright terms: Public domain W3C validator