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

Theorem zcnd 10381
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 10380 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9119 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   CCcc 8993   ZZcz 10287
This theorem is referenced by:  uzp1  10524  peano2uzr  10537  uzaddcl  10538  zsupss  10570  rpnnen1lem5  10609  fzm1  11132  fzrevral  11136  fzshftral  11139  fzoss2  11168  fzosubel  11182  fzosubel3  11184  quoremz  11241  intfrac2  11244  intfracq  11245  moddiffl  11264  modmul1  11284  modmul12d  11285  uzrdgxfr  11311  fzen2  11313  seqm1  11345  monoord2  11359  seqf1olem1  11367  seqf1olem2  11368  seqz  11376  expaddzlem  11428  modexp  11519  bcm1k  11611  bcp1nk  11613  bcval5  11614  bcpasc  11617  hashfz  11697  hashfzo  11699  hashbclem  11706  seqcoll  11717  ccatval3  11752  ccatlid  11753  ccatass  11755  swrd0val  11773  swrdid  11777  ccatswrd  11778  spllen  11788  splfv1  11789  splfv2a  11790  swrds1  11792  revccat  11803  revrev  11804  shftuz  11889  seqshft  11905  fzomaxdif  12152  climshftlem  12373  climshft  12375  climshft2  12381  iserex  12455  isercoll2  12467  serf0  12479  iseraltlem2  12481  iseraltlem3  12482  iseralt  12483  sumrblem  12510  fsumm1  12542  fsump1  12545  fsumshftm  12569  fsumrev2  12570  fsumtscopo  12586  fsumparts  12590  binomlem  12613  isumshft  12624  isumsplit  12625  isum1p  12626  arisum  12644  cvgrat  12665  mertenslem1  12666  eirrlem  12808  sqr2irrlem  12852  dvds2ln  12885  dvdsadd2b  12897  fsumdvds  12898  fzocongeq  12908  dvdsexp  12910  dvdsmod  12911  oddm1even  12914  oexpneg  12916  3dvds  12917  divalglem0  12918  divalglem4  12921  divalglem8  12925  divalgb  12929  divalgmod  12931  bitsp1  12948  bitsp1e  12949  bitsfzo  12952  bitsmod  12953  bitsinv1lem  12958  bitsf1  12963  sadaddlem  12983  bitsres  12990  bitsuz  12991  bitsshft  12992  smumullem  13009  modgcd  13041  bezoutlem1  13043  bezoutlem2  13044  bezoutlem3  13045  bezoutlem4  13046  dvdsmulgcd  13059  rplpwr  13061  mulgcddvds  13109  rpexp  13125  qmuldeneqnum  13144  numdensq  13151  qden1elz  13154  hashdvds  13169  phiprm  13171  eulerthlem2  13176  fermltl  13178  prmdiv  13179  prmdiveq  13180  odzdvds  13186  pythagtriplem6  13200  pythagtriplem7  13201  pythagtriplem15  13208  pclem  13217  pcpremul  13222  pceulem  13224  pczpre  13226  pcdiv  13231  pcqmul  13232  pcqdiv  13236  pcexp  13238  pcaddlem  13262  pcadd  13263  fldivp1  13271  pcfac  13273  pcbc  13274  prmpwdvds  13277  prmreclem4  13292  4sqlem5  13315  4sqlem8  13318  4sqlem9  13319  4sqlem10  13320  4sqlem11  13328  4sqlem14  13331  4sqlem16  13333  4sqlem17  13334  vdwapun  13347  vdwnnlem2  13369  prmlem0  13433  mulgsubcl  14909  mulgdirlem  14919  mulgdir  14920  mulgass  14925  mulgsubdir  14926  odnncl  15188  odmulg  15197  odbezout  15199  sylow1lem1  15237  sylow2alem2  15257  efgtlen  15363  efgsres  15375  efgredleme  15380  efgredlemc  15382  odadd1  15468  odadd2  15469  cyggeninv  15498  ablfacrp  15629  pgpfac1lem3  15640  zlpirlem1  16773  zlpirlem3  16775  prmirredlem  16778  zndvds0  16836  znf1o  16837  znunit  16849  tgpmulg  18128  zdis  18852  uniioombllem3  19482  mbfi1fseqlem4  19613  dvexp3  19867  aareccl  20248  aalioulem1  20254  geolim3  20261  aaliou3lem2  20265  aaliou3lem6  20270  ulmshft  20311  dvradcnv  20342  sineq0  20434  efif1olem2  20450  wilthlem1  20856  wilthlem2  20857  basellem3  20870  mumul  20969  musum  20981  musumsum  20982  muinv  20983  ppiub  20993  chtub  21001  logfac2  21006  chpchtsum  21008  dchrptlem1  21053  pcbcctr  21065  bcmono  21066  bposlem5  21077  bposlem6  21078  lgslem1  21085  lgsval2lem  21095  lgsval4a  21107  lgsneg  21108  lgsneg1  21109  lgsmod  21110  lgsdirprm  21118  lgsdir  21119  lgsdilem2  21120  lgsdi  21121  lgsne0  21122  lgsabs1  21123  lgssq  21124  lgssq2  21125  lgsdirnn0  21128  lgsdinn0  21129  lgsqrlem1  21130  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem3  21140  lgseisenlem4  21141  lgsquadlem1  21143  lgsquad2lem1  21147  lgsquad3  21150  2sqlem3  21155  2sqlem4  21156  2sqlem8a  21160  2sqlem8  21161  2sqlem11  21164  2sqblem  21166  dchrisumlem1  21188  dchrmusum2  21193  dchrvmasumlem1  21194  dchrvmasum2lem  21195  mudivsum  21229  mulogsum  21231  mulog2sumlem2  21234  selberglem1  21244  selberglem3  21246  selberg  21247  pntpbnd2  21286  pntlemf  21304  padicabvcxp  21331  wlkdvspthlem  21612  fargshiftf1  21629  fargshiftfo  21630  eupatrl  21695  gxmodid  21872  fzspl  24154  bcm1n  24156  numdenneg  24165  divnumden2  24166  ltesubnnd  24167  zzsmulg  24270  zrhnm  24358  qqhval2lem  24370  qqhghm  24377  qqhrhm  24378  qqhnm  24379  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemic  24769  ballotlem1c  24770  ballotlemsgt1  24773  ballotlemsdom  24774  ballotlemsel1i  24775  ballotlemsf1o  24776  ballotlemsima  24778  ballotlemfrceq  24791  ballotlemfrcn0  24792  ballotlem1ri  24797  igamz  24837  divcnvlin  25217  ntrivcvg  25230  ntrivcvgtail  25233  prodrblem  25260  fprodser  25280  fprodm1  25295  fprodp1  25297  fprodshft  25305  fprodrev  25306  fallfacval3  25333  fallfacfwd  25357  0fallfac  25358  binomfallfaclem2  25361  fallfacval4  25364  predfz  25483  axlowdimlem14  25899  axlowdimlem16  25901  fsumkthpow  26107  ltflcei  26247  fdc  26462  mettrifi  26476  caushft  26480  cntotbnd  26518  mzpsubmpt  26813  lzenom  26841  diophun  26845  eqrabdioph  26849  irrapxlem2  26899  irrapxlem3  26900  pellexlem6  26910  pell1234qrreccl  26930  pellfund14  26974  rmspecsqrnq  26982  rmxyneg  26996  rmxyadd  26997  rmxp1  27008  rmxm1  27010  rmym1  27011  rmxluc  27012  rmyluc  27013  rmyluc2  27014  rmxdbl  27015  rmydbl  27016  jm2.17a  27038  congadd  27044  congsub  27048  congabseq  27052  acongrep  27058  acongeq  27061  jm2.18  27072  jm2.19lem1  27073  jm2.19lem2  27074  jm2.19lem3  27075  jm2.22  27079  jm2.23  27080  jm2.20nn  27081  jm2.25  27083  jm2.26lem3  27085  jm2.27c  27091  psgnunilem5  27407  psgnunilem2  27408  psgnunilem4  27410  m1expaddsub  27411  psgnuni  27412  hashgcdlem  27506  fmul01lt1lem2  27704  clim1fr1  27716  stoweidlem11  27749  stoweidlem26  27764  wallispilem5  27807  2elfz2melfz  28139  fzosplitsnm1  28153  flpmodeq  28172  swrd0fv  28225  swrdswrd0  28234  modprm0  28261  cshwidx0  28277  cshwidxm1  28278  cshweqdif2  28303  cshweqrep  28307  sineq0ALT  29122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9052
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087  df-neg 9299  df-z 10288
  Copyright terms: Public domain W3C validator