Theorem zcnd 9646

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8073   ZZcz 9522

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 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8396  df-z 9523

This theorem is referenced by:  qapne  9916  fzm1  10378  fzrevral  10383  fzshftral  10386  nn0disj  10416  fzoss2  10452  fzo0addelr  10478  elfzoext  10481  fzosubel  10483  fzosubel3  10485  fzocatel  10488  fzosplitsnm1  10498  infssuzex  10537  zsupssdc  10542  qtri3or  10544  exbtwnzlemstep  10551  exbtwnzlemex  10553  rebtwn2zlemstep  10556  rebtwn2z  10558  flqaddz  10601  flqzadd  10602  2tnp1ge0ge0  10605  ceiqm1l  10617  intqfrac2  10625  intfracq  10626  flqdiv  10627  modqvalr  10631  flqpmodeq  10633  modq0  10635  mulqmod0  10636  modqlt  10639  modqdiffl  10641  modqfrac  10643  flqmod  10644  intqfrac  10645  modqmulnn  10648  modqvalp1  10649  modqcyc  10665  modqcyc2  10666  modqadd1  10667  mulqaddmodid  10670  mulp1mod1  10671  modqmul1  10683  modqmul12d  10684  modqnegd  10685  modqmulmodr  10696  modqdi  10698  modqsubdir  10699  modfzo0difsn  10701  modsumfzodifsn  10702  addmodlteq  10704  frecfzen2  10733  uzennn  10742  uzsinds  10750  seq3shft2  10787  monoord2  10792  iseqf1olemab  10808  seq3f1olemqsumkj  10817  seq3f1olemqsum  10819  seqf1oglem1  10825  seqf1oglem2  10826  expaddzaplem  10888  modqexp  10972  sqoddm1div8  10999  bcm1k  11066  bcp1nk  11068  bcpasc  11072  hashfz  11129  hashfzo  11130  hashfzp1  11132  seq3coll  11150  ccatval3  11223  ccatlid  11230  ccatass  11232  ccatalpha  11237  swrdfv0  11282  swrdfv2  11291  swrds1  11296  ccatswrd  11298  pfxfv  11312  ccatpfx  11329  swrdpfx  11335  pfxccatin12lem2  11359  seq3shft  11459  fzomaxdif  11734  climshft2  11927  iserex  11960  iser3shft  11967  serf0  11973  fsumm1  12038  fsumsplitsnun  12041  fsump1  12042  fsumshftm  12067  fisumrev2  12068  telfsumo  12088  fsumparts  12092  binomlem  12105  isumshft  12112  isumsplit  12113  isum1p  12114  divcnv  12119  arisum  12120  trireciplem  12122  cvgratnnlemmn  12147  cvgratnnlemsumlt  12150  mertenslemi1  12157  ntrivcvgap  12170  fprodm1  12220  fprodp1  12222  fprodfac  12237  fprodrev  12241  fprodmodd  12263  eirraplem  12399  moddvds  12421  dvdscmulr  12442  dvdsmulcr  12443  dvds2ln  12446  dvdsadd2b  12462  dvdsaddre2b  12463  fsumdvds  12464  fzocongeq  12480  addmodlteqALT  12481  dvdsexp  12483  dvdsmod  12484  mulmoddvds  12485  3dvds  12486  odd2np1  12495  oddm1even  12497  oexpneg  12499  mulsucdiv2z  12507  zob  12513  ltoddhalfle  12515  divalglemnn  12540  divalglemqt  12541  divalglemex  12544  divalglemeuneg  12545  divalgb  12547  divalgmod  12549  modremain  12551  flodddiv4  12558  bitsp1  12573  bitsfzo  12577  bitsmod  12578  bitsinv1lem  12583  dvdsbnd  12588  gcdaddm  12616  modgcd  12623  gcdmultipled  12625  dvdsgcdidd  12626  bezoutlemnewy  12628  bezoutlemaz  12635  bezoutlembz  12636  dvdsmulgcd  12657  rplpwr  12659  uzwodc  12669  lcmval  12696  lcmcllem  12700  lcmid  12713  mulgcddvds  12727  divgcdcoprm0  12734  cncongr1  12736  cncongr2  12737  rpexp  12786  sqrt2irrlem  12794  sqrt2irrap  12813  qmuldeneqnum  12828  numdensq  12835  qden1elz  12838  hashdvds  12854  phiprm  12856  eulerthlema  12863  eulerthlemh  12864  eulerthlemth  12865  fermltl  12867  prmdiv  12868  prmdiveq  12869  hashgcdlem  12871  odzdvds  12879  modprm0  12888  modprmn0modprm0  12890  pythagtriplem6  12904  pythagtriplem7  12905  pythagtriplem15  12912  pcpremul  12927  pceulem  12928  pceu  12929  pczpre  12931  pcdiv  12936  pcqmul  12937  pcqdiv  12941  pcexp  12943  pcaddlem  12973  pcadd  12974  fldivp1  12982  pcfac  12984  pcbc  12985  prmpwdvds  12989  4sqlem5  13016  4sqlem8  13019  4sqlem9  13020  4sqlem10  13021  4sqlemffi  13030  4sqexercise2  13033  4sqlemsdc  13034  4sqlem11  13035  4sqlem14  13038  4sqlem16  13040  4sqlem17  13041  znnen  13080  mulgsubcl  13784  mulgdirlem  13801  mulgdir  13802  mulgass  13807  mulgmodid  13809  mulgsubdir  13810  gsumfzconst  13989  gsumfzsnfd  13993  gsumsplit0  13994  zringmulg  14674  zndvds0  14726  znf1o  14727  znunit  14735  relogbexpap  15749  logbgcd1irraplemap  15760  wilthlem1  15774  lgslem1  15799  lgsval2lem  15809  lgsval4a  15821  lgsneg  15823  lgsneg1  15824  lgsmod  15825  lgsdirprm  15833  lgsdir  15834  lgsdilem2  15835  lgsdi  15836  lgsne0  15837  lgsabs1  15838  lgssq  15839  lgssq2  15840  lgsmulsqcoprm  15845  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem1  15860  gausslemma2dlem4  15863  gausslemma2dlem5a  15864  gausslemma2dlem5  15865  gausslemma2dlem6  15866  gausslemma2d  15868  lgseisenlem1  15869  lgseisenlem2  15870  lgseisenlem3  15871  lgseisenlem4  15872  lgsquadlem1  15876  lgsquad2lem1  15880  lgsquad3  15883  2lgslem1b  15888  2lgsoddprmlem2  15905  2sqlem3  15916  2sqlem4  15917  2sqlem8a  15921  2sqlem8  15922  clwwlkccatlem  16321  iswomni0  16764  gsumgfsumlem  16792  gsumgfsum  16793