Theorem zcnd 9305

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

Syntax hints:   -> wi 4   e. wcel 2135   CCcc 7742   ZZcz 9182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-resscn 7836

This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-rab 2451  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190  df-ov 5839  df-neg 8063  df-z 9183

This theorem is referenced by:  qapne  9568  fzm1  10025  fzrevral  10030  fzshftral  10033  nn0disj  10063  fzoss2  10097  fzosubel  10119  fzosubel3  10121  fzocatel  10124  fzosplitsnm1  10134  qtri3or  10168  exbtwnzlemstep  10173  exbtwnzlemex  10175  rebtwn2zlemstep  10178  rebtwn2z  10180  flqaddz  10222  flqzadd  10223  2tnp1ge0ge0  10226  ceiqm1l  10236  intqfrac2  10244  intfracq  10245  flqdiv  10246  modqvalr  10250  flqpmodeq  10252  modq0  10254  mulqmod0  10255  modqlt  10258  modqdiffl  10260  modqfrac  10262  flqmod  10263  intqfrac  10264  modqmulnn  10267  modqvalp1  10268  modqcyc  10284  modqcyc2  10285  modqadd1  10286  mulqaddmodid  10289  mulp1mod1  10290  modqmul1  10302  modqmul12d  10303  modqnegd  10304  modqmulmodr  10315  modqdi  10317  modqsubdir  10318  modfzo0difsn  10320  modsumfzodifsn  10321  addmodlteq  10323  frecfzen2  10352  uzennn  10361  uzsinds  10367  seq3shft2  10398  monoord2  10402  iseqf1olemab  10414  seq3f1olemqsumkj  10423  seq3f1olemqsum  10425  expaddzaplem  10488  modqexp  10570  sqoddm1div8  10597  bcm1k  10662  bcp1nk  10664  bcpasc  10668  hashfz  10723  hashfzo  10724  hashfzp1  10726  seq3coll  10741  seq3shft  10766  fzomaxdif  11041  climshft2  11233  iserex  11266  iser3shft  11273  serf0  11279  fsumm1  11343  fsumsplitsnun  11346  fsump1  11347  fsumshftm  11372  fisumrev2  11373  telfsumo  11393  fsumparts  11397  binomlem  11410  isumshft  11417  isumsplit  11418  isum1p  11419  divcnv  11424  arisum  11425  trireciplem  11427  cvgratnnlemmn  11452  cvgratnnlemsumlt  11455  mertenslemi1  11462  ntrivcvgap  11475  fprodm1  11525  fprodp1  11527  fprodfac  11542  fprodrev  11546  fprodmodd  11568  eirraplem  11703  moddvds  11725  dvdscmulr  11746  dvdsmulcr  11747  dvds2ln  11750  dvdsadd2b  11765  fzocongeq  11781  addmodlteqALT  11782  dvdsexp  11784  dvdsmod  11785  mulmoddvds  11786  odd2np1  11795  oddm1even  11797  oexpneg  11799  mulsucdiv2z  11807  zob  11813  ltoddhalfle  11815  divalglemnn  11840  divalglemqt  11841  divalglemex  11844  divalglemeuneg  11845  divalgb  11847  divalgmod  11849  modremain  11851  flodddiv4  11856  infssuzex  11867  zsupssdc  11872  dvdsbnd  11874  gcdaddm  11902  modgcd  11909  gcdmultipled  11911  dvdsgcdidd  11912  bezoutlemnewy  11914  bezoutlemaz  11921  bezoutlembz  11922  dvdsmulgcd  11943  rplpwr  11945  lcmval  11974  lcmcllem  11978  lcmid  11991  mulgcddvds  12005  divgcdcoprm0  12012  cncongr1  12014  cncongr2  12015  rpexp  12062  sqrt2irrlem  12070  sqrt2irrap  12089  qmuldeneqnum  12104  numdensq  12111  qden1elz  12114  hashdvds  12130  phiprm  12132  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  fermltl  12143  prmdiv  12144  prmdiveq  12145  hashgcdlem  12147  odzdvds  12154  modprm0  12163  modprmn0modprm0  12165  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem15  12187  pcpremul  12202  pceulem  12203  pceu  12204  pczpre  12206  pcdiv  12211  pcqmul  12212  pcqdiv  12216  pcexp  12218  pcaddlem  12247  pcadd  12248  fldivp1  12255  pcfac  12257  pcbc  12258  znnen  12268  relogbexpap  13417  logbgcd1irraplemap  13428  iswomni0  13764