Theorem zcnd 9593

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8020   ZZcz 9469

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 8114

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470

This theorem is referenced by:  qapne  9863  fzm1  10325  fzrevral  10330  fzshftral  10333  nn0disj  10363  fzoss2  10399  fzo0addelr  10424  elfzoext  10427  fzosubel  10429  fzosubel3  10431  fzocatel  10434  fzosplitsnm1  10444  infssuzex  10483  zsupssdc  10488  qtri3or  10490  exbtwnzlemstep  10497  exbtwnzlemex  10499  rebtwn2zlemstep  10502  rebtwn2z  10504  flqaddz  10547  flqzadd  10548  2tnp1ge0ge0  10551  ceiqm1l  10563  intqfrac2  10571  intfracq  10572  flqdiv  10573  modqvalr  10577  flqpmodeq  10579  modq0  10581  mulqmod0  10582  modqlt  10585  modqdiffl  10587  modqfrac  10589  flqmod  10590  intqfrac  10591  modqmulnn  10594  modqvalp1  10595  modqcyc  10611  modqcyc2  10612  modqadd1  10613  mulqaddmodid  10616  mulp1mod1  10617  modqmul1  10629  modqmul12d  10630  modqnegd  10631  modqmulmodr  10642  modqdi  10644  modqsubdir  10645  modfzo0difsn  10647  modsumfzodifsn  10648  addmodlteq  10650  frecfzen2  10679  uzennn  10688  uzsinds  10696  seq3shft2  10733  monoord2  10738  iseqf1olemab  10754  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seqf1oglem1  10771  seqf1oglem2  10772  expaddzaplem  10834  modqexp  10918  sqoddm1div8  10945  bcm1k  11012  bcp1nk  11014  bcpasc  11018  hashfz  11075  hashfzo  11076  hashfzp1  11078  seq3coll  11096  ccatval3  11166  ccatlid  11173  ccatass  11175  ccatalpha  11180  swrdfv0  11225  swrdfv2  11234  swrds1  11239  ccatswrd  11241  pfxfv  11255  ccatpfx  11272  swrdpfx  11278  pfxccatin12lem2  11302  seq3shft  11389  fzomaxdif  11664  climshft2  11857  iserex  11890  iser3shft  11897  serf0  11903  fsumm1  11967  fsumsplitsnun  11970  fsump1  11971  fsumshftm  11996  fisumrev2  11997  telfsumo  12017  fsumparts  12021  binomlem  12034  isumshft  12041  isumsplit  12042  isum1p  12043  divcnv  12048  arisum  12049  trireciplem  12051  cvgratnnlemmn  12076  cvgratnnlemsumlt  12079  mertenslemi1  12086  ntrivcvgap  12099  fprodm1  12149  fprodp1  12151  fprodfac  12166  fprodrev  12170  fprodmodd  12192  eirraplem  12328  moddvds  12350  dvdscmulr  12371  dvdsmulcr  12372  dvds2ln  12375  dvdsadd2b  12391  dvdsaddre2b  12392  fsumdvds  12393  fzocongeq  12409  addmodlteqALT  12410  dvdsexp  12412  dvdsmod  12413  mulmoddvds  12414  3dvds  12415  odd2np1  12424  oddm1even  12426  oexpneg  12428  mulsucdiv2z  12436  zob  12442  ltoddhalfle  12444  divalglemnn  12469  divalglemqt  12470  divalglemex  12473  divalglemeuneg  12474  divalgb  12476  divalgmod  12478  modremain  12480  flodddiv4  12487  bitsp1  12502  bitsfzo  12506  bitsmod  12507  bitsinv1lem  12512  dvdsbnd  12517  gcdaddm  12545  modgcd  12552  gcdmultipled  12554  dvdsgcdidd  12555  bezoutlemnewy  12557  bezoutlemaz  12564  bezoutlembz  12565  dvdsmulgcd  12586  rplpwr  12588  uzwodc  12598  lcmval  12625  lcmcllem  12629  lcmid  12642  mulgcddvds  12656  divgcdcoprm0  12663  cncongr1  12665  cncongr2  12666  rpexp  12715  sqrt2irrlem  12723  sqrt2irrap  12742  qmuldeneqnum  12757  numdensq  12764  qden1elz  12767  hashdvds  12783  phiprm  12785  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  fermltl  12796  prmdiv  12797  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  modprm0  12817  modprmn0modprm0  12819  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem15  12841  pcpremul  12856  pceulem  12857  pceu  12858  pczpre  12860  pcdiv  12865  pcqmul  12866  pcqdiv  12870  pcexp  12872  pcaddlem  12902  pcadd  12903  fldivp1  12911  pcfac  12913  pcbc  12914  prmpwdvds  12918  4sqlem5  12945  4sqlem8  12948  4sqlem9  12949  4sqlem10  12950  4sqlemffi  12959  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem14  12967  4sqlem16  12969  4sqlem17  12970  znnen  13009  mulgsubcl  13713  mulgdirlem  13730  mulgdir  13731  mulgass  13736  mulgmodid  13738  mulgsubdir  13739  gsumfzconst  13918  gsumfzsnfd  13922  zringmulg  14602  zndvds0  14654  znf1o  14655  znunit  14663  relogbexpap  15672  logbgcd1irraplemap  15683  wilthlem1  15694  lgslem1  15719  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsneg1  15744  lgsmod  15745  lgsdirprm  15753  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsabs1  15758  lgssq  15759  lgssq2  15760  lgsmulsqcoprm  15765  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem1  15780  gausslemma2dlem4  15783  gausslemma2dlem5a  15784  gausslemma2dlem5  15785  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquad2lem1  15800  lgsquad3  15803  2lgslem1b  15808  2lgsoddprmlem2  15825  2sqlem3  15836  2sqlem4  15837  2sqlem8a  15841  2sqlem8  15842  clwwlkccatlem  16195  iswomni0  16591