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

Theorem zcnd 10970
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 10969 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9620 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   CCcc 9488   ZZcz 10865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-neg 9808  df-z 10866
This theorem is referenced by:  zsupss  11175  rpnnen1lem5  11216  fzm1  11762  fzrevral  11766  fzshftral  11769  nn0disj  11794  fzoss2  11827  fzosubel  11849  fzosubel3  11851  fzocatel  11854  fzosplitsnm1  11864  quoremz  11956  intfrac2  11959  intfracq  11960  flpmodeq  11975  moddiffl  11981  modmul1  12014  modmul12d  12015  uzrdgxfr  12051  fzen2  12053  monoord2  12112  seqf1olem1  12120  seqf1olem2  12121  seqz  12129  expaddzlem  12183  modexp  12275  bcm1k  12367  bcp1nk  12369  bcval5  12370  bcpasc  12373  hashfz  12459  hashfzo  12461  hashbclem  12475  seqcoll  12486  ccatval3  12571  ccatlid  12577  ccatass  12579  swrd0val  12622  swrdid  12626  swrd0fv  12640  swrdspsleq  12647  swrds1  12650  ccatswrd  12655  swrdswrd0  12661  spllen  12704  splfv1  12705  splfv2a  12706  revccat  12714  revrev  12715  cshwidxmod  12748  cshwidxm1  12751  cshweqrep  12763  2cshwcshw  12767  seqshft  12892  fzomaxdif  13150  climshft2  13379  iserex  13453  isercoll2  13465  serf0  13477  iseraltlem2  13479  iseraltlem3  13480  iseralt  13481  sumrblem  13507  fsumm1  13540  fsumsplitsnun  13544  fsump1  13545  fsumshftm  13570  fsumrev2  13571  telfsumo  13590  fsumparts  13594  binomlem  13615  isumshft  13625  isumsplit  13626  isum1p  13627  arisum  13645  cvgrat  13666  mertenslem1  13667  eirrlem  13809  sqr2irrlem  13853  dvds2ln  13886  dvdsadd2b  13900  fsumdvds  13901  fzocongeq  13912  dvdsexp  13914  dvdsmod  13915  odd2np1  13918  oddm1even  13919  oexpneg  13921  3dvds  13922  divalglem0  13923  divalglem4  13926  divalglem8  13930  divalgb  13934  divalgmod  13936  bitsp1  13953  bitsfzo  13957  bitsmod  13958  bitsinv1lem  13963  bitsf1  13968  sadaddlem  13988  bitsres  13995  bitsuz  13996  bitsshft  13997  smumullem  14014  modgcd  14046  bezoutlem1  14048  bezoutlem2  14049  bezoutlem3  14050  bezoutlem4  14051  dvdsmulgcd  14064  rplpwr  14066  mulgcddvds  14117  rpexp  14133  qmuldeneqnum  14152  numdensq  14159  qden1elz  14162  hashdvds  14177  phiprm  14179  eulerthlem2  14184  fermltl  14186  prmdiv  14187  prmdiveq  14188  odzdvds  14194  modprm0  14202  modprmn0modprm0  14204  pythagtriplem6  14217  pythagtriplem7  14218  pythagtriplem15  14225  pcpremul  14239  pceulem  14241  pczpre  14243  pcdiv  14248  pcqmul  14249  pcqdiv  14253  pcexp  14255  pcaddlem  14279  pcadd  14280  fldivp1  14288  pcfac  14290  pcbc  14291  prmpwdvds  14294  prmreclem4  14309  4sqlem5  14332  4sqlem8  14335  4sqlem9  14336  4sqlem10  14337  4sqlem11  14345  4sqlem14  14348  4sqlem16  14350  4sqlem17  14351  vdwapun  14364  vdwnnlem2  14386  prmlem0  14463  mulgsubcl  16025  mulgdirlem  16035  mulgdir  16036  mulgass  16041  mulgsubdir  16042  psgnunilem5  16388  psgnunilem2  16389  psgnunilem4  16391  m1expaddsub  16392  psgnuni  16393  odnncl  16438  odmulg  16447  odbezout  16449  sylow1lem1  16487  sylow2alem2  16507  efgsres  16625  efgredleme  16630  efgredlemc  16632  odadd1  16723  odadd2  16724  cyggeninv  16755  gsummptshft  16825  ablfacrp  16985  pgpfac1lem3  16996  srgbinomlem3  17061  srgbinomlem4  17062  zringmulg  18364  zrngmulg  18370  zringlpirlem1  18376  zringlpirlem3  18378  zlpirlem1  18381  zlpirlem3  18383  prmirredlem  18390  prmirredlemOLD  18393  zndvds0  18456  znf1o  18457  znunit  18469  cayhamlem1  19234  tgpmulg  20458  zdis  21187  uniioombllem3  21860  mbfi1fseqlem4  21991  dvexp3  22245  aareccl  22587  aalioulem1  22593  geolim3  22600  aaliou3lem2  22604  aaliou3lem6  22609  ulmshft  22650  sineq0  22779  efif1olem2  22795  wilthlem1  23207  wilthlem2  23208  basellem3  23221  mumul  23320  musum  23332  musumsum  23333  muinv  23334  ppiub  23344  chtub  23352  logfac2  23357  chpchtsum  23359  dchrptlem1  23404  pcbcctr  23416  bcmono  23417  bposlem5  23428  bposlem6  23429  lgslem1  23436  lgsval2lem  23446  lgsval4a  23458  lgsneg  23459  lgsneg1  23460  lgsmod  23461  lgsdirprm  23469  lgsdir  23470  lgsdilem2  23471  lgsdi  23472  lgsne0  23473  lgsabs1  23474  lgssq  23475  lgssq2  23476  lgsdirnn0  23479  lgsdinn0  23480  lgsqrlem1  23481  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem3  23491  lgseisenlem4  23492  lgsquadlem1  23494  lgsquad2lem1  23498  lgsquad3  23501  2sqlem3  23506  2sqlem4  23507  2sqlem8a  23511  2sqlem8  23512  2sqlem11  23515  2sqblem  23517  dchrisumlem1  23539  dchrmusum2  23544  dchrvmasumlem1  23545  dchrvmasum2lem  23546  mudivsum  23580  mulogsum  23582  mulog2sumlem2  23585  selberglem1  23595  selberglem3  23597  selberg  23598  pntpbnd2  23637  pntlemf  23655  padicabvcxp  23682  axlowdimlem14  24123  axlowdimlem16  24125  wlkdvspthlem  24474  fargshiftf1  24502  fargshiftfo  24503  clwwisshclww  24672  eupatrl  24833  gxmodid  25146  znsqcld  27426  fzspl  27463  bcm1n  27465  numdenneg  27473  divnumden2  27474  ltesubnnd  27478  2sqn0  27500  2sqmod  27502  archiabllem1  27603  archiabllem2c  27605  zrhnm  27816  cnzh  27817  rezh  27818  qqhval2lem  27828  qqhghm  27835  qqhrhm  27836  qqhnm  27837  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemic  28311  ballotlem1c  28312  ballotlemsgt1  28315  ballotlemsdom  28316  ballotlemsel1i  28317  ballotlemsf1o  28318  ballotlemsima  28320  ballotlemfrceq  28333  ballotlemfrcn0  28334  ballotlem1ri  28339  signsplypnf  28373  igamz  28456  divcnvlin  28986  ntrivcvg  28999  ntrivcvgtail  29002  prodrblem  29029  fprodser  29049  fprodm1  29064  fprodp1  29066  fprodrev  29075  fallfacval3  29102  fallfacfwd  29126  0fallfac  29127  binomfallfaclem2  29130  fallfacval4  29133  predfz  29251  fsumkthpow  29786  ltflcei  30011  fdc  30206  mettrifi  30218  caushft  30222  cntotbnd  30260  mzpsubmpt  30643  lzenom  30671  diophun  30675  eqrabdioph  30679  irrapxlem2  30727  irrapxlem3  30728  pellexlem6  30738  pell1234qrreccl  30758  pellfund14  30802  rmxyneg  30824  rmxyadd  30825  rmxp1  30836  rmxm1  30838  rmym1  30839  rmxluc  30840  rmyluc  30841  rmyluc2  30842  rmxdbl  30843  rmydbl  30844  congadd  30872  congsub  30876  congabseq  30880  acongrep  30886  acongeq  30889  jm2.18  30898  jm2.19lem1  30899  jm2.19lem2  30900  jm2.19lem3  30901  jm2.22  30905  jm2.23  30906  jm2.20nn  30907  jm2.25  30909  jm2.26lem3  30911  jm2.27c  30917  hashgcdlem  31126  lcmid  31184  nzss  31191  hashnzfz  31194  hashnzfz2  31195  hashnzfzclim  31196  fzisoeu  31445  fperiodmul  31449  fmul01lt1lem2  31503  sumnnodd  31540  stoweidlem11  31678  stoweidlem26  31693  dirkertrigeqlem1  31765  dirkertrigeqlem2  31766  dirkertrigeqlem3  31767  dirkertrigeq  31768  dirkeritg  31769  fourierdlem26  31800  fourierdlem48  31822  fourierdlem49  31823  fourierdlem79  31853  fourierdlem91  31865  fourierdlem103  31877  fourierdlem104  31878  fouriersw  31899  2elfz2melfz  32168  fsumsplitsndif  32180  2zrngamnd  32447  2zrngacmnd  32448  2zrngagrp  32449  2zrngALT  32454  2zrngnmlid  32455  2zrngnmlid2  32457  ztprmneprm  32644  altgsumbcALT  32650  sineq0ALT  33445
  Copyright terms: Public domain W3C validator