Theorem zcnd 9602

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8029   ZZcz 9478

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  qapne  9872  fzm1  10334  fzrevral  10339  fzshftral  10342  nn0disj  10372  fzoss2  10408  fzo0addelr  10433  elfzoext  10436  fzosubel  10438  fzosubel3  10440  fzocatel  10443  fzosplitsnm1  10453  infssuzex  10492  zsupssdc  10497  qtri3or  10499  exbtwnzlemstep  10506  exbtwnzlemex  10508  rebtwn2zlemstep  10511  rebtwn2z  10513  flqaddz  10556  flqzadd  10557  2tnp1ge0ge0  10560  ceiqm1l  10572  intqfrac2  10580  intfracq  10581  flqdiv  10582  modqvalr  10586  flqpmodeq  10588  modq0  10590  mulqmod0  10591  modqlt  10594  modqdiffl  10596  modqfrac  10598  flqmod  10599  intqfrac  10600  modqmulnn  10603  modqvalp1  10604  modqcyc  10620  modqcyc2  10621  modqadd1  10622  mulqaddmodid  10625  mulp1mod1  10626  modqmul1  10638  modqmul12d  10639  modqnegd  10640  modqmulmodr  10651  modqdi  10653  modqsubdir  10654  modfzo0difsn  10656  modsumfzodifsn  10657  addmodlteq  10659  frecfzen2  10688  uzennn  10697  uzsinds  10705  seq3shft2  10742  monoord2  10747  iseqf1olemab  10763  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seqf1oglem1  10780  seqf1oglem2  10781  expaddzaplem  10843  modqexp  10927  sqoddm1div8  10954  bcm1k  11021  bcp1nk  11023  bcpasc  11027  hashfz  11084  hashfzo  11085  hashfzp1  11087  seq3coll  11105  ccatval3  11175  ccatlid  11182  ccatass  11184  ccatalpha  11189  swrdfv0  11234  swrdfv2  11243  swrds1  11248  ccatswrd  11250  pfxfv  11264  ccatpfx  11281  swrdpfx  11287  pfxccatin12lem2  11311  seq3shft  11398  fzomaxdif  11673  climshft2  11866  iserex  11899  iser3shft  11906  serf0  11912  fsumm1  11976  fsumsplitsnun  11979  fsump1  11980  fsumshftm  12005  fisumrev2  12006  telfsumo  12026  fsumparts  12030  binomlem  12043  isumshft  12050  isumsplit  12051  isum1p  12052  divcnv  12057  arisum  12058  trireciplem  12060  cvgratnnlemmn  12085  cvgratnnlemsumlt  12088  mertenslemi1  12095  ntrivcvgap  12108  fprodm1  12158  fprodp1  12160  fprodfac  12175  fprodrev  12179  fprodmodd  12201  eirraplem  12337  moddvds  12359  dvdscmulr  12380  dvdsmulcr  12381  dvds2ln  12384  dvdsadd2b  12400  dvdsaddre2b  12401  fsumdvds  12402  fzocongeq  12418  addmodlteqALT  12419  dvdsexp  12421  dvdsmod  12422  mulmoddvds  12423  3dvds  12424  odd2np1  12433  oddm1even  12435  oexpneg  12437  mulsucdiv2z  12445  zob  12451  ltoddhalfle  12453  divalglemnn  12478  divalglemqt  12479  divalglemex  12482  divalglemeuneg  12483  divalgb  12485  divalgmod  12487  modremain  12489  flodddiv4  12496  bitsp1  12511  bitsfzo  12515  bitsmod  12516  bitsinv1lem  12521  dvdsbnd  12526  gcdaddm  12554  modgcd  12561  gcdmultipled  12563  dvdsgcdidd  12564  bezoutlemnewy  12566  bezoutlemaz  12573  bezoutlembz  12574  dvdsmulgcd  12595  rplpwr  12597  uzwodc  12607  lcmval  12634  lcmcllem  12638  lcmid  12651  mulgcddvds  12665  divgcdcoprm0  12672  cncongr1  12674  cncongr2  12675  rpexp  12724  sqrt2irrlem  12732  sqrt2irrap  12751  qmuldeneqnum  12766  numdensq  12773  qden1elz  12776  hashdvds  12792  phiprm  12794  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  fermltl  12805  prmdiv  12806  prmdiveq  12807  hashgcdlem  12809  odzdvds  12817  modprm0  12826  modprmn0modprm0  12828  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem15  12850  pcpremul  12865  pceulem  12866  pceu  12867  pczpre  12869  pcdiv  12874  pcqmul  12875  pcqdiv  12879  pcexp  12881  pcaddlem  12911  pcadd  12912  fldivp1  12920  pcfac  12922  pcbc  12923  prmpwdvds  12927  4sqlem5  12954  4sqlem8  12957  4sqlem9  12958  4sqlem10  12959  4sqlemffi  12968  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem14  12976  4sqlem16  12978  4sqlem17  12979  znnen  13018  mulgsubcl  13722  mulgdirlem  13739  mulgdir  13740  mulgass  13745  mulgmodid  13747  mulgsubdir  13748  gsumfzconst  13927  gsumfzsnfd  13931  zringmulg  14611  zndvds0  14663  znf1o  14664  znunit  14672  relogbexpap  15681  logbgcd1irraplemap  15692  wilthlem1  15703  lgslem1  15728  lgsval2lem  15738  lgsval4a  15750  lgsneg  15752  lgsneg1  15753  lgsmod  15754  lgsdirprm  15762  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsabs1  15767  lgssq  15768  lgssq2  15769  lgsmulsqcoprm  15774  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem1  15789  gausslemma2dlem4  15792  gausslemma2dlem5a  15793  gausslemma2dlem5  15794  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquad2lem1  15809  lgsquad3  15812  2lgslem1b  15817  2lgsoddprmlem2  15834  2sqlem3  15845  2sqlem4  15846  2sqlem8a  15850  2sqlem8  15851  clwwlkccatlem  16250  iswomni0  16655  gsumgfsumlem  16683  gsumgfsum  16684