Theorem zcnd 9570

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 7997   ZZcz 9446

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8091

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004  df-neg 8320  df-z 9447

This theorem is referenced by:  qapne  9834  fzm1  10296  fzrevral  10301  fzshftral  10304  nn0disj  10334  fzoss2  10370  fzo0addelr  10395  elfzoext  10398  fzosubel  10400  fzosubel3  10402  fzocatel  10405  fzosplitsnm1  10415  infssuzex  10453  zsupssdc  10458  qtri3or  10460  exbtwnzlemstep  10467  exbtwnzlemex  10469  rebtwn2zlemstep  10472  rebtwn2z  10474  flqaddz  10517  flqzadd  10518  2tnp1ge0ge0  10521  ceiqm1l  10533  intqfrac2  10541  intfracq  10542  flqdiv  10543  modqvalr  10547  flqpmodeq  10549  modq0  10551  mulqmod0  10552  modqlt  10555  modqdiffl  10557  modqfrac  10559  flqmod  10560  intqfrac  10561  modqmulnn  10564  modqvalp1  10565  modqcyc  10581  modqcyc2  10582  modqadd1  10583  mulqaddmodid  10586  mulp1mod1  10587  modqmul1  10599  modqmul12d  10600  modqnegd  10601  modqmulmodr  10612  modqdi  10614  modqsubdir  10615  modfzo0difsn  10617  modsumfzodifsn  10618  addmodlteq  10620  frecfzen2  10649  uzennn  10658  uzsinds  10666  seq3shft2  10703  monoord2  10708  iseqf1olemab  10724  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seqf1oglem1  10741  seqf1oglem2  10742  expaddzaplem  10804  modqexp  10888  sqoddm1div8  10915  bcm1k  10982  bcp1nk  10984  bcpasc  10988  hashfz  11043  hashfzo  11044  hashfzp1  11046  seq3coll  11064  ccatval3  11134  ccatlid  11141  ccatass  11143  swrdfv0  11186  swrdfv2  11195  swrds1  11200  ccatswrd  11202  pfxfv  11216  ccatpfx  11233  swrdpfx  11239  pfxccatin12lem2  11263  seq3shft  11349  fzomaxdif  11624  climshft2  11817  iserex  11850  iser3shft  11857  serf0  11863  fsumm1  11927  fsumsplitsnun  11930  fsump1  11931  fsumshftm  11956  fisumrev2  11957  telfsumo  11977  fsumparts  11981  binomlem  11994  isumshft  12001  isumsplit  12002  isum1p  12003  divcnv  12008  arisum  12009  trireciplem  12011  cvgratnnlemmn  12036  cvgratnnlemsumlt  12039  mertenslemi1  12046  ntrivcvgap  12059  fprodm1  12109  fprodp1  12111  fprodfac  12126  fprodrev  12130  fprodmodd  12152  eirraplem  12288  moddvds  12310  dvdscmulr  12331  dvdsmulcr  12332  dvds2ln  12335  dvdsadd2b  12351  dvdsaddre2b  12352  fsumdvds  12353  fzocongeq  12369  addmodlteqALT  12370  dvdsexp  12372  dvdsmod  12373  mulmoddvds  12374  3dvds  12375  odd2np1  12384  oddm1even  12386  oexpneg  12388  mulsucdiv2z  12396  zob  12402  ltoddhalfle  12404  divalglemnn  12429  divalglemqt  12430  divalglemex  12433  divalglemeuneg  12434  divalgb  12436  divalgmod  12438  modremain  12440  flodddiv4  12447  bitsp1  12462  bitsfzo  12466  bitsmod  12467  bitsinv1lem  12472  dvdsbnd  12477  gcdaddm  12505  modgcd  12512  gcdmultipled  12514  dvdsgcdidd  12515  bezoutlemnewy  12517  bezoutlemaz  12524  bezoutlembz  12525  dvdsmulgcd  12546  rplpwr  12548  uzwodc  12558  lcmval  12585  lcmcllem  12589  lcmid  12602  mulgcddvds  12616  divgcdcoprm0  12623  cncongr1  12625  cncongr2  12626  rpexp  12675  sqrt2irrlem  12683  sqrt2irrap  12702  qmuldeneqnum  12717  numdensq  12724  qden1elz  12727  hashdvds  12743  phiprm  12745  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  fermltl  12756  prmdiv  12757  prmdiveq  12758  hashgcdlem  12760  odzdvds  12768  modprm0  12777  modprmn0modprm0  12779  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem15  12801  pcpremul  12816  pceulem  12817  pceu  12818  pczpre  12820  pcdiv  12825  pcqmul  12826  pcqdiv  12830  pcexp  12832  pcaddlem  12862  pcadd  12863  fldivp1  12871  pcfac  12873  pcbc  12874  prmpwdvds  12878  4sqlem5  12905  4sqlem8  12908  4sqlem9  12909  4sqlem10  12910  4sqlemffi  12919  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem14  12927  4sqlem16  12929  4sqlem17  12930  znnen  12969  mulgsubcl  13673  mulgdirlem  13690  mulgdir  13691  mulgass  13696  mulgmodid  13698  mulgsubdir  13699  gsumfzconst  13878  gsumfzsnfd  13882  zringmulg  14562  zndvds0  14614  znf1o  14615  znunit  14623  relogbexpap  15632  logbgcd1irraplemap  15643  wilthlem1  15654  lgslem1  15679  lgsval2lem  15689  lgsval4a  15701  lgsneg  15703  lgsneg1  15704  lgsmod  15705  lgsdirprm  15713  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsabs1  15718  lgssq  15719  lgssq2  15720  lgsmulsqcoprm  15725  lgsdirnn0  15726  lgsdinn0  15727  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem1  15740  gausslemma2dlem4  15743  gausslemma2dlem5a  15744  gausslemma2dlem5  15745  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquad2lem1  15760  lgsquad3  15763  2lgslem1b  15768  2lgsoddprmlem2  15785  2sqlem3  15796  2sqlem4  15797  2sqlem8a  15801  2sqlem8  15802  iswomni0  16419