Theorem zcnd 9780

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8183  ℤcz 9655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8277

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656

This theorem is used by:  qapne  10055  ltesubnnd  10187  fzsplit3  10475  fzspl  10493  fzm1  10524  fzrevral  10529  fzshftral  10532  nn0disj  10562  fzoss2  10598  fzo0addelr  10624  elfzoext  10627  fzosubel  10629  fzosubel3  10631  fzocatel  10634  fzosplitsnm1  10644  infssuzex  10683  zsupssdc  10690  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemex  10701  rebtwn2zlemstep  10704  rebtwn2z  10706  flqaddz  10753  flqzadd  10754  2tnp1ge0ge0  10757  ceiqm1l  10769  intqfrac2  10777  intfracq  10778  flqdiv  10779  modqvalr  10783  flqpmodeq  10785  modq0  10787  mulqmod0  10788  modqlt  10791  modqdiffl  10793  modqfrac  10795  flqmod  10796  intqfrac  10797  modqmulnn  10800  modqvalp1  10801  modqcyc  10817  modqcyc2  10818  modqadd1  10819  mulqaddmodid  10822  mulp1mod1  10823  modqmul1  10835  modqmul12d  10836  modqnegd  10837  modqmulmodr  10848  modqdi  10850  modqsubdir  10851  modfzo0difsn  10853  modsumfzodifsn  10854  addmodlteq  10856  frecfzen2  10885  uzennn  10894  uzsinds  10902  seq3shft2  10939  monoord2  10944  iseqf1olemab  10960  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seqf1oglem1  10977  seqf1oglem2  10978  expaddzaplem  11040  modqexp  11125  sqoddm1div8  11152  bcm1k  11220  bcp1nk  11222  bcpasc  11226  bcm1n  11229  hashfz  11284  hashfzo  11285  hashfzp1  11287  hashfibclem  11304  seq3coll  11316  ccatval3  11389  ccatlid  11396  ccatass  11398  ccatalpha  11403  swrdfv0  11448  swrdfv2  11457  swrds1  11462  ccatswrd  11464  pfxfv  11478  ccatpfx  11495  swrdpfx  11501  pfxccatin12lem2  11525  seq3shft  11625  fzomaxdif  11902  climshft2  12097  iserex  12130  iser3shft  12137  serf0  12143  fsumm1  12208  fsumsplitsnun  12211  fsump1  12212  fsumshftm  12237  fisumrev2  12238  telfsumo  12258  fsumparts  12262  binomlem  12275  isumshft  12282  isumsplit  12283  isum1p  12284  divcnv  12289  arisum  12290  trireciplem  12292  cvgratnnlemmn  12317  cvgratnnlemsumlt  12320  mertenslemi1  12327  ntrivcvgap  12340  fprodm1  12390  fprodp1  12392  fprodfac  12407  fprodrev  12411  fprodmodd  12433  eirraplem  12569  moddvds  12591  dvdscmulr  12612  dvdsmulcr  12613  dvds2ln  12616  dvdsadd2b  12632  dvdsaddre2b  12633  fsumdvds  12634  fzocongeq  12650  addmodlteqALT  12651  dvdsexp  12653  dvdsmod  12654  mulmoddvds  12655  3dvds  12656  odd2np1  12665  oddm1even  12667  oexpneg  12669  mulsucdiv2z  12677  zob  12683  ltoddhalfle  12685  divalglemnn  12710  divalglemqt  12711  divalglemex  12714  divalglemeuneg  12715  divalgb  12717  divalgmod  12719  modremain  12721  flodddiv4  12728  bitsp1  12743  bitsfzo  12747  bitsmod  12748  bitsinv1lem  12753  dvdsbnd  12758  gcdaddm  12786  modgcd  12793  gcdmultipled  12795  dvdsgcdidd  12796  bezoutlemnewy  12798  bezoutlemaz  12805  bezoutlembz  12806  dvdsmulgcd  12827  rplpwr  12829  uzwodc  12839  lcmval  12866  lcmcllem  12870  lcmid  12883  mulgcddvds  12897  divgcdcoprm0  12904  cncongr1  12906  cncongr2  12907  rpexp  12957  sqrt2irrlem  12965  sqrt2irrap  12985  qmuldeneqnum  13000  numdensq  13007  qden1elz  13010  hashdvds  13028  phiprm  13030  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  fermltl  13041  prmdiv  13042  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  modprm0  13062  modprmn0modprm0  13064  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem15  13086  pcpremul  13101  pceulem  13102  pceu  13103  pczpre  13105  pcdiv  13110  pcqmul  13111  pcqdiv  13115  pcexp  13117  pcaddlem  13147  pcadd  13148  fldivp1  13156  pcfac  13158  pcbc  13159  prmpwdvds  13163  4sqlem5  13190  4sqlem8  13193  4sqlem9  13194  4sqlem10  13195  4sqlemffi  13204  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem14  13212  4sqlem16  13214  4sqlem17  13215  prmlem0  13249  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsgt1  13312  ballotfilemsdom  13313  ballotfilemsel1i  13314  ballotfilemsf1o  13315  ballotfilemsima  13317  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilem1ri  13336  znnen  13347  mulgsubcl  13998  mulgdirlem  14015  mulgdir  14016  mulgass  14021  mulgmodid  14023  mulgsubdir  14024  gzsumconst  14233  gzsumsnfd  14237  gzsumsplit0  14238  gzsumshift  14239  gzsumgsum  14245  zringmulg  15042  zndvds0  15094  znf1o  15095  znunit  15103  logfac  16126  relogbexpap  16194  logbgcd1irraplemap  16205  wilthlem1  16232  ppiqub  16293  chtqub  16296  pcbcctr  16303  bcmono  16304  bposlem5  16315  bposlem6  16316  lgslem1  16324  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsneg1  16349  lgsmod  16350  lgsdirprm  16358  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsabs1  16363  lgssq  16364  lgssq2  16365  lgsmulsqcoprm  16370  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem1  16385  gausslemma2dlem4  16388  gausslemma2dlem5a  16389  gausslemma2dlem5  16390  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquad2lem1  16405  lgsquad3  16408  2lgslem1b  16413  2lgsoddprmlem2  16430  2sqlem3  16441  2sqlem4  16442  2sqlem8a  16446  2sqlem8  16447  clwwlkccatlem  16846  iswomni0  17308