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

Theorem zcnd 10966
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 10965 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9611 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CCcc 9479   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-neg 9799  df-z 10861
This theorem is referenced by:  zsupss  11172  rpnnen1lem5  11213  fzm1  11762  fzrevral  11767  fzshftral  11770  nn0disj  11795  fzoss2  11830  fzo0addelr  11852  fzosubel  11856  fzosubel3  11858  fzocatel  11861  fzosplitsnm1  11871  quoremz  11964  intfrac2  11967  intfracq  11968  flpmodeq  11983  moddiffl  11989  modmul1  12022  modmul12d  12023  uzrdgxfr  12059  fzen2  12061  monoord2  12120  seqf1olem1  12128  seqf1olem2  12129  seqz  12137  expaddzlem  12191  modexp  12283  bcm1k  12375  bcp1nk  12377  bcval5  12378  bcpasc  12381  hashfz  12469  hashfzo  12471  hashbclem  12485  seqcoll  12496  ccatval3  12586  ccatlid  12592  ccatass  12594  swrd0val  12637  swrdid  12644  swrd0fv  12655  swrdfv2  12662  swrds1  12667  ccatswrd  12672  swrdswrd0  12678  spllen  12721  splfv1  12722  splfv2a  12723  revccat  12731  revrev  12732  cshwidxmod  12765  cshwidxm1  12768  cshweqrep  12780  2cshwcshw  12784  seqshft  13000  fzomaxdif  13258  climshft2  13487  iserex  13561  isercoll2  13573  serf0  13585  iseraltlem2  13587  iseraltlem3  13588  iseralt  13589  sumrblem  13615  fsumm1  13648  fsumsplitsnun  13652  fsump1  13653  fsumshftm  13678  fsumrev2  13679  telfsumo  13698  fsumparts  13702  binomlem  13723  isumshft  13733  isumsplit  13734  isum1p  13735  arisum  13753  cvgrat  13774  mertenslem1  13775  ntrivcvg  13788  ntrivcvgtail  13791  prodrblem  13818  fprodser  13838  fprodm1  13853  fprodp1  13855  fprodrev  13863  eirrlem  14019  sqr2irrlem  14065  dvds2ln  14098  dvdsadd2b  14112  fsumdvds  14113  fzocongeq  14124  dvdsexp  14126  dvdsmod  14127  odd2np1  14130  oddm1even  14131  oexpneg  14133  3dvds  14134  divalglem0  14135  divalglem4  14138  divalglem8  14142  divalgb  14146  divalgmod  14148  bitsp1  14165  bitsfzo  14169  bitsmod  14170  bitsinv1lem  14175  bitsf1  14180  sadaddlem  14200  bitsres  14207  bitsuz  14208  bitsshft  14209  smumullem  14226  modgcd  14258  bezoutlem1  14260  bezoutlem2  14261  bezoutlem3  14262  bezoutlem4  14263  dvdsmulgcd  14276  rplpwr  14278  mulgcddvds  14329  rpexp  14345  qmuldeneqnum  14364  numdensq  14371  qden1elz  14374  hashdvds  14389  phiprm  14391  eulerthlem2  14396  fermltl  14398  prmdiv  14399  prmdiveq  14400  odzdvds  14406  modprm0  14414  modprmn0modprm0  14416  pythagtriplem6  14429  pythagtriplem7  14430  pythagtriplem15  14437  pcpremul  14451  pceulem  14453  pczpre  14455  pcdiv  14460  pcqmul  14461  pcqdiv  14465  pcexp  14467  pcaddlem  14491  pcadd  14492  fldivp1  14500  pcfac  14502  pcbc  14503  prmpwdvds  14506  prmreclem4  14521  4sqlem5  14544  4sqlem8  14547  4sqlem9  14548  4sqlem10  14549  4sqlem11  14557  4sqlem14  14560  4sqlem16  14562  4sqlem17  14563  vdwapun  14576  vdwnnlem2  14598  prmlem0  14675  mulgsubcl  16355  mulgdirlem  16365  mulgdir  16366  mulgass  16371  mulgsubdir  16372  psgnunilem5  16718  psgnunilem2  16719  psgnunilem4  16721  m1expaddsub  16722  psgnuni  16723  odnncl  16768  odmulg  16777  odbezout  16779  sylow1lem1  16817  sylow2alem2  16837  efgsres  16955  efgredleme  16960  efgredlemc  16962  odadd1  17053  odadd2  17054  cyggeninv  17085  gsummptshft  17154  ablfacrp  17312  pgpfac1lem3  17323  srgbinomlem3  17388  srgbinomlem4  17389  zringmulg  18691  zringlpirlem1  18697  zringlpirlem3  18699  prmirredlem  18705  zndvds0  18762  znf1o  18763  znunit  18775  cayhamlem1  19534  tgpmulg  20758  zdis  21487  uniioombllem3  22160  mbfi1fseqlem4  22291  dvexp3  22545  aareccl  22888  aalioulem1  22894  geolim3  22901  aaliou3lem2  22905  aaliou3lem6  22910  ulmshft  22951  sineq0  23080  efif1olem2  23096  wilthlem1  23540  wilthlem2  23541  basellem3  23554  mumul  23653  musum  23665  musumsum  23666  muinv  23667  ppiub  23677  chtub  23685  logfac2  23690  chpchtsum  23692  dchrptlem1  23737  pcbcctr  23749  bcmono  23750  bposlem5  23761  bposlem6  23762  lgslem1  23769  lgsval2lem  23779  lgsval4a  23791  lgsneg  23792  lgsneg1  23793  lgsmod  23794  lgsdirprm  23802  lgsdir  23803  lgsdilem2  23804  lgsdi  23805  lgsne0  23806  lgsabs1  23807  lgssq  23808  lgssq2  23809  lgsdirnn0  23812  lgsdinn0  23813  lgsqrlem1  23814  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgseisenlem4  23825  lgsquadlem1  23827  lgsquad2lem1  23831  lgsquad3  23834  2sqlem3  23839  2sqlem4  23840  2sqlem8a  23844  2sqlem8  23845  2sqlem11  23848  2sqblem  23850  dchrisumlem1  23872  dchrmusum2  23877  dchrvmasumlem1  23878  dchrvmasum2lem  23879  mudivsum  23913  mulogsum  23915  mulog2sumlem2  23918  selberglem1  23928  selberglem3  23930  selberg  23931  pntpbnd2  23970  pntlemf  23988  padicabvcxp  24015  axlowdimlem14  24460  axlowdimlem16  24462  wlkdvspthlem  24811  fargshiftf1  24839  fargshiftfo  24840  clwwisshclww  25009  eupatrl  25170  gxmodid  25479  znsqcld  27792  fzspl  27832  bcm1n  27834  numdenneg  27842  divnumden2  27843  ltesubnnd  27846  2sqn0  27868  2sqmod  27870  archiabllem1  27971  archiabllem2c  27973  zrhnm  28184  cnzh  28185  rezh  28186  qqhval2lem  28196  qqhghm  28203  qqhrhm  28204  qqhnm  28205  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemic  28709  ballotlem1c  28710  ballotlemsgt1  28713  ballotlemsdom  28714  ballotlemsel1i  28715  ballotlemsf1o  28716  ballotlemsima  28718  ballotlemfrceq  28731  ballotlemfrcn0  28732  ballotlem1ri  28737  signsplypnf  28771  igamz  28854  divcnvlin  29359  fallfacval3  29375  fallfacfwd  29399  0fallfac  29400  binomfallfaclem2  29403  fallfacval4  29406  predfz  29523  fsumkthpow  30046  ltflcei  30283  fdc  30478  mettrifi  30490  caushft  30494  cntotbnd  30532  mzpsubmpt  30915  lzenom  30942  diophun  30946  eqrabdioph  30950  irrapxlem2  30998  irrapxlem3  30999  pellexlem6  31009  pell1234qrreccl  31029  pellfund14  31073  rmxyneg  31095  rmxyadd  31096  rmxp1  31107  rmxm1  31109  rmym1  31110  rmxluc  31111  rmyluc  31112  rmyluc2  31113  rmxdbl  31114  rmydbl  31115  congadd  31143  congsub  31147  congabseq  31151  acongrep  31157  acongeq  31160  jm2.18  31169  jm2.19lem1  31170  jm2.19lem2  31171  jm2.19lem3  31172  jm2.22  31176  jm2.23  31177  jm2.20nn  31178  jm2.25  31180  jm2.26lem3  31182  jm2.27c  31188  hashgcdlem  31398  lcmid  31456  nzss  31463  hashnzfz  31466  hashnzfz2  31467  hashnzfzclim  31468  uzmptshftfval  31492  fzisoeu  31739  fperiodmul  31743  fmul01lt1lem2  31818  sumnnodd  31875  dvdsn1add  31975  dvnmul  31979  dvnprodlem1  31982  stoweidlem11  32032  stoweidlem26  32047  dirkertrigeqlem1  32119  dirkertrigeqlem2  32120  dirkertrigeqlem3  32121  dirkertrigeq  32122  dirkeritg  32123  fourierdlem26  32154  fourierdlem48  32176  fourierdlem49  32177  fourierdlem79  32207  fourierdlem91  32219  fourierdlem103  32231  fourierdlem104  32232  fouriersw  32253  etransclem1  32257  etransclem4  32260  etransclem8  32264  etransclem9  32265  etransclem15  32271  etransclem17  32273  etransclem18  32274  etransclem20  32276  etransclem21  32277  etransclem22  32278  etransclem23  32279  etransclem24  32280  etransclem25  32281  etransclem35  32291  etransclem38  32294  etransclem41  32297  etransclem44  32300  etransclem45  32301  etransclem46  32302  etransclem47  32303  etransclem48  32304  mod2eq1n2dvds  32534  elmod2  32535  zob  32548  dfodd6  32552  onego  32560  zofldiv2ALTV  32573  oddflALTV  32574  oexpnegALTV  32583  omoeALTV  32591  omeoALTV  32592  pfxfv  32627  ccatpfx  32637  pfxccatin12lem2  32652  2elfz2melfz  32708  fsumsplitsndif  32718  2zrngamnd  33001  2zrngacmnd  33002  2zrngagrp  33003  2zrngALT  33008  2zrngnmlid  33009  2zrngnmlid2  33011  ztprmneprm  33190  altgsumbcALT  33196  fldivmod  33385  m1modmmod  33388  zofldiv2  33402  fllogbd  33435  nnpw2blen  33455  blen1b  33463  blennngt2o2  33467  blennn0e2  33469  dig2nn1st  33480  dignn0flhalflem1  33490  sineq0ALT  34138
  Copyright terms: Public domain W3C validator