Theorem zcnd 9603

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  qapne  9873  fzm1  10335  fzrevral  10340  fzshftral  10343  nn0disj  10373  fzoss2  10409  fzo0addelr  10435  elfzoext  10438  fzosubel  10440  fzosubel3  10442  fzocatel  10445  fzosplitsnm1  10455  infssuzex  10494  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  rebtwn2zlemstep  10513  rebtwn2z  10515  flqaddz  10558  flqzadd  10559  2tnp1ge0ge0  10562  ceiqm1l  10574  intqfrac2  10582  intfracq  10583  flqdiv  10584  modqvalr  10588  flqpmodeq  10590  modq0  10592  mulqmod0  10593  modqlt  10596  modqdiffl  10598  modqfrac  10600  flqmod  10601  intqfrac  10602  modqmulnn  10605  modqvalp1  10606  modqcyc  10622  modqcyc2  10623  modqadd1  10624  mulqaddmodid  10627  mulp1mod1  10628  modqmul1  10640  modqmul12d  10641  modqnegd  10642  modqmulmodr  10653  modqdi  10655  modqsubdir  10656  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecfzen2  10690  uzennn  10699  uzsinds  10707  seq3shft2  10744  monoord2  10749  iseqf1olemab  10765  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seqf1oglem1  10782  seqf1oglem2  10783  expaddzaplem  10845  modqexp  10929  sqoddm1div8  10956  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashfz  11086  hashfzo  11087  hashfzp1  11089  seq3coll  11107  ccatval3  11180  ccatlid  11187  ccatass  11189  ccatalpha  11194  swrdfv0  11239  swrdfv2  11248  swrds1  11253  ccatswrd  11255  pfxfv  11269  ccatpfx  11286  swrdpfx  11292  pfxccatin12lem2  11316  seq3shft  11403  fzomaxdif  11678  climshft2  11871  iserex  11904  iser3shft  11911  serf0  11917  fsumm1  11982  fsumsplitsnun  11985  fsump1  11986  fsumshftm  12011  fisumrev2  12012  telfsumo  12032  fsumparts  12036  binomlem  12049  isumshft  12056  isumsplit  12057  isum1p  12058  divcnv  12063  arisum  12064  trireciplem  12066  cvgratnnlemmn  12091  cvgratnnlemsumlt  12094  mertenslemi1  12101  ntrivcvgap  12114  fprodm1  12164  fprodp1  12166  fprodfac  12181  fprodrev  12185  fprodmodd  12207  eirraplem  12343  moddvds  12365  dvdscmulr  12386  dvdsmulcr  12387  dvds2ln  12390  dvdsadd2b  12406  dvdsaddre2b  12407  fsumdvds  12408  fzocongeq  12424  addmodlteqALT  12425  dvdsexp  12427  dvdsmod  12428  mulmoddvds  12429  3dvds  12430  odd2np1  12439  oddm1even  12441  oexpneg  12443  mulsucdiv2z  12451  zob  12457  ltoddhalfle  12459  divalglemnn  12484  divalglemqt  12485  divalglemex  12488  divalglemeuneg  12489  divalgb  12491  divalgmod  12493  modremain  12495  flodddiv4  12502  bitsp1  12517  bitsfzo  12521  bitsmod  12522  bitsinv1lem  12527  dvdsbnd  12532  gcdaddm  12560  modgcd  12567  gcdmultipled  12569  dvdsgcdidd  12570  bezoutlemnewy  12572  bezoutlemaz  12579  bezoutlembz  12580  dvdsmulgcd  12601  rplpwr  12603  uzwodc  12613  lcmval  12640  lcmcllem  12644  lcmid  12657  mulgcddvds  12671  divgcdcoprm0  12678  cncongr1  12680  cncongr2  12681  rpexp  12730  sqrt2irrlem  12738  sqrt2irrap  12757  qmuldeneqnum  12772  numdensq  12779  qden1elz  12782  hashdvds  12798  phiprm  12800  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  fermltl  12811  prmdiv  12812  prmdiveq  12813  hashgcdlem  12815  odzdvds  12823  modprm0  12832  modprmn0modprm0  12834  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem15  12856  pcpremul  12871  pceulem  12872  pceu  12873  pczpre  12875  pcdiv  12880  pcqmul  12881  pcqdiv  12885  pcexp  12887  pcaddlem  12917  pcadd  12918  fldivp1  12926  pcfac  12928  pcbc  12929  prmpwdvds  12933  4sqlem5  12960  4sqlem8  12963  4sqlem9  12964  4sqlem10  12965  4sqlemffi  12974  4sqexercise2  12977  4sqlemsdc  12978  4sqlem11  12979  4sqlem14  12982  4sqlem16  12984  4sqlem17  12985  znnen  13024  mulgsubcl  13728  mulgdirlem  13745  mulgdir  13746  mulgass  13751  mulgmodid  13753  mulgsubdir  13754  gsumfzconst  13933  gsumfzsnfd  13937  gsumsplit0  13938  zringmulg  14618  zndvds0  14670  znf1o  14671  znunit  14679  relogbexpap  15688  logbgcd1irraplemap  15699  wilthlem1  15710  lgslem1  15735  lgsval2lem  15745  lgsval4a  15757  lgsneg  15759  lgsneg1  15760  lgsmod  15761  lgsdirprm  15769  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsabs1  15774  lgssq  15775  lgssq2  15776  lgsmulsqcoprm  15781  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem1  15796  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  gausslemma2dlem5  15801  gausslemma2dlem6  15802  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlem1  15812  lgsquad2lem1  15816  lgsquad3  15819  2lgslem1b  15824  2lgsoddprmlem2  15841  2sqlem3  15852  2sqlem4  15853  2sqlem8a  15857  2sqlem8  15858  clwwlkccatlem  16257  iswomni0  16681  gsumgfsumlem  16709  gsumgfsum  16710