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

Theorem zcnd 11064
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 11063 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9687 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   CCcc 9555   ZZcz 10961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-resscn 9614
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597  df-ov 6311  df-neg 9883  df-z 10962
This theorem is referenced by:  zsupss  11276  rpnnen1lem5  11317  fzm1  11900  fzrevral  11905  fzshftral  11908  nn0disj  11932  predfz  11941  fzoss2  11973  fzo0addelr  11998  fzosubel  12002  fzosubel3  12004  fzocatel  12007  fzosplitsnm1  12017  elfzom1elp1fzo1  12040  quoremz  12115  intfrac2  12118  intfracq  12119  flpmodeq  12134  moddiffl  12141  modmul1  12177  modmul12d  12178  modfzo0difsn  12195  modsumfzodifsn  12196  addmodlteq  12198  uzrdgxfr  12218  fzen2  12220  monoord2  12282  seqf1olem1  12290  seqf1olem2  12291  seqz  12299  expaddzlem  12353  modexp  12445  bcm1k  12538  bcp1nk  12540  bcval5  12541  bcpasc  12544  hashfz  12640  hashfzo  12642  hashbclem  12656  seqcoll  12668  ccatval3  12775  ccatlid  12781  ccatass  12783  ccatalpha  12787  swrd0val  12831  swrdid  12838  swrd0fv  12849  swrdfv2  12856  swrds1  12861  ccatswrd  12866  swrdswrd0  12872  spllen  12915  splfv1  12916  splfv2a  12917  revccat  12925  revrev  12926  cshwidxmod  12959  cshwidxm1  12963  cshweqrep  12977  2cshwcshw  12981  cshimadifsn0  12986  seqshft  13225  fzomaxdif  13483  climshft2  13723  iserex  13797  isercoll2  13809  serf0  13824  iseraltlem2  13826  iseraltlem3  13827  iseralt  13828  sumrblem  13854  fsumm1  13889  fsumsplitsnun  13893  fsump1  13894  fsumshftm  13919  fsumrev2  13920  telfsumo  13939  fsumparts  13943  binomlem  13964  isumshft  13974  isumsplit  13975  isum1p  13976  arisum  13995  cvgrat  14016  mertenslem1  14017  ntrivcvg  14030  ntrivcvgtail  14033  prodrblem  14060  fprodser  14080  fprodm1  14098  fprodp1  14100  fprodrev  14108  fallfacval3  14142  fallfacfwd  14166  0fallfac  14167  binomfallfaclem2  14170  fallfacval4  14173  fsumkthpow  14186  eirrlem  14333  sqr2irrlem  14377  dvds2ln  14410  dvdsadd2b  14424  fsumdvds  14425  fzocongeq  14436  addmodlteqALT  14437  dvdsexp  14439  dvdsmod  14440  odd2np1  14443  oddm1even  14444  oexpneg  14446  3dvds  14448  divalglem0  14450  divalglem4  14454  divalglem8  14459  divalgb  14464  divalgmod  14466  bitsp1  14483  bitsfzo  14488  bitsmod  14489  bitsinv1lem  14494  bitsf1  14499  sadaddlem  14519  bitsres  14526  bitsuz  14527  bitsshft  14528  smumullem  14545  modgcd  14579  bezoutlem1  14582  bezoutlem2OLD  14583  bezoutlem3OLD  14584  bezoutlem4OLD  14585  bezoutlem2  14586  bezoutlem3  14587  bezoutlem4  14588  dvdsmulgcd  14601  rplpwr  14603  lcmid  14653  absprodnn  14667  mulgcddvds  14740  rpexp  14751  qmuldeneqnum  14775  numdensq  14782  qden1elz  14785  hashdvds  14802  phiprm  14804  eulerthlem2  14809  fermltl  14811  prmdiv  14812  prmdiveq  14813  odzdvds  14819  odzdvdsOLD  14825  vfermltlALT  14832  modprm0  14835  modprmn0modprm0  14837  pythagtriplem6  14850  pythagtriplem7  14851  pythagtriplem15  14858  pcpremul  14872  pceulem  14874  pczpre  14876  pcdiv  14881  pcqmul  14882  pcqdiv  14886  pcexp  14888  pcaddlem  14912  pcadd  14913  fldivp1  14921  pcfac  14923  pcbc  14924  prmpwdvds  14927  prmreclem4  14942  4sqlem5  14965  4sqlem8  14968  4sqlem9  14969  4sqlem10  14970  4sqlem11  14978  4sqlem14OLD  14981  4sqlem16OLD  14983  4sqlem17OLD  14984  4sqlem14  14987  4sqlem16  14989  4sqlem17  14990  vdwapun  15003  vdwnnlem2  15025  prmop1  15075  prmdvdsprmo  15079  prmdvdsprmorOLD  15094  prmgaplem7  15106  prmlem0  15155  mulgsubcl  16850  mulgdirlem  16860  mulgdir  16861  mulgass  16866  mulgsubdir  16867  psgnunilem5  17213  psgnunilem2  17214  psgnunilem4  17216  m1expaddsub  17217  psgnuni  17218  odnncl  17272  odmulg  17285  odbezout  17287  sylow1lem1  17328  sylow2alem2  17348  efgsres  17466  efgredleme  17471  efgredlemc  17473  odadd1  17564  odadd2  17565  cyggeninv  17596  gsummptshft  17647  ablfacrp  17777  pgpfac1lem3  17788  srgbinomlem3  17853  srgbinomlem4  17854  zringmulg  19124  zringlpirlem1  19130  zringlpirlem3OLD  19132  zringlpirlem3  19134  prmirredlem  19141  zndvds0  19198  znf1o  19199  znunit  19211  cayhamlem1  19967  tgpmulg  21186  zdis  21912  uniioombllem3  22622  mbfi1fseqlem4  22755  dvexp3  23009  aareccl  23361  aalioulem1  23367  geolim3  23374  aaliou3lem2  23378  aaliou3lem6  23383  ulmshft  23424  sineq0  23555  efif1olem2  23571  igamz  24052  wilthlem1  24072  wilthlem2  24073  basellem3  24088  mumul  24187  musum  24199  musumsum  24200  muinv  24201  ppiub  24211  chtub  24219  logfac2  24224  chpchtsum  24226  dchrptlem1  24271  pcbcctr  24283  bcmono  24284  bposlem5  24295  bposlem6  24296  lgslem1  24303  lgsval2lem  24313  lgsval4a  24325  lgsneg  24326  lgsneg1  24327  lgsmod  24328  lgsdirprm  24336  lgsdir  24337  lgsdilem2  24338  lgsdi  24339  lgsne0  24340  lgsabs1  24341  lgssq  24342  lgssq2  24343  lgsdirnn0  24346  lgsdinn0  24347  lgsqrlem1  24348  lgseisenlem1  24356  lgseisenlem2  24357  lgseisenlem3  24358  lgseisenlem4  24359  lgsquadlem1  24361  lgsquad2lem1  24365  lgsquad3  24368  2sqlem3  24373  2sqlem4  24374  2sqlem8a  24378  2sqlem8  24379  2sqlem11  24382  2sqblem  24384  dchrisumlem1  24406  dchrmusum2  24411  dchrvmasumlem1  24412  dchrvmasum2lem  24413  mudivsum  24447  mulogsum  24449  mulog2sumlem2  24452  selberglem1  24462  selberglem3  24464  selberg  24465  pntpbnd2  24504  pntlemf  24522  padicabvcxp  24549  axlowdimlem14  25064  axlowdimlem16  25066  wlkdvspthlem  25416  fargshiftf1  25444  fargshiftfo  25445  clwwisshclww  25614  eupatrl  25775  gxmodid  26088  znsqcld  28398  fzspl  28443  bcm1n  28446  numdenneg  28455  divnumden2  28456  ltesubnnd  28460  2sqn0  28482  2sqmod  28484  archiabllem1  28584  archiabllem2c  28586  zrhnm  28847  cnzh  28848  rezh  28849  qqhval2lem  28859  qqhghm  28866  qqhrhm  28867  qqhnm  28868  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemic  29412  ballotlem1c  29413  ballotlemsgt1  29416  ballotlemsdom  29417  ballotlemsel1i  29418  ballotlemsf1o  29419  ballotlemsima  29421  ballotlemfrceq  29434  ballotlemfrcn0  29435  ballotlem1ri  29440  ballotlemicOLD  29450  ballotlem1cOLD  29451  ballotlemsgt1OLD  29454  ballotlemsdomOLD  29455  ballotlemsel1iOLD  29456  ballotlemsf1oOLD  29457  ballotlemsimaOLD  29459  ballotlemfrceqOLD  29472  ballotlemfrcn0OLD  29473  ballotlem1riOLD  29478  signsplypnf  29511  divcnvlin  30438  fwddifnp1  31003  ltflcei  31997  poimirlem1  32005  poimirlem2  32006  poimirlem7  32011  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem24  32028  poimirlem31  32035  poimirlem32  32036  fdc  32138  mettrifi  32150  caushft  32154  cntotbnd  32192  mzpsubmpt  35656  lzenom  35683  diophun  35687  eqrabdioph  35691  irrapxlem2  35738  irrapxlem3  35739  pellexlem6  35749  pell1234qrreccl  35771  pellfund14  35817  rmxyneg  35839  rmxyadd  35840  rmxp1  35851  rmxm1  35853  rmym1  35854  rmxluc  35855  rmyluc  35856  rmyluc2  35857  rmxdbl  35858  rmydbl  35859  congadd  35887  congsub  35891  congabseq  35895  acongrep  35901  acongeq  35904  jm2.18  35914  jm2.19lem1  35915  jm2.19lem2  35916  jm2.19lem3  35917  jm2.22  35921  jm2.23  35922  jm2.20nn  35923  jm2.25  35925  jm2.26lem3  35927  jm2.27c  35933  hashgcdlem  36145  nzss  36736  hashnzfz  36739  hashnzfz2  36740  hashnzfzclim  36741  uzmptshftfval  36765  sineq0ALT  37397  fzisoeu  37606  fperiodmul  37610  fmul01lt1lem2  37760  sumnnodd  37807  dvdsn1add  37911  dvnmul  37915  dvnprodlem1  37918  stoweidlem11  37983  stoweidlem26  37998  dirkertrigeqlem1  38072  dirkertrigeqlem2  38073  dirkertrigeqlem3  38074  dirkertrigeq  38075  dirkeritg  38076  fourierdlem26  38107  fourierdlem48  38130  fourierdlem49  38131  fourierdlem79  38161  fourierdlem91  38173  fourierdlem103  38185  fourierdlem104  38186  fouriersw  38207  etransclem1  38212  etransclem4  38215  etransclem8  38219  etransclem9  38220  etransclem15  38226  etransclem17  38228  etransclem18  38229  etransclem20  38231  etransclem21  38232  etransclem22  38233  etransclem23  38234  etransclem24  38235  etransclem25  38236  etransclem35  38246  etransclem38  38249  etransclem41  38252  etransclem44  38255  etransclem45  38256  etransclem46  38257  etransclem47  38258  etransclem48OLD  38259  etransclem48  38260  mod2eq1n2dvds  38870  elmod2OLD  38871  iccpartgtprec  38879  zob  38908  dfodd6  38912  onego  38921  m1expoddALTV  38923  zofldiv2ALTV  38936  oddflALTV  38937  oexpnegALTV  38951  omoeALTV  38959  omeoALTV  38960  epoo  38975  emoo  38976  epee  38977  emee  38978  evensumeven  38979  bgoldbst  39024  sgoldbaltlem2  39026  nnsum3primesprm  39030  nnsum4primesodd  39036  nnsum4primesoddALTV  39037  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbndlem2  39046  bgoldbtbndlem4  39048  bgoldbtbnd  39049  modexp2m1d  39057  pfxfv  39087  ccatpfx  39097  pfxccatin12lem2  39112  2elfz2melfz  39203  fsumsplitsndif  39242  pthdadjvtx  39923  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem5  39992  crctcshlem4  39998  crctcsh  40002  eucrctshift  40155  2zrngamnd  40449  2zrngacmnd  40450  2zrngagrp  40451  2zrngALT  40456  2zrngnmlid  40457  2zrngnmlid2  40459  ztprmneprm  40636  altgsumbcALT  40642  fldivmod  40829  m1modmmod  40832  zofldiv2  40846  fllogbd  40879  nnpw2blen  40899  blen1b  40907  blennngt2o2  40911  blennn0e2  40913  dig2nn1st  40924  dignn0flhalflem1  40934
  Copyright terms: Public domain W3C validator