Theorem zcnd 9378

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 9377	. 2 |- ( ph -> A e. RR )
3	2	recnd 7988	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7811   ZZcz 9255

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256

This theorem is referenced by:  qapne  9641  fzm1  10102  fzrevral  10107  fzshftral  10110  nn0disj  10140  fzoss2  10174  fzosubel  10196  fzosubel3  10198  fzocatel  10201  fzosplitsnm1  10211  qtri3or  10245  exbtwnzlemstep  10250  exbtwnzlemex  10252  rebtwn2zlemstep  10255  rebtwn2z  10257  flqaddz  10299  flqzadd  10300  2tnp1ge0ge0  10303  ceiqm1l  10313  intqfrac2  10321  intfracq  10322  flqdiv  10323  modqvalr  10327  flqpmodeq  10329  modq0  10331  mulqmod0  10332  modqlt  10335  modqdiffl  10337  modqfrac  10339  flqmod  10340  intqfrac  10341  modqmulnn  10344  modqvalp1  10345  modqcyc  10361  modqcyc2  10362  modqadd1  10363  mulqaddmodid  10366  mulp1mod1  10367  modqmul1  10379  modqmul12d  10380  modqnegd  10381  modqmulmodr  10392  modqdi  10394  modqsubdir  10395  modfzo0difsn  10397  modsumfzodifsn  10398  addmodlteq  10400  frecfzen2  10429  uzennn  10438  uzsinds  10444  seq3shft2  10475  monoord2  10479  iseqf1olemab  10491  seq3f1olemqsumkj  10500  seq3f1olemqsum  10502  expaddzaplem  10565  modqexp  10649  sqoddm1div8  10676  bcm1k  10742  bcp1nk  10744  bcpasc  10748  hashfz  10803  hashfzo  10804  hashfzp1  10806  seq3coll  10824  seq3shft  10849  fzomaxdif  11124  climshft2  11316  iserex  11349  iser3shft  11356  serf0  11362  fsumm1  11426  fsumsplitsnun  11429  fsump1  11430  fsumshftm  11455  fisumrev2  11456  telfsumo  11476  fsumparts  11480  binomlem  11493  isumshft  11500  isumsplit  11501  isum1p  11502  divcnv  11507  arisum  11508  trireciplem  11510  cvgratnnlemmn  11535  cvgratnnlemsumlt  11538  mertenslemi1  11545  ntrivcvgap  11558  fprodm1  11608  fprodp1  11610  fprodfac  11625  fprodrev  11629  fprodmodd  11651  eirraplem  11786  moddvds  11808  dvdscmulr  11829  dvdsmulcr  11830  dvds2ln  11833  dvdsadd2b  11849  dvdsaddre2b  11850  fzocongeq  11866  addmodlteqALT  11867  dvdsexp  11869  dvdsmod  11870  mulmoddvds  11871  odd2np1  11880  oddm1even  11882  oexpneg  11884  mulsucdiv2z  11892  zob  11898  ltoddhalfle  11900  divalglemnn  11925  divalglemqt  11926  divalglemex  11929  divalglemeuneg  11930  divalgb  11932  divalgmod  11934  modremain  11936  flodddiv4  11941  infssuzex  11952  zsupssdc  11957  dvdsbnd  11959  gcdaddm  11987  modgcd  11994  gcdmultipled  11996  dvdsgcdidd  11997  bezoutlemnewy  11999  bezoutlemaz  12006  bezoutlembz  12007  dvdsmulgcd  12028  rplpwr  12030  uzwodc  12040  lcmval  12065  lcmcllem  12069  lcmid  12082  mulgcddvds  12096  divgcdcoprm0  12103  cncongr1  12105  cncongr2  12106  rpexp  12155  sqrt2irrlem  12163  sqrt2irrap  12182  qmuldeneqnum  12197  numdensq  12204  qden1elz  12207  hashdvds  12223  phiprm  12225  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  fermltl  12236  prmdiv  12237  prmdiveq  12238  hashgcdlem  12240  odzdvds  12247  modprm0  12256  modprmn0modprm0  12258  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem15  12280  pcpremul  12295  pceulem  12296  pceu  12297  pczpre  12299  pcdiv  12304  pcqmul  12305  pcqdiv  12309  pcexp  12311  pcaddlem  12340  pcadd  12341  fldivp1  12348  pcfac  12350  pcbc  12351  prmpwdvds  12355  4sqlem5  12382  4sqlem8  12385  4sqlem9  12386  4sqlem10  12387  znnen  12401  mulgsubcl  13002  mulgdirlem  13019  mulgdir  13020  mulgass  13025  mulgmodid  13027  mulgsubdir  13028  zringmulg  13527  relogbexpap  14415  logbgcd1irraplemap  14426  lgslem1  14440  lgsval2lem  14450  lgsval4a  14462  lgsneg  14464  lgsneg1  14465  lgsmod  14466  lgsdirprm  14474  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgsabs1  14479  lgssq  14480  lgssq2  14481  lgsmulsqcoprm  14486  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem1  14489  lgseisenlem2  14490  2lgsoddprmlem2  14493  2sqlem3  14503  2sqlem4  14504  2sqlem8a  14508  2sqlem8  14509  iswomni0  14838