Theorem zcnd 9324

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7761  ℤcz 9201

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7855

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5854  df-neg 8082  df-z 9202

This theorem is referenced by:  qapne  9587  fzm1  10045  fzrevral  10050  fzshftral  10053  nn0disj  10083  fzoss2  10117  fzosubel  10139  fzosubel3  10141  fzocatel  10144  fzosplitsnm1  10154  qtri3or  10188  exbtwnzlemstep  10193  exbtwnzlemex  10195  rebtwn2zlemstep  10198  rebtwn2z  10200  flqaddz  10242  flqzadd  10243  2tnp1ge0ge0  10246  ceiqm1l  10256  intqfrac2  10264  intfracq  10265  flqdiv  10266  modqvalr  10270  flqpmodeq  10272  modq0  10274  mulqmod0  10275  modqlt  10278  modqdiffl  10280  modqfrac  10282  flqmod  10283  intqfrac  10284  modqmulnn  10287  modqvalp1  10288  modqcyc  10304  modqcyc2  10305  modqadd1  10306  mulqaddmodid  10309  mulp1mod1  10310  modqmul1  10322  modqmul12d  10323  modqnegd  10324  modqmulmodr  10335  modqdi  10337  modqsubdir  10338  modfzo0difsn  10340  modsumfzodifsn  10341  addmodlteq  10343  frecfzen2  10372  uzennn  10381  uzsinds  10387  seq3shft2  10418  monoord2  10422  iseqf1olemab  10434  seq3f1olemqsumkj  10443  seq3f1olemqsum  10445  expaddzaplem  10508  modqexp  10591  sqoddm1div8  10618  bcm1k  10683  bcp1nk  10685  bcpasc  10689  hashfz  10745  hashfzo  10746  hashfzp1  10748  seq3coll  10766  seq3shft  10791  fzomaxdif  11066  climshft2  11258  iserex  11291  iser3shft  11298  serf0  11304  fsumm1  11368  fsumsplitsnun  11371  fsump1  11372  fsumshftm  11397  fisumrev2  11398  telfsumo  11418  fsumparts  11422  binomlem  11435  isumshft  11442  isumsplit  11443  isum1p  11444  divcnv  11449  arisum  11450  trireciplem  11452  cvgratnnlemmn  11477  cvgratnnlemsumlt  11480  mertenslemi1  11487  ntrivcvgap  11500  fprodm1  11550  fprodp1  11552  fprodfac  11567  fprodrev  11571  fprodmodd  11593  eirraplem  11728  moddvds  11750  dvdscmulr  11771  dvdsmulcr  11772  dvds2ln  11775  dvdsadd2b  11791  fzocongeq  11807  addmodlteqALT  11808  dvdsexp  11810  dvdsmod  11811  mulmoddvds  11812  odd2np1  11821  oddm1even  11823  oexpneg  11825  mulsucdiv2z  11833  zob  11839  ltoddhalfle  11841  divalglemnn  11866  divalglemqt  11867  divalglemex  11870  divalglemeuneg  11871  divalgb  11873  divalgmod  11875  modremain  11877  flodddiv4  11882  infssuzex  11893  zsupssdc  11898  dvdsbnd  11900  gcdaddm  11928  modgcd  11935  gcdmultipled  11937  dvdsgcdidd  11938  bezoutlemnewy  11940  bezoutlemaz  11947  bezoutlembz  11948  dvdsmulgcd  11969  rplpwr  11971  uzwodc  11981  lcmval  12006  lcmcllem  12010  lcmid  12023  mulgcddvds  12037  divgcdcoprm0  12044  cncongr1  12046  cncongr2  12047  rpexp  12096  sqrt2irrlem  12104  sqrt2irrap  12123  qmuldeneqnum  12138  numdensq  12145  qden1elz  12148  hashdvds  12164  phiprm  12166  eulerthlema  12173  eulerthlemh  12174  eulerthlemth  12175  fermltl  12177  prmdiv  12178  prmdiveq  12179  hashgcdlem  12181  odzdvds  12188  modprm0  12197  modprmn0modprm0  12199  pythagtriplem6  12213  pythagtriplem7  12214  pythagtriplem15  12221  pcpremul  12236  pceulem  12237  pceu  12238  pczpre  12240  pcdiv  12245  pcqmul  12246  pcqdiv  12250  pcexp  12252  pcaddlem  12281  pcadd  12282  fldivp1  12289  pcfac  12291  pcbc  12292  prmpwdvds  12296  4sqlem5  12323  4sqlem8  12326  4sqlem9  12327  4sqlem10  12328  znnen  12342  relogbexpap  13631  logbgcd1irraplemap  13642  lgslem1  13656  lgsval2lem  13666  lgsval4a  13678  lgsneg  13680  lgsneg1  13681  lgsmod  13682  lgsdirprm  13690  lgsdir  13691  lgsdilem2  13692  lgsdi  13693  lgsne0  13694  lgsabs1  13695  lgssq  13696  lgssq2  13697  lgsmulsqcoprm  13702  lgsdirnn0  13703  lgsdinn0  13704  2sqlem3  13708  2sqlem4  13709  2sqlem8a  13713  2sqlem8  13714  iswomni0  14045