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

Theorem zcnd 10740
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 10739 . 2  |-  ( ph  ->  A  e.  RR )
32recnd 9404 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   CCcc 9272   ZZcz 10638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639
This theorem is referenced by:  uzp1  10886  peano2uzr  10902  uzaddcl  10903  zsupss  10936  rpnnen1lem5  10975  fzm1  11532  fzrevral  11536  fzshftral  11539  fzoss2  11569  fzosubel  11591  fzosubel3  11593  fzocatel  11594  fzosplitsnm1  11600  quoremz  11686  intfrac2  11689  intfracq  11690  flpmodeq  11705  moddiffl  11711  modmul1  11744  modmul12d  11745  uzrdgxfr  11781  fzen2  11783  seqm1  11815  monoord2  11829  seqf1olem1  11837  seqf1olem2  11838  seqz  11846  expaddzlem  11899  modexp  11991  bcm1k  12083  bcp1nk  12085  bcval5  12086  bcpasc  12089  hashfz  12180  hashfzo  12182  hashbclem  12197  seqcoll  12208  ccatval3  12270  ccatlid  12276  ccatass  12278  swrd0val  12309  swrdid  12313  swrd0fv  12327  swrdspsleq  12334  swrds1  12337  ccatswrd  12342  swrdswrd0  12348  spllen  12388  splfv1  12389  splfv2a  12390  revccat  12398  revrev  12399  cshwidxmod  12432  cshwidxm1  12435  shftuz  12550  seqshft  12566  fzomaxdif  12823  climshftlem  13044  climshft  13046  climshft2  13052  iserex  13126  isercoll2  13138  serf0  13150  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  sumrblem  13180  fsumm1  13212  fsump1  13215  fsumshftm  13240  fsumrev2  13241  fsumtscopo  13257  fsumparts  13261  binomlem  13284  isumshft  13294  isumsplit  13295  isum1p  13296  arisum  13314  cvgrat  13335  mertenslem1  13336  eirrlem  13478  sqr2irrlem  13522  dvds2ln  13555  dvdsadd2b  13567  fsumdvds  13568  fzocongeq  13579  dvdsexp  13581  dvdsmod  13582  oddm1even  13585  oexpneg  13587  3dvds  13588  divalglem0  13589  divalglem4  13592  divalglem8  13596  divalgb  13600  divalgmod  13602  bitsp1  13619  bitsfzo  13623  bitsmod  13624  bitsinv1lem  13629  bitsf1  13634  sadaddlem  13654  bitsres  13661  bitsuz  13662  bitsshft  13663  smumullem  13680  modgcd  13712  bezoutlem1  13714  bezoutlem2  13715  bezoutlem3  13716  bezoutlem4  13717  dvdsmulgcd  13730  rplpwr  13732  mulgcddvds  13782  rpexp  13798  qmuldeneqnum  13817  numdensq  13824  qden1elz  13827  hashdvds  13842  phiprm  13844  eulerthlem2  13849  fermltl  13851  prmdiv  13852  prmdiveq  13853  odzdvds  13859  modprm0  13865  modprmn0modprm0  13867  pythagtriplem6  13880  pythagtriplem7  13881  pythagtriplem15  13888  pclem  13897  pcpremul  13902  pceulem  13904  pczpre  13906  pcdiv  13911  pcqmul  13912  pcqdiv  13916  pcexp  13918  pcaddlem  13942  pcadd  13943  fldivp1  13951  pcfac  13953  pcbc  13954  prmpwdvds  13957  prmreclem4  13972  4sqlem5  13995  4sqlem8  13998  4sqlem9  13999  4sqlem10  14000  4sqlem11  14008  4sqlem14  14011  4sqlem16  14013  4sqlem17  14014  vdwapun  14027  vdwnnlem2  14049  prmlem0  14125  mulgsubcl  15632  mulgdirlem  15642  mulgdir  15643  mulgass  15648  mulgsubdir  15649  psgnunilem5  15991  psgnunilem2  15992  psgnunilem4  15994  m1expaddsub  15995  psgnuni  15996  odnncl  16039  odmulg  16048  odbezout  16050  sylow1lem1  16088  sylow2alem2  16108  efgtlen  16214  efgsres  16226  efgredleme  16231  efgredlemc  16233  odadd1  16321  odadd2  16322  cyggeninv  16351  gsummptshft  16419  ablfacrp  16557  pgpfac1lem3  16568  srgbinomlem3  16630  srgbinomlem4  16631  zringmulg  17871  zrngmulg  17877  zringlpirlem1  17883  zringlpirlem3  17885  zlpirlem1  17888  zlpirlem3  17890  prmirredlem  17897  prmirredlemOLD  17900  zndvds0  17963  znf1o  17964  znunit  17976  tgpmulg  19644  zdis  20373  uniioombllem3  21045  mbfi1fseqlem4  21176  dvexp3  21430  aareccl  21772  aalioulem1  21778  geolim3  21785  aaliou3lem2  21789  aaliou3lem6  21794  ulmshft  21835  dvradcnv  21866  sineq0  21963  efif1olem2  21979  wilthlem1  22386  wilthlem2  22387  basellem3  22400  mumul  22499  musum  22511  musumsum  22512  muinv  22513  ppiub  22523  chtub  22531  logfac2  22536  chpchtsum  22538  dchrptlem1  22583  pcbcctr  22595  bcmono  22596  bposlem5  22607  bposlem6  22608  lgslem1  22615  lgsval2lem  22625  lgsval4a  22637  lgsneg  22638  lgsneg1  22639  lgsmod  22640  lgsdirprm  22648  lgsdir  22649  lgsdilem2  22650  lgsdi  22651  lgsne0  22652  lgsabs1  22653  lgssq  22654  lgssq2  22655  lgsdirnn0  22658  lgsdinn0  22659  lgsqrlem1  22660  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem3  22670  lgseisenlem4  22671  lgsquadlem1  22673  lgsquad2lem1  22677  lgsquad3  22680  2sqlem3  22685  2sqlem4  22686  2sqlem8a  22690  2sqlem8  22691  2sqlem11  22694  2sqblem  22696  dchrisumlem1  22718  dchrmusum2  22723  dchrvmasumlem1  22724  dchrvmasum2lem  22725  mudivsum  22759  mulogsum  22761  mulog2sumlem2  22764  selberglem1  22774  selberglem3  22776  selberg  22777  pntpbnd2  22816  pntlemf  22834  padicabvcxp  22861  axlowdimlem14  23169  axlowdimlem16  23171  wlkdvspthlem  23474  fargshiftf1  23491  fargshiftfo  23492  eupatrl  23557  gxmodid  23734  fzspl  26045  bcm1n  26047  numdenneg  26054  divnumden2  26055  ltesubnnd  26059  archiabllem1  26178  archiabllem2c  26180  zrhnm  26367  qqhval2lem  26379  qqhghm  26386  qqhrhm  26387  qqhnm  26388  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemic  26858  ballotlem1c  26859  ballotlemsgt1  26862  ballotlemsdom  26863  ballotlemsel1i  26864  ballotlemsf1o  26865  ballotlemsima  26867  ballotlemfrceq  26880  ballotlemfrcn0  26881  ballotlem1ri  26886  signsplypnf  26920  igamz  27003  divcnvlin  27368  ntrivcvg  27381  ntrivcvgtail  27384  prodrblem  27411  fprodser  27431  fprodm1  27446  fprodp1  27448  fprodshft  27456  fprodrev  27457  fallfacval3  27484  fallfacfwd  27508  0fallfac  27509  binomfallfaclem2  27512  fallfacval4  27515  predfz  27633  fsumkthpow  28168  ltflcei  28390  fdc  28612  mettrifi  28624  caushft  28628  cntotbnd  28666  mzpsubmpt  29050  lzenom  29079  diophun  29083  eqrabdioph  29087  irrapxlem2  29135  irrapxlem3  29136  pellexlem6  29146  pell1234qrreccl  29166  pellfund14  29210  rmspecsqrnq  29218  rmxyneg  29232  rmxyadd  29233  rmxp1  29244  rmxm1  29246  rmym1  29247  rmxluc  29248  rmyluc  29249  rmyluc2  29250  rmxdbl  29251  rmydbl  29252  jm2.17a  29274  congadd  29280  congsub  29284  congabseq  29288  acongrep  29294  acongeq  29297  jm2.18  29308  jm2.19lem1  29309  jm2.19lem2  29310  jm2.19lem3  29311  jm2.22  29315  jm2.23  29316  jm2.20nn  29317  jm2.25  29319  jm2.26lem3  29321  jm2.27c  29327  hashgcdlem  29536  fmul01lt1lem2  29737  clim1fr1  29745  stoweidlem11  29777  stoweidlem26  29792  wallispilem5  29835  2elfz2melfz  30173  fsumsplitsndif  30209  fsumsplitsnun  30213  clwwisshclww  30442  cshwlemma1  30460  ztprmneprm  30709  altgsumbcALT  30719  sineq0ALT  31602
  Copyright terms: Public domain W3C validator