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

Theorem zcnd 10956
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 10955 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9611 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   CCcc 9479   ZZcz 10853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-neg 9797  df-z 10854
This theorem is referenced by:  uzp1  11104  peano2uzr  11125  uzaddcl  11126  zsupss  11160  rpnnen1lem5  11201  fzm1  11747  fzrevral  11751  fzshftral  11754  nn0disj  11777  fzoss2  11810  fzosubel  11832  fzosubel3  11834  fzocatel  11837  fzosplitsnm1  11847  quoremz  11938  intfrac2  11941  intfracq  11942  flpmodeq  11957  moddiffl  11963  modmul1  11996  modmul12d  11997  uzrdgxfr  12033  fzen2  12035  seqm1  12080  monoord2  12094  seqf1olem1  12102  seqf1olem2  12103  seqz  12111  expaddzlem  12164  modexp  12256  bcm1k  12348  bcp1nk  12350  bcval5  12351  bcpasc  12354  hashfz  12437  hashfzo  12439  hashbclem  12454  seqcoll  12465  ccatval3  12549  ccatlid  12555  ccatass  12557  swrd0val  12598  swrdid  12602  swrd0fv  12616  swrdspsleq  12623  swrds1  12626  ccatswrd  12631  swrdswrd0  12637  spllen  12680  splfv1  12681  splfv2a  12682  revccat  12690  revrev  12691  cshwidxmod  12724  cshwidxm1  12727  2cshwcshw  12743  shftuz  12852  seqshft  12868  fzomaxdif  13125  climshftlem  13346  climshft  13348  climshft2  13354  iserex  13428  isercoll2  13440  serf0  13452  iseraltlem2  13454  iseraltlem3  13455  iseralt  13456  sumrblem  13482  fsumm1  13515  fsumsplitsnun  13519  fsump1  13520  fsumshftm  13545  fsumrev2  13546  telfsumo  13565  fsumparts  13569  binomlem  13593  isumshft  13603  isumsplit  13604  isum1p  13605  arisum  13623  cvgrat  13644  mertenslem1  13645  eirrlem  13787  sqr2irrlem  13831  dvds2ln  13864  dvdsadd2b  13876  fsumdvds  13877  fzocongeq  13888  dvdsexp  13890  dvdsmod  13891  oddm1even  13895  oexpneg  13897  3dvds  13898  divalglem0  13899  divalglem4  13902  divalglem8  13906  divalgb  13910  divalgmod  13912  bitsp1  13929  bitsfzo  13933  bitsmod  13934  bitsinv1lem  13939  bitsf1  13944  sadaddlem  13964  bitsres  13971  bitsuz  13972  bitsshft  13973  smumullem  13990  modgcd  14022  bezoutlem1  14024  bezoutlem2  14025  bezoutlem3  14026  bezoutlem4  14027  dvdsmulgcd  14040  rplpwr  14042  mulgcddvds  14093  rpexp  14109  qmuldeneqnum  14128  numdensq  14135  qden1elz  14138  hashdvds  14153  phiprm  14155  eulerthlem2  14160  fermltl  14162  prmdiv  14163  prmdiveq  14164  odzdvds  14170  modprm0  14178  modprmn0modprm0  14180  pythagtriplem6  14193  pythagtriplem7  14194  pythagtriplem15  14201  pclem  14210  pcpremul  14215  pceulem  14217  pczpre  14219  pcdiv  14224  pcqmul  14225  pcqdiv  14229  pcexp  14231  pcaddlem  14255  pcadd  14256  fldivp1  14264  pcfac  14266  pcbc  14267  prmpwdvds  14270  prmreclem4  14285  4sqlem5  14308  4sqlem8  14311  4sqlem9  14312  4sqlem10  14313  4sqlem11  14321  4sqlem14  14324  4sqlem16  14326  4sqlem17  14327  vdwapun  14340  vdwnnlem2  14362  prmlem0  14438  mulgsubcl  15949  mulgdirlem  15959  mulgdir  15960  mulgass  15965  mulgsubdir  15966  psgnunilem5  16308  psgnunilem2  16309  psgnunilem4  16311  m1expaddsub  16312  psgnuni  16313  odnncl  16358  odmulg  16367  odbezout  16369  sylow1lem1  16407  sylow2alem2  16427  efgtlen  16533  efgsres  16545  efgredleme  16550  efgredlemc  16552  odadd1  16640  odadd2  16641  cyggeninv  16670  gsummptshft  16740  ablfacrp  16900  pgpfac1lem3  16911  srgbinomlem3  16974  srgbinomlem4  16975  zringmulg  18257  zrngmulg  18263  zringlpirlem1  18269  zringlpirlem3  18271  zlpirlem1  18274  zlpirlem3  18276  prmirredlem  18283  prmirredlemOLD  18286  zndvds0  18349  znf1o  18350  znunit  18362  cayhamlem1  19127  tgpmulg  20320  zdis  21049  uniioombllem3  21722  mbfi1fseqlem4  21853  dvexp3  22107  aareccl  22449  aalioulem1  22455  geolim3  22462  aaliou3lem2  22466  aaliou3lem6  22471  ulmshft  22512  dvradcnv  22543  sineq0  22640  efif1olem2  22656  wilthlem1  23063  wilthlem2  23064  basellem3  23077  mumul  23176  musum  23188  musumsum  23189  muinv  23190  ppiub  23200  chtub  23208  logfac2  23213  chpchtsum  23215  dchrptlem1  23260  pcbcctr  23272  bcmono  23273  bposlem5  23284  bposlem6  23285  lgslem1  23292  lgsval2lem  23302  lgsval4a  23314  lgsneg  23315  lgsneg1  23316  lgsmod  23317  lgsdirprm  23325  lgsdir  23326  lgsdilem2  23327  lgsdi  23328  lgsne0  23329  lgsabs1  23330  lgssq  23331  lgssq2  23332  lgsdirnn0  23335  lgsdinn0  23336  lgsqrlem1  23337  lgseisenlem1  23345  lgseisenlem2  23346  lgseisenlem3  23347  lgseisenlem4  23348  lgsquadlem1  23350  lgsquad2lem1  23354  lgsquad3  23357  2sqlem3  23362  2sqlem4  23363  2sqlem8a  23367  2sqlem8  23368  2sqlem11  23371  2sqblem  23373  dchrisumlem1  23395  dchrmusum2  23400  dchrvmasumlem1  23401  dchrvmasum2lem  23402  mudivsum  23436  mulogsum  23438  mulog2sumlem2  23441  selberglem1  23451  selberglem3  23453  selberg  23454  pntpbnd2  23493  pntlemf  23511  padicabvcxp  23538  axlowdimlem14  23927  axlowdimlem16  23929  wlkdvspthlem  24271  fargshiftf1  24299  fargshiftfo  24300  clwwisshclww  24469  eupatrl  24630  gxmodid  24807  fzspl  27116  bcm1n  27118  numdenneg  27125  divnumden2  27126  ltesubnnd  27130  archiabllem1  27249  archiabllem2c  27251  zrhnm  27436  qqhval2lem  27448  qqhghm  27455  qqhrhm  27456  qqhnm  27457  ballotlemfc0  27921  ballotlemfcc  27922  ballotlemic  27935  ballotlem1c  27936  ballotlemsgt1  27939  ballotlemsdom  27940  ballotlemsel1i  27941  ballotlemsf1o  27942  ballotlemsima  27944  ballotlemfrceq  27957  ballotlemfrcn0  27958  ballotlem1ri  27963  signsplypnf  27997  igamz  28080  divcnvlin  28445  ntrivcvg  28458  ntrivcvgtail  28461  prodrblem  28488  fprodser  28508  fprodm1  28523  fprodp1  28525  fprodshft  28533  fprodrev  28534  fallfacval3  28561  fallfacfwd  28585  0fallfac  28586  binomfallfaclem2  28589  fallfacval4  28592  predfz  28710  fsumkthpow  29245  ltflcei  29470  fdc  29692  mettrifi  29704  caushft  29708  cntotbnd  29746  mzpsubmpt  30130  lzenom  30158  diophun  30162  eqrabdioph  30166  irrapxlem2  30214  irrapxlem3  30215  pellexlem6  30225  pell1234qrreccl  30245  pellfund14  30289  rmspecsqrnq  30297  rmxyneg  30311  rmxyadd  30312  rmxp1  30323  rmxm1  30325  rmym1  30326  rmxluc  30327  rmyluc  30328  rmyluc2  30329  rmxdbl  30330  rmydbl  30331  jm2.17a  30353  congadd  30359  congsub  30363  congabseq  30367  acongrep  30373  acongeq  30376  jm2.18  30387  jm2.19lem1  30388  jm2.19lem2  30389  jm2.19lem3  30390  jm2.22  30394  jm2.23  30395  jm2.20nn  30396  jm2.25  30398  jm2.26lem3  30400  jm2.27c  30406  hashgcdlem  30615  fzisoeu  30896  fperiodmul  30900  fmul01lt1lem2  30954  clim1fr1  30962  sumnnodd  30991  stoweidlem11  31130  stoweidlem26  31145  wallispilem5  31188  dirkertrigeqlem1  31217  dirkertrigeqlem2  31218  dirkertrigeqlem3  31219  dirkeritg  31221  fourierdlem11  31237  fourierdlem26  31252  fourierdlem48  31274  fourierdlem54  31280  fourierdlem79  31305  fourierdlem103  31329  fourierdlem104  31330  2elfz2melfz  31622  fsumsplitsndif  31632  ztprmneprm  31875  altgsumbcALT  31881  sineq0ALT  32692
  Copyright terms: Public domain W3C validator