Theorem zcnd 9198

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℂcc 7642  ℤcz 9078

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-neg 7960  df-z 9079

This theorem is referenced by:  qapne  9458  fzm1  9911  fzrevral  9916  fzshftral  9919  nn0disj  9946  fzoss2  9980  fzosubel  10002  fzosubel3  10004  fzocatel  10007  fzosplitsnm1  10017  qtri3or  10051  exbtwnzlemstep  10056  exbtwnzlemex  10058  rebtwn2zlemstep  10061  rebtwn2z  10063  flqaddz  10101  flqzadd  10102  2tnp1ge0ge0  10105  ceiqm1l  10115  intqfrac2  10123  intfracq  10124  flqdiv  10125  modqvalr  10129  flqpmodeq  10131  modq0  10133  mulqmod0  10134  modqlt  10137  modqdiffl  10139  modqfrac  10141  flqmod  10142  intqfrac  10143  modqmulnn  10146  modqvalp1  10147  modqcyc  10163  modqcyc2  10164  modqadd1  10165  mulqaddmodid  10168  mulp1mod1  10169  modqmul1  10181  modqmul12d  10182  modqnegd  10183  modqmulmodr  10194  modqdi  10196  modqsubdir  10197  modfzo0difsn  10199  modsumfzodifsn  10200  addmodlteq  10202  frecfzen2  10231  uzennn  10240  uzsinds  10246  seq3shft2  10277  monoord2  10281  iseqf1olemab  10293  seq3f1olemqsumkj  10302  seq3f1olemqsum  10304  expaddzaplem  10367  sqoddm1div8  10475  bcm1k  10538  bcp1nk  10540  bcpasc  10544  hashfz  10599  hashfzo  10600  hashfzp1  10602  seq3coll  10617  seq3shft  10642  fzomaxdif  10917  climshft2  11107  iserex  11140  iser3shft  11147  serf0  11153  fsumm1  11217  fsumsplitsnun  11220  fsump1  11221  fsumshftm  11246  fisumrev2  11247  telfsumo  11267  fsumparts  11271  binomlem  11284  isumshft  11291  isumsplit  11292  isum1p  11293  divcnv  11298  arisum  11299  trireciplem  11301  cvgratnnlemmn  11326  cvgratnnlemsumlt  11329  mertenslemi1  11336  ntrivcvgap  11349  eirraplem  11519  moddvds  11538  dvdscmulr  11558  dvdsmulcr  11559  dvds2ln  11562  dvdsadd2b  11576  fzocongeq  11592  addmodlteqALT  11593  dvdsexp  11595  dvdsmod  11596  mulmoddvds  11597  odd2np1  11606  oddm1even  11608  oexpneg  11610  mulsucdiv2z  11618  zob  11624  ltoddhalfle  11626  divalglemnn  11651  divalglemqt  11652  divalglemex  11655  divalglemeuneg  11656  divalgb  11658  divalgmod  11660  modremain  11662  flodddiv4  11667  infssuzex  11678  dvdsbnd  11681  gcdaddm  11708  modgcd  11715  gcdmultipled  11717  dvdsgcdidd  11718  bezoutlemnewy  11720  bezoutlemaz  11727  bezoutlembz  11728  dvdsmulgcd  11749  rplpwr  11751  lcmval  11780  lcmcllem  11784  lcmid  11797  mulgcddvds  11811  divgcdcoprm0  11818  cncongr1  11820  cncongr2  11821  rpexp  11867  sqrt2irrlem  11875  sqrt2irrap  11894  qmuldeneqnum  11909  numdensq  11916  qden1elz  11919  hashdvds  11933  phiprm  11935  hashgcdlem  11939  znnen  11947  relogbexpap  13083  logbgcd1irraplemap  13094