Theorem zcnd 9531

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

Syntax hints:   -> wi 4   e. wcel 2178   CCcc 7958   ZZcz 9407

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  qapne  9795  fzm1  10257  fzrevral  10262  fzshftral  10265  nn0disj  10295  fzoss2  10331  fzo0addelr  10355  elfzoext  10358  fzosubel  10360  fzosubel3  10362  fzocatel  10365  fzosplitsnm1  10375  infssuzex  10413  zsupssdc  10418  qtri3or  10420  exbtwnzlemstep  10427  exbtwnzlemex  10429  rebtwn2zlemstep  10432  rebtwn2z  10434  flqaddz  10477  flqzadd  10478  2tnp1ge0ge0  10481  ceiqm1l  10493  intqfrac2  10501  intfracq  10502  flqdiv  10503  modqvalr  10507  flqpmodeq  10509  modq0  10511  mulqmod0  10512  modqlt  10515  modqdiffl  10517  modqfrac  10519  flqmod  10520  intqfrac  10521  modqmulnn  10524  modqvalp1  10525  modqcyc  10541  modqcyc2  10542  modqadd1  10543  mulqaddmodid  10546  mulp1mod1  10547  modqmul1  10559  modqmul12d  10560  modqnegd  10561  modqmulmodr  10572  modqdi  10574  modqsubdir  10575  modfzo0difsn  10577  modsumfzodifsn  10578  addmodlteq  10580  frecfzen2  10609  uzennn  10618  uzsinds  10626  seq3shft2  10663  monoord2  10668  iseqf1olemab  10684  seq3f1olemqsumkj  10693  seq3f1olemqsum  10695  seqf1oglem1  10701  seqf1oglem2  10702  expaddzaplem  10764  modqexp  10848  sqoddm1div8  10875  bcm1k  10942  bcp1nk  10944  bcpasc  10948  hashfz  11003  hashfzo  11004  hashfzp1  11006  seq3coll  11024  ccatval3  11093  ccatlid  11100  ccatass  11102  swrdfv0  11145  swrdfv2  11154  swrds1  11159  ccatswrd  11161  pfxfv  11175  ccatpfx  11192  swrdpfx  11198  pfxccatin12lem2  11222  seq3shft  11264  fzomaxdif  11539  climshft2  11732  iserex  11765  iser3shft  11772  serf0  11778  fsumm1  11842  fsumsplitsnun  11845  fsump1  11846  fsumshftm  11871  fisumrev2  11872  telfsumo  11892  fsumparts  11896  binomlem  11909  isumshft  11916  isumsplit  11917  isum1p  11918  divcnv  11923  arisum  11924  trireciplem  11926  cvgratnnlemmn  11951  cvgratnnlemsumlt  11954  mertenslemi1  11961  ntrivcvgap  11974  fprodm1  12024  fprodp1  12026  fprodfac  12041  fprodrev  12045  fprodmodd  12067  eirraplem  12203  moddvds  12225  dvdscmulr  12246  dvdsmulcr  12247  dvds2ln  12250  dvdsadd2b  12266  dvdsaddre2b  12267  fsumdvds  12268  fzocongeq  12284  addmodlteqALT  12285  dvdsexp  12287  dvdsmod  12288  mulmoddvds  12289  3dvds  12290  odd2np1  12299  oddm1even  12301  oexpneg  12303  mulsucdiv2z  12311  zob  12317  ltoddhalfle  12319  divalglemnn  12344  divalglemqt  12345  divalglemex  12348  divalglemeuneg  12349  divalgb  12351  divalgmod  12353  modremain  12355  flodddiv4  12362  bitsp1  12377  bitsfzo  12381  bitsmod  12382  bitsinv1lem  12387  dvdsbnd  12392  gcdaddm  12420  modgcd  12427  gcdmultipled  12429  dvdsgcdidd  12430  bezoutlemnewy  12432  bezoutlemaz  12439  bezoutlembz  12440  dvdsmulgcd  12461  rplpwr  12463  uzwodc  12473  lcmval  12500  lcmcllem  12504  lcmid  12517  mulgcddvds  12531  divgcdcoprm0  12538  cncongr1  12540  cncongr2  12541  rpexp  12590  sqrt2irrlem  12598  sqrt2irrap  12617  qmuldeneqnum  12632  numdensq  12639  qden1elz  12642  hashdvds  12658  phiprm  12660  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  fermltl  12671  prmdiv  12672  prmdiveq  12673  hashgcdlem  12675  odzdvds  12683  modprm0  12692  modprmn0modprm0  12694  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem15  12716  pcpremul  12731  pceulem  12732  pceu  12733  pczpre  12735  pcdiv  12740  pcqmul  12741  pcqdiv  12745  pcexp  12747  pcaddlem  12777  pcadd  12778  fldivp1  12786  pcfac  12788  pcbc  12789  prmpwdvds  12793  4sqlem5  12820  4sqlem8  12823  4sqlem9  12824  4sqlem10  12825  4sqlemffi  12834  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem14  12842  4sqlem16  12844  4sqlem17  12845  znnen  12884  mulgsubcl  13587  mulgdirlem  13604  mulgdir  13605  mulgass  13610  mulgmodid  13612  mulgsubdir  13613  gsumfzconst  13792  gsumfzsnfd  13796  zringmulg  14475  zndvds0  14527  znf1o  14528  znunit  14536  relogbexpap  15545  logbgcd1irraplemap  15556  wilthlem1  15567  lgslem1  15592  lgsval2lem  15602  lgsval4a  15614  lgsneg  15616  lgsneg1  15617  lgsmod  15618  lgsdirprm  15626  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsabs1  15631  lgssq  15632  lgssq2  15633  lgsmulsqcoprm  15638  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  gausslemma2dlem1  15653  gausslemma2dlem4  15656  gausslemma2dlem5a  15657  gausslemma2dlem5  15658  gausslemma2dlem6  15659  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgsquadlem1  15669  lgsquad2lem1  15673  lgsquad3  15676  2lgslem1b  15681  2lgsoddprmlem2  15698  2sqlem3  15709  2sqlem4  15710  2sqlem8a  15714  2sqlem8  15715  iswomni0  16192