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

Theorem zcnd 10365
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 10364 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9103 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   CCcc 8977   ZZcz 10271
This theorem is referenced by:  uzp1  10508  peano2uzr  10521  uzaddcl  10522  zsupss  10554  rpnnen1lem5  10593  fzm1  11115  fzrevral  11119  fzshftral  11122  fzoss2  11151  fzosubel  11165  fzosubel3  11167  quoremz  11224  intfrac2  11227  intfracq  11228  moddiffl  11247  modmul1  11267  modmul12d  11268  uzrdgxfr  11294  fzen2  11296  seqm1  11328  monoord2  11342  seqf1olem1  11350  seqf1olem2  11351  seqz  11359  expaddzlem  11411  modexp  11502  bcm1k  11594  bcp1nk  11596  bcval5  11597  bcpasc  11600  hashfz  11680  hashfzo  11682  hashbclem  11689  seqcoll  11700  ccatval3  11735  ccatlid  11736  ccatass  11738  swrd0val  11756  swrdid  11760  ccatswrd  11761  spllen  11771  splfv1  11772  splfv2a  11773  swrds1  11775  revccat  11786  revrev  11787  shftuz  11872  seqshft  11888  fzomaxdif  12135  climshftlem  12356  climshft  12358  climshft2  12364  iserex  12438  isercoll2  12450  serf0  12462  iseraltlem2  12464  iseraltlem3  12465  iseralt  12466  sumrblem  12493  fsumm1  12525  fsump1  12528  fsumshftm  12552  fsumrev2  12553  fsumtscopo  12569  fsumparts  12573  binomlem  12596  isumshft  12607  isumsplit  12608  isum1p  12609  arisum  12627  cvgrat  12648  mertenslem1  12649  eirrlem  12791  sqr2irrlem  12835  dvds2ln  12868  dvdsadd2b  12880  fsumdvds  12881  fzocongeq  12891  dvdsexp  12893  dvdsmod  12894  oddm1even  12897  oexpneg  12899  3dvds  12900  divalglem0  12901  divalglem4  12904  divalglem8  12908  divalgb  12912  divalgmod  12914  bitsp1  12931  bitsp1e  12932  bitsfzo  12935  bitsmod  12936  bitsinv1lem  12941  bitsf1  12946  sadaddlem  12966  bitsres  12973  bitsuz  12974  bitsshft  12975  smumullem  12992  modgcd  13024  bezoutlem1  13026  bezoutlem2  13027  bezoutlem3  13028  bezoutlem4  13029  dvdsmulgcd  13042  rplpwr  13044  mulgcddvds  13092  rpexp  13108  qmuldeneqnum  13127  numdensq  13134  qden1elz  13137  hashdvds  13152  phiprm  13154  eulerthlem2  13159  fermltl  13161  prmdiv  13162  prmdiveq  13163  odzdvds  13169  pythagtriplem6  13183  pythagtriplem7  13184  pythagtriplem15  13191  pclem  13200  pcpremul  13205  pceulem  13207  pczpre  13209  pcdiv  13214  pcqmul  13215  pcqdiv  13219  pcexp  13221  pcaddlem  13245  pcadd  13246  fldivp1  13254  pcfac  13256  pcbc  13257  prmpwdvds  13260  prmreclem4  13275  4sqlem5  13298  4sqlem8  13301  4sqlem9  13302  4sqlem10  13303  4sqlem11  13311  4sqlem14  13314  4sqlem16  13316  4sqlem17  13317  vdwapun  13330  vdwnnlem2  13352  prmlem0  13416  mulgsubcl  14892  mulgdirlem  14902  mulgdir  14903  mulgass  14908  mulgsubdir  14909  odnncl  15171  odmulg  15180  odbezout  15182  sylow1lem1  15220  sylow2alem2  15240  efgtlen  15346  efgsres  15358  efgredleme  15363  efgredlemc  15365  odadd1  15451  odadd2  15452  cyggeninv  15481  ablfacrp  15612  pgpfac1lem3  15623  zlpirlem1  16756  zlpirlem3  16758  prmirredlem  16761  zndvds0  16819  znf1o  16820  znunit  16832  tgpmulg  18111  zdis  18835  uniioombllem3  19465  mbfi1fseqlem4  19598  dvexp3  19850  aareccl  20231  aalioulem1  20237  geolim3  20244  aaliou3lem2  20248  aaliou3lem6  20253  ulmshft  20294  dvradcnv  20325  sineq0  20417  efif1olem2  20433  wilthlem1  20839  wilthlem2  20840  basellem3  20853  mumul  20952  musum  20964  musumsum  20965  muinv  20966  ppiub  20976  chtub  20984  logfac2  20989  chpchtsum  20991  dchrptlem1  21036  pcbcctr  21048  bcmono  21049  bposlem5  21060  bposlem6  21061  lgslem1  21068  lgsval2lem  21078  lgsval4a  21090  lgsneg  21091  lgsneg1  21092  lgsmod  21093  lgsdirprm  21101  lgsdir  21102  lgsdilem2  21103  lgsdi  21104  lgsne0  21105  lgsabs1  21106  lgssq  21107  lgssq2  21108  lgsdirnn0  21111  lgsdinn0  21112  lgsqrlem1  21113  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgseisenlem4  21124  lgsquadlem1  21126  lgsquad2lem1  21130  lgsquad3  21133  2sqlem3  21138  2sqlem4  21139  2sqlem8a  21143  2sqlem8  21144  2sqlem11  21147  2sqblem  21149  dchrisumlem1  21171  dchrmusum2  21176  dchrvmasumlem1  21177  dchrvmasum2lem  21178  mudivsum  21212  mulogsum  21214  mulog2sumlem2  21217  selberglem1  21227  selberglem3  21229  selberg  21230  pntpbnd2  21269  pntlemf  21287  padicabvcxp  21314  wlkdvspthlem  21595  fargshiftf1  21612  fargshiftfo  21613  eupatrl  21678  gxmodid  21855  fzspl  24137  bcm1n  24139  numdenneg  24148  divnumden2  24149  ltesubnnd  24150  zzsmulg  24253  zrhnm  24341  qqhval2lem  24353  qqhghm  24360  qqhrhm  24361  qqhnm  24362  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemic  24752  ballotlem1c  24753  ballotlemsgt1  24756  ballotlemsdom  24757  ballotlemsel1i  24758  ballotlemsf1o  24759  ballotlemsima  24761  ballotlemfrceq  24774  ballotlemfrcn0  24775  ballotlem1ri  24780  igamz  24820  divcnvlin  25200  ntrivcvg  25214  ntrivcvgtail  25217  prodrblem  25244  fprodser  25264  fprodm1  25279  fprodp1  25281  fprodshft  25289  fprodrev  25290  fallfacval3  25317  fallfacfwd  25341  0fallfac  25342  binomfallfaclem2  25345  fallfacval4  25348  predfz  25458  axlowdimlem14  25842  axlowdimlem16  25844  fsumkthpow  26050  ltflcei  26187  fdc  26386  mettrifi  26400  caushft  26404  cntotbnd  26442  mzpsubmpt  26737  lzenom  26765  diophun  26769  eqrabdioph  26773  irrapxlem2  26823  irrapxlem3  26824  pellexlem6  26834  pell1234qrreccl  26854  pellfund14  26898  rmspecsqrnq  26906  rmxyneg  26920  rmxyadd  26921  rmxp1  26932  rmxm1  26934  rmym1  26935  rmxluc  26936  rmyluc  26937  rmyluc2  26938  rmxdbl  26939  rmydbl  26940  jm2.17a  26962  congadd  26968  congsub  26972  congabseq  26976  acongrep  26982  acongeq  26985  jm2.18  26996  jm2.19lem1  26997  jm2.19lem2  26998  jm2.19lem3  26999  jm2.22  27003  jm2.23  27004  jm2.20nn  27005  jm2.25  27007  jm2.26lem3  27009  jm2.27c  27015  psgnunilem5  27332  psgnunilem2  27333  psgnunilem4  27335  m1expaddsub  27336  psgnuni  27337  hashgcdlem  27431  fmul01lt1lem2  27629  clim1fr1  27641  stoweidlem11  27674  stoweidlem26  27689  wallispilem5  27732  fzosplitsnm1  28043  flpmodeq  28056  swrdswrd0  28088  swrdccatin12c  28103  modprm0  28112  shwrdidx0  28132  shwrdidxm1  28133  shwrdeqdif2  28156
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 9036
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 5409  df-fv 5453  df-ov 6075  df-neg 9283  df-z 10272
  Copyright terms: Public domain W3C validator