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

Theorem zcnd 10366
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 10365 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9104 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8978   ZZcz 10272
This theorem is referenced by:  uzp1  10509  peano2uzr  10522  uzaddcl  10523  zsupss  10555  rpnnen1lem5  10594  fzm1  11117  fzrevral  11121  fzshftral  11124  fzoss2  11153  fzosubel  11167  fzosubel3  11169  quoremz  11226  intfrac2  11229  intfracq  11230  moddiffl  11249  modmul1  11269  modmul12d  11270  uzrdgxfr  11296  fzen2  11298  seqm1  11330  monoord2  11344  seqf1olem1  11352  seqf1olem2  11353  seqz  11361  expaddzlem  11413  modexp  11504  bcm1k  11596  bcp1nk  11598  bcval5  11599  bcpasc  11602  hashfz  11682  hashfzo  11684  hashbclem  11691  seqcoll  11702  ccatval3  11737  ccatlid  11738  ccatass  11740  swrd0val  11758  swrdid  11762  ccatswrd  11763  spllen  11773  splfv1  11774  splfv2a  11775  swrds1  11777  revccat  11788  revrev  11789  shftuz  11874  seqshft  11890  fzomaxdif  12137  climshftlem  12358  climshft  12360  climshft2  12366  iserex  12440  isercoll2  12452  serf0  12464  iseraltlem2  12466  iseraltlem3  12467  iseralt  12468  sumrblem  12495  fsumm1  12527  fsump1  12530  fsumshftm  12554  fsumrev2  12555  fsumtscopo  12571  fsumparts  12575  binomlem  12598  isumshft  12609  isumsplit  12610  isum1p  12611  arisum  12629  cvgrat  12650  mertenslem1  12651  eirrlem  12793  sqr2irrlem  12837  dvds2ln  12870  dvdsadd2b  12882  fsumdvds  12883  fzocongeq  12893  dvdsexp  12895  dvdsmod  12896  oddm1even  12899  oexpneg  12901  3dvds  12902  divalglem0  12903  divalglem4  12906  divalglem8  12910  divalgb  12914  divalgmod  12916  bitsp1  12933  bitsp1e  12934  bitsfzo  12937  bitsmod  12938  bitsinv1lem  12943  bitsf1  12948  sadaddlem  12968  bitsres  12975  bitsuz  12976  bitsshft  12977  smumullem  12994  modgcd  13026  bezoutlem1  13028  bezoutlem2  13029  bezoutlem3  13030  bezoutlem4  13031  dvdsmulgcd  13044  rplpwr  13046  mulgcddvds  13094  rpexp  13110  qmuldeneqnum  13129  numdensq  13136  qden1elz  13139  hashdvds  13154  phiprm  13156  eulerthlem2  13161  fermltl  13163  prmdiv  13164  prmdiveq  13165  odzdvds  13171  pythagtriplem6  13185  pythagtriplem7  13186  pythagtriplem15  13193  pclem  13202  pcpremul  13207  pceulem  13209  pczpre  13211  pcdiv  13216  pcqmul  13217  pcqdiv  13221  pcexp  13223  pcaddlem  13247  pcadd  13248  fldivp1  13256  pcfac  13258  pcbc  13259  prmpwdvds  13262  prmreclem4  13277  4sqlem5  13300  4sqlem8  13303  4sqlem9  13304  4sqlem10  13305  4sqlem11  13313  4sqlem14  13316  4sqlem16  13318  4sqlem17  13319  vdwapun  13332  vdwnnlem2  13354  prmlem0  13418  mulgsubcl  14894  mulgdirlem  14904  mulgdir  14905  mulgass  14910  mulgsubdir  14911  odnncl  15173  odmulg  15182  odbezout  15184  sylow1lem1  15222  sylow2alem2  15242  efgtlen  15348  efgsres  15360  efgredleme  15365  efgredlemc  15367  odadd1  15453  odadd2  15454  cyggeninv  15483  ablfacrp  15614  pgpfac1lem3  15625  zlpirlem1  16758  zlpirlem3  16760  prmirredlem  16763  zndvds0  16821  znf1o  16822  znunit  16834  tgpmulg  18113  zdis  18837  uniioombllem3  19467  mbfi1fseqlem4  19600  dvexp3  19852  aareccl  20233  aalioulem1  20239  geolim3  20246  aaliou3lem2  20250  aaliou3lem6  20255  ulmshft  20296  dvradcnv  20327  sineq0  20419  efif1olem2  20435  wilthlem1  20841  wilthlem2  20842  basellem3  20855  mumul  20954  musum  20966  musumsum  20967  muinv  20968  ppiub  20978  chtub  20986  logfac2  20991  chpchtsum  20993  dchrptlem1  21038  pcbcctr  21050  bcmono  21051  bposlem5  21062  bposlem6  21063  lgslem1  21070  lgsval2lem  21080  lgsval4a  21092  lgsneg  21093  lgsneg1  21094  lgsmod  21095  lgsdirprm  21103  lgsdir  21104  lgsdilem2  21105  lgsdi  21106  lgsne0  21107  lgsabs1  21108  lgssq  21109  lgssq2  21110  lgsdirnn0  21113  lgsdinn0  21114  lgsqrlem1  21115  lgseisenlem1  21123  lgseisenlem2  21124  lgseisenlem3  21125  lgseisenlem4  21126  lgsquadlem1  21128  lgsquad2lem1  21132  lgsquad3  21135  2sqlem3  21140  2sqlem4  21141  2sqlem8a  21145  2sqlem8  21146  2sqlem11  21149  2sqblem  21151  dchrisumlem1  21173  dchrmusum2  21178  dchrvmasumlem1  21179  dchrvmasum2lem  21180  mudivsum  21214  mulogsum  21216  mulog2sumlem2  21219  selberglem1  21229  selberglem3  21231  selberg  21232  pntpbnd2  21271  pntlemf  21289  padicabvcxp  21316  wlkdvspthlem  21597  fargshiftf1  21614  fargshiftfo  21615  eupatrl  21680  gxmodid  21857  fzspl  24139  bcm1n  24141  numdenneg  24150  divnumden2  24151  ltesubnnd  24152  zzsmulg  24255  zrhnm  24343  qqhval2lem  24355  qqhghm  24362  qqhrhm  24363  qqhnm  24364  ballotlemfc0  24740  ballotlemfcc  24741  ballotlemic  24754  ballotlem1c  24755  ballotlemsgt1  24758  ballotlemsdom  24759  ballotlemsel1i  24760  ballotlemsf1o  24761  ballotlemsima  24763  ballotlemfrceq  24776  ballotlemfrcn0  24777  ballotlem1ri  24782  igamz  24822  divcnvlin  25202  ntrivcvg  25215  ntrivcvgtail  25218  prodrblem  25245  fprodser  25265  fprodm1  25280  fprodp1  25282  fprodshft  25290  fprodrev  25291  fallfacval3  25318  fallfacfwd  25342  0fallfac  25343  binomfallfaclem2  25346  fallfacval4  25349  predfz  25463  axlowdimlem14  25859  axlowdimlem16  25861  fsumkthpow  26067  ltflcei  26204  fdc  26403  mettrifi  26417  caushft  26421  cntotbnd  26459  mzpsubmpt  26754  lzenom  26782  diophun  26786  eqrabdioph  26790  irrapxlem2  26840  irrapxlem3  26841  pellexlem6  26851  pell1234qrreccl  26871  pellfund14  26915  rmspecsqrnq  26923  rmxyneg  26937  rmxyadd  26938  rmxp1  26949  rmxm1  26951  rmym1  26952  rmxluc  26953  rmyluc  26954  rmyluc2  26955  rmxdbl  26956  rmydbl  26957  jm2.17a  26979  congadd  26985  congsub  26989  congabseq  26993  acongrep  26999  acongeq  27002  jm2.18  27013  jm2.19lem1  27014  jm2.19lem2  27015  jm2.19lem3  27016  jm2.22  27020  jm2.23  27021  jm2.20nn  27022  jm2.25  27024  jm2.26lem3  27026  jm2.27c  27032  psgnunilem5  27349  psgnunilem2  27350  psgnunilem4  27352  m1expaddsub  27353  psgnuni  27354  hashgcdlem  27448  fmul01lt1lem2  27646  clim1fr1  27658  stoweidlem11  27691  stoweidlem26  27706  wallispilem5  27749  2elfz2melfz  28065  fzosplitsnm1  28078  flpmodeq  28092  swrdswrd0  28131  modprm0  28158  cshwidx0  28174  cshwidxm1  28175  cshweqdif2  28197  cshweqrep  28201  sineq0ALT  28950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-resscn 9037
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-neg 9284  df-z 10273
  Copyright terms: Public domain W3C validator