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

Theorem zcnd 10735
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 10734 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9399 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   CCcc 9267   ZZcz 10633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9326
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9585  df-z 10634
This theorem is referenced by:  uzp1  10881  peano2uzr  10897  uzaddcl  10898  zsupss  10931  rpnnen1lem5  10970  fzm1  11523  fzrevral  11527  fzshftral  11530  fzoss2  11560  fzosubel  11582  fzosubel3  11584  fzocatel  11585  fzosplitsnm1  11591  quoremz  11677  intfrac2  11680  intfracq  11681  flpmodeq  11696  moddiffl  11702  modmul1  11735  modmul12d  11736  uzrdgxfr  11772  fzen2  11774  seqm1  11806  monoord2  11820  seqf1olem1  11828  seqf1olem2  11829  seqz  11837  expaddzlem  11890  modexp  11982  bcm1k  12074  bcp1nk  12076  bcval5  12077  bcpasc  12080  hashfz  12171  hashfzo  12173  hashbclem  12188  seqcoll  12199  ccatval3  12261  ccatlid  12267  ccatass  12269  swrd0val  12300  swrdid  12304  swrd0fv  12318  swrdspsleq  12325  swrds1  12328  ccatswrd  12333  swrdswrd0  12339  spllen  12379  splfv1  12380  splfv2a  12381  revccat  12389  revrev  12390  cshwidxmod  12423  cshwidxm1  12426  shftuz  12541  seqshft  12557  fzomaxdif  12814  climshftlem  13035  climshft  13037  climshft2  13043  iserex  13117  isercoll2  13129  serf0  13141  iseraltlem2  13143  iseraltlem3  13144  iseralt  13145  sumrblem  13171  fsumm1  13203  fsump1  13206  fsumshftm  13230  fsumrev2  13231  fsumtscopo  13247  fsumparts  13251  binomlem  13274  isumshft  13284  isumsplit  13285  isum1p  13286  arisum  13304  cvgrat  13325  mertenslem1  13326  eirrlem  13468  sqr2irrlem  13512  dvds2ln  13545  dvdsadd2b  13557  fsumdvds  13558  fzocongeq  13569  dvdsexp  13571  dvdsmod  13572  oddm1even  13575  oexpneg  13577  3dvds  13578  divalglem0  13579  divalglem4  13582  divalglem8  13586  divalgb  13590  divalgmod  13592  bitsp1  13609  bitsfzo  13613  bitsmod  13614  bitsinv1lem  13619  bitsf1  13624  sadaddlem  13644  bitsres  13651  bitsuz  13652  bitsshft  13653  smumullem  13670  modgcd  13702  bezoutlem1  13704  bezoutlem2  13705  bezoutlem3  13706  bezoutlem4  13707  dvdsmulgcd  13720  rplpwr  13722  mulgcddvds  13772  rpexp  13788  qmuldeneqnum  13807  numdensq  13814  qden1elz  13817  hashdvds  13832  phiprm  13834  eulerthlem2  13839  fermltl  13841  prmdiv  13842  prmdiveq  13843  odzdvds  13849  modprm0  13855  modprmn0modprm0  13857  pythagtriplem6  13870  pythagtriplem7  13871  pythagtriplem15  13878  pclem  13887  pcpremul  13892  pceulem  13894  pczpre  13896  pcdiv  13901  pcqmul  13902  pcqdiv  13906  pcexp  13908  pcaddlem  13932  pcadd  13933  fldivp1  13941  pcfac  13943  pcbc  13944  prmpwdvds  13947  prmreclem4  13962  4sqlem5  13985  4sqlem8  13988  4sqlem9  13989  4sqlem10  13990  4sqlem11  13998  4sqlem14  14001  4sqlem16  14003  4sqlem17  14004  vdwapun  14017  vdwnnlem2  14039  prmlem0  14115  mulgsubcl  15620  mulgdirlem  15630  mulgdir  15631  mulgass  15636  mulgsubdir  15637  psgnunilem5  15979  psgnunilem2  15980  psgnunilem4  15982  m1expaddsub  15983  psgnuni  15984  odnncl  16027  odmulg  16036  odbezout  16038  sylow1lem1  16076  sylow2alem2  16096  efgtlen  16202  efgsres  16214  efgredleme  16219  efgredlemc  16221  odadd1  16309  odadd2  16310  cyggeninv  16339  ablfacrp  16540  pgpfac1lem3  16551  zringmulg  17732  zrngmulg  17738  zringlpirlem1  17744  zringlpirlem3  17746  zlpirlem1  17749  zlpirlem3  17751  prmirredlem  17758  prmirredlemOLD  17761  zndvds0  17824  znf1o  17825  znunit  17837  tgpmulg  19505  zdis  20234  uniioombllem3  20906  mbfi1fseqlem4  21037  dvexp3  21291  aareccl  21676  aalioulem1  21682  geolim3  21689  aaliou3lem2  21693  aaliou3lem6  21698  ulmshft  21739  dvradcnv  21770  sineq0  21867  efif1olem2  21883  wilthlem1  22290  wilthlem2  22291  basellem3  22304  mumul  22403  musum  22415  musumsum  22416  muinv  22417  ppiub  22427  chtub  22435  logfac2  22440  chpchtsum  22442  dchrptlem1  22487  pcbcctr  22499  bcmono  22500  bposlem5  22511  bposlem6  22512  lgslem1  22519  lgsval2lem  22529  lgsval4a  22541  lgsneg  22542  lgsneg1  22543  lgsmod  22544  lgsdirprm  22552  lgsdir  22553  lgsdilem2  22554  lgsdi  22555  lgsne0  22556  lgsabs1  22557  lgssq  22558  lgssq2  22559  lgsdirnn0  22562  lgsdinn0  22563  lgsqrlem1  22564  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem3  22574  lgseisenlem4  22575  lgsquadlem1  22577  lgsquad2lem1  22581  lgsquad3  22584  2sqlem3  22589  2sqlem4  22590  2sqlem8a  22594  2sqlem8  22595  2sqlem11  22598  2sqblem  22600  dchrisumlem1  22622  dchrmusum2  22627  dchrvmasumlem1  22628  dchrvmasum2lem  22629  mudivsum  22663  mulogsum  22665  mulog2sumlem2  22668  selberglem1  22678  selberglem3  22680  selberg  22681  pntpbnd2  22720  pntlemf  22738  padicabvcxp  22765  axlowdimlem14  23023  axlowdimlem16  23025  wlkdvspthlem  23328  fargshiftf1  23345  fargshiftfo  23346  eupatrl  23411  gxmodid  23588  fzspl  25899  bcm1n  25901  numdenneg  25908  divnumden2  25909  ltesubnnd  25913  archiabllem1  26033  archiabllem2c  26035  zrhnm  26251  qqhval2lem  26263  qqhghm  26270  qqhrhm  26271  qqhnm  26272  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemic  26736  ballotlem1c  26737  ballotlemsgt1  26740  ballotlemsdom  26741  ballotlemsel1i  26742  ballotlemsf1o  26743  ballotlemsima  26745  ballotlemfrceq  26758  ballotlemfrcn0  26759  ballotlem1ri  26764  signsplypnf  26798  igamz  26881  divcnvlin  27245  ntrivcvg  27258  ntrivcvgtail  27261  prodrblem  27288  fprodser  27308  fprodm1  27323  fprodp1  27325  fprodshft  27333  fprodrev  27334  fallfacval3  27361  fallfacfwd  27385  0fallfac  27386  binomfallfaclem2  27389  fallfacval4  27392  predfz  27510  fsumkthpow  28045  ltflcei  28260  fdc  28482  mettrifi  28494  caushft  28498  cntotbnd  28536  mzpsubmpt  28921  lzenom  28950  diophun  28954  eqrabdioph  28958  irrapxlem2  29006  irrapxlem3  29007  pellexlem6  29017  pell1234qrreccl  29037  pellfund14  29081  rmspecsqrnq  29089  rmxyneg  29103  rmxyadd  29104  rmxp1  29115  rmxm1  29117  rmym1  29118  rmxluc  29119  rmyluc  29120  rmyluc2  29121  rmxdbl  29122  rmydbl  29123  jm2.17a  29145  congadd  29151  congsub  29155  congabseq  29159  acongrep  29165  acongeq  29168  jm2.18  29179  jm2.19lem1  29180  jm2.19lem2  29181  jm2.19lem3  29182  jm2.22  29186  jm2.23  29187  jm2.20nn  29188  jm2.25  29190  jm2.26lem3  29192  jm2.27c  29198  hashgcdlem  29407  fmul01lt1lem2  29608  clim1fr1  29617  stoweidlem11  29649  stoweidlem26  29664  wallispilem5  29707  2elfz2melfz  30045  fsumsplitsndif  30081  fsumsplitsnun  30085  clwwisshclww  30314  cshwlemma1  30332  ztprmneprm  30580  sineq0ALT  31372
  Copyright terms: Public domain W3C validator