Theorem zcnd 8930

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

Syntax hints:   → wi 4   ∈ wcel 1439  ℂcc 7409  ℤcz 8811

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-resscn 7498

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-rex 2366  df-rab 2369  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669  df-neg 7717  df-z 8812

This theorem is referenced by:  qapne  9185  fzm1  9575  fzrevral  9580  fzshftral  9583  nn0disj  9610  fzoss2  9644  fzosubel  9666  fzosubel3  9668  fzocatel  9671  fzosplitsnm1  9681  qtri3or  9715  exbtwnzlemstep  9720  exbtwnzlemex  9722  rebtwn2zlemstep  9725  rebtwn2z  9727  flqaddz  9765  flqzadd  9766  2tnp1ge0ge0  9769  ceiqm1l  9779  intqfrac2  9787  intfracq  9788  flqdiv  9789  modqvalr  9793  flqpmodeq  9795  modq0  9797  mulqmod0  9798  modqlt  9801  modqdiffl  9803  modqfrac  9805  flqmod  9806  intqfrac  9807  modqmulnn  9810  modqvalp1  9811  modqcyc  9827  modqcyc2  9828  modqadd1  9829  mulqaddmodid  9832  mulp1mod1  9833  modqmul1  9845  modqmul12d  9846  modqnegd  9847  modqmulmodr  9858  modqdi  9860  modqsubdir  9861  modfzo0difsn  9863  modsumfzodifsn  9864  addmodlteq  9866  frecfzen2  9895  uzsinds  9909  monoord2  9966  iseqf1olemab  9979  seq3f1olemqsumkj  9988  seq3f1olemqsum  9990  expaddzaplem  10059  sqoddm1div8  10167  bcm1k  10229  bcp1nk  10231  bcpasc  10235  hashfz  10290  hashfzo  10291  hashfzp1  10293  iseqcoll  10308  seq3shft  10333  fzomaxdif  10607  climshft2  10756  iserex  10788  iser3shft  10796  serf0  10802  fsumm1  10871  fsumsplitsnun  10874  fsump1  10875  fsumshftm  10900  fisumrev2  10901  telfsumo  10921  fsumparts  10925  binomlem  10938  isumshft  10945  isumsplit  10946  isum1p  10947  divcnv  10952  arisum  10953  trireciplem  10955  cvgratnnlemmn  10980  cvgratnnlemsumlt  10983  mertenslemi1  10990  eirraplem  11125  moddvds  11144  dvdscmulr  11164  dvdsmulcr  11165  dvds2ln  11168  dvdsadd2b  11182  fzocongeq  11198  addmodlteqALT  11199  dvdsexp  11201  dvdsmod  11202  mulmoddvds  11203  odd2np1  11212  oddm1even  11214  oexpneg  11216  mulsucdiv2z  11224  zob  11230  ltoddhalfle  11232  divalglemnn  11257  divalglemqt  11258  divalglemex  11261  divalglemeuneg  11262  divalgb  11264  divalgmod  11266  modremain  11268  flodddiv4  11273  infssuzex  11284  dvdsbnd  11287  gcdaddm  11314  modgcd  11321  bezoutlemnewy  11324  bezoutlemaz  11331  bezoutlembz  11332  dvdsmulgcd  11353  rplpwr  11355  lcmval  11384  lcmcllem  11388  lcmid  11401  mulgcddvds  11415  divgcdcoprm0  11422  cncongr1  11424  cncongr2  11425  rpexp  11471  sqrt2irrlem  11479  sqrt2irrap  11497  qmuldeneqnum  11512  numdensq  11519  qden1elz  11522  hashdvds  11536  phiprm  11538  hashgcdlem  11542  znnen  11550