Theorem zcnd 9314

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

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7751   ZZcz 9191

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7845

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-rab 2453  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845  df-neg 8072  df-z 9192

This theorem is referenced by:  qapne  9577  fzm1  10035  fzrevral  10040  fzshftral  10043  nn0disj  10073  fzoss2  10107  fzosubel  10129  fzosubel3  10131  fzocatel  10134  fzosplitsnm1  10144  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemex  10185  rebtwn2zlemstep  10188  rebtwn2z  10190  flqaddz  10232  flqzadd  10233  2tnp1ge0ge0  10236  ceiqm1l  10246  intqfrac2  10254  intfracq  10255  flqdiv  10256  modqvalr  10260  flqpmodeq  10262  modq0  10264  mulqmod0  10265  modqlt  10268  modqdiffl  10270  modqfrac  10272  flqmod  10273  intqfrac  10274  modqmulnn  10277  modqvalp1  10278  modqcyc  10294  modqcyc2  10295  modqadd1  10296  mulqaddmodid  10299  mulp1mod1  10300  modqmul1  10312  modqmul12d  10313  modqnegd  10314  modqmulmodr  10325  modqdi  10327  modqsubdir  10328  modfzo0difsn  10330  modsumfzodifsn  10331  addmodlteq  10333  frecfzen2  10362  uzennn  10371  uzsinds  10377  seq3shft2  10408  monoord2  10412  iseqf1olemab  10424  seq3f1olemqsumkj  10433  seq3f1olemqsum  10435  expaddzaplem  10498  modqexp  10581  sqoddm1div8  10608  bcm1k  10673  bcp1nk  10675  bcpasc  10679  hashfz  10734  hashfzo  10735  hashfzp1  10737  seq3coll  10755  seq3shft  10780  fzomaxdif  11055  climshft2  11247  iserex  11280  iser3shft  11287  serf0  11293  fsumm1  11357  fsumsplitsnun  11360  fsump1  11361  fsumshftm  11386  fisumrev2  11387  telfsumo  11407  fsumparts  11411  binomlem  11424  isumshft  11431  isumsplit  11432  isum1p  11433  divcnv  11438  arisum  11439  trireciplem  11441  cvgratnnlemmn  11466  cvgratnnlemsumlt  11469  mertenslemi1  11476  ntrivcvgap  11489  fprodm1  11539  fprodp1  11541  fprodfac  11556  fprodrev  11560  fprodmodd  11582  eirraplem  11717  moddvds  11739  dvdscmulr  11760  dvdsmulcr  11761  dvds2ln  11764  dvdsadd2b  11780  fzocongeq  11796  addmodlteqALT  11797  dvdsexp  11799  dvdsmod  11800  mulmoddvds  11801  odd2np1  11810  oddm1even  11812  oexpneg  11814  mulsucdiv2z  11822  zob  11828  ltoddhalfle  11830  divalglemnn  11855  divalglemqt  11856  divalglemex  11859  divalglemeuneg  11860  divalgb  11862  divalgmod  11864  modremain  11866  flodddiv4  11871  infssuzex  11882  zsupssdc  11887  dvdsbnd  11889  gcdaddm  11917  modgcd  11924  gcdmultipled  11926  dvdsgcdidd  11927  bezoutlemnewy  11929  bezoutlemaz  11936  bezoutlembz  11937  dvdsmulgcd  11958  rplpwr  11960  uzwodc  11970  lcmval  11995  lcmcllem  11999  lcmid  12012  mulgcddvds  12026  divgcdcoprm0  12033  cncongr1  12035  cncongr2  12036  rpexp  12085  sqrt2irrlem  12093  sqrt2irrap  12112  qmuldeneqnum  12127  numdensq  12134  qden1elz  12137  hashdvds  12153  phiprm  12155  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  fermltl  12166  prmdiv  12167  prmdiveq  12168  hashgcdlem  12170  odzdvds  12177  modprm0  12186  modprmn0modprm0  12188  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem15  12210  pcpremul  12225  pceulem  12226  pceu  12227  pczpre  12229  pcdiv  12234  pcqmul  12235  pcqdiv  12239  pcexp  12241  pcaddlem  12270  pcadd  12271  fldivp1  12278  pcfac  12280  pcbc  12281  prmpwdvds  12285  4sqlem5  12312  4sqlem8  12315  4sqlem9  12316  4sqlem10  12317  znnen  12331  relogbexpap  13516  logbgcd1irraplemap  13527  lgslem1  13541  lgsval2lem  13551  lgsval4a  13563  lgsneg  13565  lgsneg1  13566  lgsmod  13567  lgsdirprm  13575  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgsabs1  13580  lgssq  13581  lgssq2  13582  lgsmulsqcoprm  13587  lgsdirnn0  13588  lgsdinn0  13589  2sqlem3  13593  2sqlem4  13594  2sqlem8a  13598  2sqlem8  13599  iswomni0  13930