Theorem zcnd 9167

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

Syntax hints:   → wi 4   ∈ wcel 1480  ℂcc 7611  ℤcz 9047

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-resscn 7705

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-rab 2423  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770  df-neg 7929  df-z 9048

This theorem is referenced by:  qapne  9424  fzm1  9873  fzrevral  9878  fzshftral  9881  nn0disj  9908  fzoss2  9942  fzosubel  9964  fzosubel3  9966  fzocatel  9969  fzosplitsnm1  9979  qtri3or  10013  exbtwnzlemstep  10018  exbtwnzlemex  10020  rebtwn2zlemstep  10023  rebtwn2z  10025  flqaddz  10063  flqzadd  10064  2tnp1ge0ge0  10067  ceiqm1l  10077  intqfrac2  10085  intfracq  10086  flqdiv  10087  modqvalr  10091  flqpmodeq  10093  modq0  10095  mulqmod0  10096  modqlt  10099  modqdiffl  10101  modqfrac  10103  flqmod  10104  intqfrac  10105  modqmulnn  10108  modqvalp1  10109  modqcyc  10125  modqcyc2  10126  modqadd1  10127  mulqaddmodid  10130  mulp1mod1  10131  modqmul1  10143  modqmul12d  10144  modqnegd  10145  modqmulmodr  10156  modqdi  10158  modqsubdir  10159  modfzo0difsn  10161  modsumfzodifsn  10162  addmodlteq  10164  frecfzen2  10193  uzennn  10202  uzsinds  10208  seq3shft2  10239  monoord2  10243  iseqf1olemab  10255  seq3f1olemqsumkj  10264  seq3f1olemqsum  10266  expaddzaplem  10329  sqoddm1div8  10437  bcm1k  10499  bcp1nk  10501  bcpasc  10505  hashfz  10560  hashfzo  10561  hashfzp1  10563  seq3coll  10578  seq3shft  10603  fzomaxdif  10878  climshft2  11068  iserex  11101  iser3shft  11108  serf0  11114  fsumm1  11178  fsumsplitsnun  11181  fsump1  11182  fsumshftm  11207  fisumrev2  11208  telfsumo  11228  fsumparts  11232  binomlem  11245  isumshft  11252  isumsplit  11253  isum1p  11254  divcnv  11259  arisum  11260  trireciplem  11262  cvgratnnlemmn  11287  cvgratnnlemsumlt  11290  mertenslemi1  11297  ntrivcvgap  11310  eirraplem  11472  moddvds  11491  dvdscmulr  11511  dvdsmulcr  11512  dvds2ln  11515  dvdsadd2b  11529  fzocongeq  11545  addmodlteqALT  11546  dvdsexp  11548  dvdsmod  11549  mulmoddvds  11550  odd2np1  11559  oddm1even  11561  oexpneg  11563  mulsucdiv2z  11571  zob  11577  ltoddhalfle  11579  divalglemnn  11604  divalglemqt  11605  divalglemex  11608  divalglemeuneg  11609  divalgb  11611  divalgmod  11613  modremain  11615  flodddiv4  11620  infssuzex  11631  dvdsbnd  11634  gcdaddm  11661  modgcd  11668  gcdmultipled  11670  dvdsgcdidd  11671  bezoutlemnewy  11673  bezoutlemaz  11680  bezoutlembz  11681  dvdsmulgcd  11702  rplpwr  11704  lcmval  11733  lcmcllem  11737  lcmid  11750  mulgcddvds  11764  divgcdcoprm0  11771  cncongr1  11773  cncongr2  11774  rpexp  11820  sqrt2irrlem  11828  sqrt2irrap  11847  qmuldeneqnum  11862  numdensq  11869  qden1elz  11872  hashdvds  11886  phiprm  11888  hashgcdlem  11892  znnen  11900