Theorem zcnd 9603

Description: An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zcnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem zcnd

Step	Hyp	Ref	Expression
1		zred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2	1	zred 9602	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8208	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  qapne  9873  fzm1  10335  fzrevral  10340  fzshftral  10343  nn0disj  10373  fzoss2  10409  fzo0addelr  10435  elfzoext  10438  fzosubel  10440  fzosubel3  10442  fzocatel  10445  fzosplitsnm1  10455  infssuzex  10494  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  flqaddz  10558  flqzadd  10559  2tnp1ge0ge0  10562  ceiqm1l  10574  intqfrac2  10582  intfracq  10583  flqdiv  10584  modqvalr  10588  flqpmodeq  10590  modq0  10592  mulqmod0  10593  modqlt  10596  modqdiffl  10598  modqfrac  10600  flqmod  10601  intqfrac  10602  modqmulnn  10605  modqvalp1  10606  modqcyc  10622  modqcyc2  10623  modqadd1  10624  mulqaddmodid  10627  mulp1mod1  10628  modqmul1  10640  modqmul12d  10641  modqnegd  10642  modqmulmodr  10653  modqdi  10655  modqsubdir  10656  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecfzen2  10690  uzennn  10699  uzsinds  10707  seq3shft2  10744  monoord2  10749  iseqf1olemab  10765  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  expaddzaplem  10845  modqexp  10929  sqoddm1div8  10956  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashfz  11086  hashfzo  11087  hashfzp1  11089  seq3coll  11107  ccatval3  11180  ccatlid  11187  ccatass  11189  ccatalpha  11194  swrdfv0  11239  swrdfv2  11248  swrds1  11253  ccatswrd  11255  pfxfv  11269  ccatpfx  11286  swrdpfx  11292  pfxccatin12lem2  11316  seq3shft  11416  fzomaxdif  11691  climshft2  11884  iserex  11917  iser3shft  11924  serf0  11930  fsumm1  11995  fsumsplitsnun  11998  fsump1  11999  fsumshftm  12024  fisumrev2  12025  telfsumo  12045  fsumparts  12049  binomlem  12062  isumshft  12069  isumsplit  12070  isum1p  12071  divcnv  12076  arisum  12077  trireciplem  12079  cvgratnnlemmn  12104  cvgratnnlemsumlt  12107  mertenslemi1  12114  ntrivcvgap  12127  fprodm1  12177  fprodp1  12179  fprodfac  12194  fprodrev  12198  fprodmodd  12220  eirraplem  12356  moddvds  12378  dvdscmulr  12399  dvdsmulcr  12400  dvds2ln  12403  dvdsadd2b  12419  dvdsaddre2b  12420  fsumdvds  12421  fzocongeq  12437  addmodlteqALT  12438  dvdsexp  12440  dvdsmod  12441  mulmoddvds  12442  3dvds  12443  odd2np1  12452  oddm1even  12454  oexpneg  12456  mulsucdiv2z  12464  zob  12470  ltoddhalfle  12472  divalglemnn  12497  divalglemqt  12498  divalglemex  12501  divalglemeuneg  12502  divalgb  12504  divalgmod  12506  modremain  12508  flodddiv4  12515  bitsp1  12530  bitsfzo  12534  bitsmod  12535  bitsinv1lem  12540  dvdsbnd  12545  gcdaddm  12573  modgcd  12580  gcdmultipled  12582  dvdsgcdidd  12583  bezoutlemnewy  12585  bezoutlemaz  12592  bezoutlembz  12593  dvdsmulgcd  12614  rplpwr  12616  uzwodc  12626  lcmval  12653  lcmcllem  12657  lcmid  12670  mulgcddvds  12684  divgcdcoprm0  12691  cncongr1  12693  cncongr2  12694  rpexp  12743  sqrt2irrlem  12751  sqrt2irrap  12770  qmuldeneqnum  12785  numdensq  12792  qden1elz  12795  hashdvds  12811  phiprm  12813  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  fermltl  12824  prmdiv  12825  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  modprm0  12845  modprmn0modprm0  12847  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem15  12869  pcpremul  12884  pceulem  12885  pceu  12886  pczpre  12888  pcdiv  12893  pcqmul  12894  pcqdiv  12898  pcexp  12900  pcaddlem  12930  pcadd  12931  fldivp1  12939  pcfac  12941  pcbc  12942  prmpwdvds  12946  4sqlem5  12973  4sqlem8  12976  4sqlem9  12977  4sqlem10  12978  4sqlemffi  12987  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem14  12995  4sqlem16  12997  4sqlem17  12998  znnen  13037  mulgsubcl  13741  mulgdirlem  13758  mulgdir  13759  mulgass  13764  mulgmodid  13766  mulgsubdir  13767  gsumfzconst  13946  gsumfzsnfd  13950  gsumsplit0  13951  zringmulg  14631  zndvds0  14683  znf1o  14684  znunit  14692  relogbexpap  15701  logbgcd1irraplemap  15712  wilthlem1  15723  lgslem1  15748  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsneg1  15773  lgsmod  15774  lgsdirprm  15782  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsabs1  15787  lgssq  15788  lgssq2  15789  lgsmulsqcoprm  15794  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem1  15809  gausslemma2dlem4  15812  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquad2lem1  15829  lgsquad3  15832  2lgslem1b  15837  2lgsoddprmlem2  15854  2sqlem3  15865  2sqlem4  15866  2sqlem8a  15870  2sqlem8  15871  clwwlkccatlem  16270  iswomni0  16707  gsumgfsumlem  16735  gsumgfsum  16736