Theorem zcnd 9704

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

Step	Hyp	Ref	Expression
1		zred.1	. . 3 |- ( ph -> A e. ZZ )
2	1	zred 9703	. 2 |- ( ph -> A e. RR )
3	2	recnd 8304	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8127   ZZcz 9579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8221

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8449  df-z 9580

This theorem is referenced by:  qapne  9974  fzspl  10407  fzm1  10438  fzrevral  10443  fzshftral  10446  nn0disj  10476  fzoss2  10512  fzo0addelr  10538  elfzoext  10541  fzosubel  10543  fzosubel3  10545  fzocatel  10548  fzosplitsnm1  10558  infssuzex  10597  zsupssdc  10602  qtri3or  10604  exbtwnzlemstep  10611  exbtwnzlemex  10613  rebtwn2zlemstep  10616  rebtwn2z  10618  flqaddz  10661  flqzadd  10662  2tnp1ge0ge0  10665  ceiqm1l  10677  intqfrac2  10685  intfracq  10686  flqdiv  10687  modqvalr  10691  flqpmodeq  10693  modq0  10695  mulqmod0  10696  modqlt  10699  modqdiffl  10701  modqfrac  10703  flqmod  10704  intqfrac  10705  modqmulnn  10708  modqvalp1  10709  modqcyc  10725  modqcyc2  10726  modqadd1  10727  mulqaddmodid  10730  mulp1mod1  10731  modqmul1  10743  modqmul12d  10744  modqnegd  10745  modqmulmodr  10756  modqdi  10758  modqsubdir  10759  modfzo0difsn  10761  modsumfzodifsn  10762  addmodlteq  10764  frecfzen2  10793  uzennn  10802  uzsinds  10810  seq3shft2  10847  monoord2  10852  iseqf1olemab  10868  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seqf1oglem1  10885  seqf1oglem2  10886  expaddzaplem  10948  modqexp  11032  sqoddm1div8  11059  bcm1k  11126  bcp1nk  11128  bcpasc  11132  bcm1n  11135  hashfz  11190  hashfzo  11191  hashfzp1  11193  hashfibclem  11210  seq3coll  11218  ccatval3  11291  ccatlid  11298  ccatass  11300  ccatalpha  11305  swrdfv0  11350  swrdfv2  11359  swrds1  11364  ccatswrd  11366  pfxfv  11380  ccatpfx  11397  swrdpfx  11403  pfxccatin12lem2  11427  seq3shft  11527  fzomaxdif  11802  climshft2  11995  iserex  12028  iser3shft  12035  serf0  12041  fsumm1  12106  fsumsplitsnun  12109  fsump1  12110  fsumshftm  12135  fisumrev2  12136  telfsumo  12156  fsumparts  12160  binomlem  12173  isumshft  12180  isumsplit  12181  isum1p  12182  divcnv  12187  arisum  12188  trireciplem  12190  cvgratnnlemmn  12215  cvgratnnlemsumlt  12218  mertenslemi1  12225  ntrivcvgap  12238  fprodm1  12288  fprodp1  12290  fprodfac  12305  fprodrev  12309  fprodmodd  12331  eirraplem  12467  moddvds  12489  dvdscmulr  12510  dvdsmulcr  12511  dvds2ln  12514  dvdsadd2b  12530  dvdsaddre2b  12531  fsumdvds  12532  fzocongeq  12548  addmodlteqALT  12549  dvdsexp  12551  dvdsmod  12552  mulmoddvds  12553  3dvds  12554  odd2np1  12563  oddm1even  12565  oexpneg  12567  mulsucdiv2z  12575  zob  12581  ltoddhalfle  12583  divalglemnn  12608  divalglemqt  12609  divalglemex  12612  divalglemeuneg  12613  divalgb  12615  divalgmod  12617  modremain  12619  flodddiv4  12626  bitsp1  12641  bitsfzo  12645  bitsmod  12646  bitsinv1lem  12651  dvdsbnd  12656  gcdaddm  12684  modgcd  12691  gcdmultipled  12693  dvdsgcdidd  12694  bezoutlemnewy  12696  bezoutlemaz  12703  bezoutlembz  12704  dvdsmulgcd  12725  rplpwr  12727  uzwodc  12737  lcmval  12764  lcmcllem  12768  lcmid  12781  mulgcddvds  12795  divgcdcoprm0  12802  cncongr1  12804  cncongr2  12805  rpexp  12854  sqrt2irrlem  12862  sqrt2irrap  12881  qmuldeneqnum  12896  numdensq  12903  qden1elz  12906  hashdvds  12922  phiprm  12924  eulerthlema  12931  eulerthlemh  12932  eulerthlemth  12933  fermltl  12935  prmdiv  12936  prmdiveq  12937  hashgcdlem  12939  odzdvds  12947  modprm0  12956  modprmn0modprm0  12958  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem15  12980  pcpremul  12995  pceulem  12996  pceu  12997  pczpre  12999  pcdiv  13004  pcqmul  13005  pcqdiv  13009  pcexp  13011  pcaddlem  13041  pcadd  13042  fldivp1  13050  pcfac  13052  pcbc  13053  prmpwdvds  13057  4sqlem5  13084  4sqlem8  13087  4sqlem9  13088  4sqlem10  13089  4sqlemffi  13098  4sqexercise2  13101  4sqlemsdc  13102  4sqlem11  13103  4sqlem14  13106  4sqlem16  13108  4sqlem17  13109  ballotfilemfc0  13153  ballotfilemfcc  13154  znnen  13166  mulgsubcl  13870  mulgdirlem  13887  mulgdir  13888  mulgass  13893  mulgmodid  13895  mulgsubdir  13896  gsumfzconst  14075  gsumfzsnfd  14079  gsumsplit0  14080  zringmulg  14763  zndvds0  14815  znf1o  14816  znunit  14824  relogbexpap  15840  logbgcd1irraplemap  15851  wilthlem1  15865  lgslem1  15890  lgsval2lem  15900  lgsval4a  15912  lgsneg  15914  lgsneg1  15915  lgsmod  15916  lgsdirprm  15924  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsabs1  15929  lgssq  15930  lgssq2  15931  lgsmulsqcoprm  15936  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  gausslemma2dlem1  15951  gausslemma2dlem4  15954  gausslemma2dlem5a  15955  gausslemma2dlem5  15956  gausslemma2dlem6  15957  gausslemma2d  15959  lgseisenlem1  15960  lgseisenlem2  15961  lgseisenlem3  15962  lgseisenlem4  15963  lgsquadlem1  15967  lgsquad2lem1  15971  lgsquad3  15974  2lgslem1b  15979  2lgsoddprmlem2  15996  2sqlem3  16007  2sqlem4  16008  2sqlem8a  16012  2sqlem8  16013  clwwlkccatlem  16412  iswomni0  16853  gsumgfsumlem  16882  gsumgfsum  16883