Theorem zcnd 9664

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 9663	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 8267	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8090  ℤcz 9540

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 8184

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 8412  df-z 9541

This theorem is referenced by:  qapne  9934  fzm1  10397  fzrevral  10402  fzshftral  10405  nn0disj  10435  fzoss2  10471  fzo0addelr  10497  elfzoext  10500  fzosubel  10502  fzosubel3  10504  fzocatel  10507  fzosplitsnm1  10517  infssuzex  10556  zsupssdc  10561  qtri3or  10563  exbtwnzlemstep  10570  exbtwnzlemex  10572  rebtwn2zlemstep  10575  rebtwn2z  10577  flqaddz  10620  flqzadd  10621  2tnp1ge0ge0  10624  ceiqm1l  10636  intqfrac2  10644  intfracq  10645  flqdiv  10646  modqvalr  10650  flqpmodeq  10652  modq0  10654  mulqmod0  10655  modqlt  10658  modqdiffl  10660  modqfrac  10662  flqmod  10663  intqfrac  10664  modqmulnn  10667  modqvalp1  10668  modqcyc  10684  modqcyc2  10685  modqadd1  10686  mulqaddmodid  10689  mulp1mod1  10690  modqmul1  10702  modqmul12d  10703  modqnegd  10704  modqmulmodr  10715  modqdi  10717  modqsubdir  10718  modfzo0difsn  10720  modsumfzodifsn  10721  addmodlteq  10723  frecfzen2  10752  uzennn  10761  uzsinds  10769  seq3shft2  10806  monoord2  10811  iseqf1olemab  10827  seq3f1olemqsumkj  10836  seq3f1olemqsum  10838  seqf1oglem1  10844  seqf1oglem2  10845  expaddzaplem  10907  modqexp  10991  sqoddm1div8  11018  bcm1k  11085  bcp1nk  11087  bcpasc  11091  hashfz  11148  hashfzo  11149  hashfzp1  11151  seq3coll  11169  ccatval3  11242  ccatlid  11249  ccatass  11251  ccatalpha  11256  swrdfv0  11301  swrdfv2  11310  swrds1  11315  ccatswrd  11317  pfxfv  11331  ccatpfx  11348  swrdpfx  11354  pfxccatin12lem2  11378  seq3shft  11478  fzomaxdif  11753  climshft2  11946  iserex  11979  iser3shft  11986  serf0  11992  fsumm1  12057  fsumsplitsnun  12060  fsump1  12061  fsumshftm  12086  fisumrev2  12087  telfsumo  12107  fsumparts  12111  binomlem  12124  isumshft  12131  isumsplit  12132  isum1p  12133  divcnv  12138  arisum  12139  trireciplem  12141  cvgratnnlemmn  12166  cvgratnnlemsumlt  12169  mertenslemi1  12176  ntrivcvgap  12189  fprodm1  12239  fprodp1  12241  fprodfac  12256  fprodrev  12260  fprodmodd  12282  eirraplem  12418  moddvds  12440  dvdscmulr  12461  dvdsmulcr  12462  dvds2ln  12465  dvdsadd2b  12481  dvdsaddre2b  12482  fsumdvds  12483  fzocongeq  12499  addmodlteqALT  12500  dvdsexp  12502  dvdsmod  12503  mulmoddvds  12504  3dvds  12505  odd2np1  12514  oddm1even  12516  oexpneg  12518  mulsucdiv2z  12526  zob  12532  ltoddhalfle  12534  divalglemnn  12559  divalglemqt  12560  divalglemex  12563  divalglemeuneg  12564  divalgb  12566  divalgmod  12568  modremain  12570  flodddiv4  12577  bitsp1  12592  bitsfzo  12596  bitsmod  12597  bitsinv1lem  12602  dvdsbnd  12607  gcdaddm  12635  modgcd  12642  gcdmultipled  12644  dvdsgcdidd  12645  bezoutlemnewy  12647  bezoutlemaz  12654  bezoutlembz  12655  dvdsmulgcd  12676  rplpwr  12678  uzwodc  12688  lcmval  12715  lcmcllem  12719  lcmid  12732  mulgcddvds  12746  divgcdcoprm0  12753  cncongr1  12755  cncongr2  12756  rpexp  12805  sqrt2irrlem  12813  sqrt2irrap  12832  qmuldeneqnum  12847  numdensq  12854  qden1elz  12857  hashdvds  12873  phiprm  12875  eulerthlema  12882  eulerthlemh  12883  eulerthlemth  12884  fermltl  12886  prmdiv  12887  prmdiveq  12888  hashgcdlem  12890  odzdvds  12898  modprm0  12907  modprmn0modprm0  12909  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem15  12931  pcpremul  12946  pceulem  12947  pceu  12948  pczpre  12950  pcdiv  12955  pcqmul  12956  pcqdiv  12960  pcexp  12962  pcaddlem  12992  pcadd  12993  fldivp1  13001  pcfac  13003  pcbc  13004  prmpwdvds  13008  4sqlem5  13035  4sqlem8  13038  4sqlem9  13039  4sqlem10  13040  4sqlemffi  13049  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem14  13057  4sqlem16  13059  4sqlem17  13060  znnen  13099  mulgsubcl  13803  mulgdirlem  13820  mulgdir  13821  mulgass  13826  mulgmodid  13828  mulgsubdir  13829  gsumfzconst  14008  gsumfzsnfd  14012  gsumsplit0  14013  zringmulg  14694  zndvds0  14746  znf1o  14747  znunit  14755  relogbexpap  15769  logbgcd1irraplemap  15780  wilthlem1  15794  lgslem1  15819  lgsval2lem  15829  lgsval4a  15841  lgsneg  15843  lgsneg1  15844  lgsmod  15845  lgsdirprm  15853  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsabs1  15858  lgssq  15859  lgssq2  15860  lgsmulsqcoprm  15865  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem1  15880  gausslemma2dlem4  15883  gausslemma2dlem5a  15884  gausslemma2dlem5  15885  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquad2lem1  15900  lgsquad3  15903  2lgslem1b  15908  2lgsoddprmlem2  15925  2sqlem3  15936  2sqlem4  15937  2sqlem8a  15941  2sqlem8  15942  clwwlkccatlem  16341  iswomni0  16784  gsumgfsumlem  16812  gsumgfsum  16813