Theorem zcnd 9774

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

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

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 8272

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 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  qapne  10049  ltesubnnd  10181  fzsplit3  10469  fzspl  10487  fzm1  10518  fzrevral  10523  fzshftral  10526  nn0disj  10556  fzoss2  10592  fzo0addelr  10618  elfzoext  10621  fzosubel  10623  fzosubel3  10625  fzocatel  10628  fzosplitsnm1  10638  infssuzex  10677  zsupssdc  10684  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  rebtwn2zlemstep  10698  rebtwn2z  10700  flqaddz  10747  flqzadd  10748  2tnp1ge0ge0  10751  ceiqm1l  10763  intqfrac2  10771  intfracq  10772  flqdiv  10773  modqvalr  10777  flqpmodeq  10779  modq0  10781  mulqmod0  10782  modqlt  10785  modqdiffl  10787  modqfrac  10789  flqmod  10790  intqfrac  10791  modqmulnn  10794  modqvalp1  10795  modqcyc  10811  modqcyc2  10812  modqadd1  10813  mulqaddmodid  10816  mulp1mod1  10817  modqmul1  10829  modqmul12d  10830  modqnegd  10831  modqmulmodr  10842  modqdi  10844  modqsubdir  10845  modfzo0difsn  10847  modsumfzodifsn  10848  addmodlteq  10850  frecfzen2  10879  uzennn  10888  uzsinds  10896  seq3shft2  10933  monoord2  10938  iseqf1olemab  10954  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seqf1oglem1  10971  seqf1oglem2  10972  expaddzaplem  11034  modqexp  11119  sqoddm1div8  11146  bcm1k  11214  bcp1nk  11216  bcpasc  11220  bcm1n  11223  hashfz  11278  hashfzo  11279  hashfzp1  11281  hashfibclem  11298  seq3coll  11310  ccatval3  11383  ccatlid  11390  ccatass  11392  ccatalpha  11397  swrdfv0  11442  swrdfv2  11451  swrds1  11456  ccatswrd  11458  pfxfv  11472  ccatpfx  11489  swrdpfx  11495  pfxccatin12lem2  11519  seq3shft  11619  fzomaxdif  11896  climshft2  12091  iserex  12124  iser3shft  12131  serf0  12137  fsumm1  12202  fsumsplitsnun  12205  fsump1  12206  fsumshftm  12231  fisumrev2  12232  telfsumo  12252  fsumparts  12256  binomlem  12269  isumshft  12276  isumsplit  12277  isum1p  12278  divcnv  12283  arisum  12284  trireciplem  12286  cvgratnnlemmn  12311  cvgratnnlemsumlt  12314  mertenslemi1  12321  ntrivcvgap  12334  fprodm1  12384  fprodp1  12386  fprodfac  12401  fprodrev  12405  fprodmodd  12427  eirraplem  12563  moddvds  12585  dvdscmulr  12606  dvdsmulcr  12607  dvds2ln  12610  dvdsadd2b  12626  dvdsaddre2b  12627  fsumdvds  12628  fzocongeq  12644  addmodlteqALT  12645  dvdsexp  12647  dvdsmod  12648  mulmoddvds  12649  3dvds  12650  odd2np1  12659  oddm1even  12661  oexpneg  12663  mulsucdiv2z  12671  zob  12677  ltoddhalfle  12679  divalglemnn  12704  divalglemqt  12705  divalglemex  12708  divalglemeuneg  12709  divalgb  12711  divalgmod  12713  modremain  12715  flodddiv4  12722  bitsp1  12737  bitsfzo  12741  bitsmod  12742  bitsinv1lem  12747  dvdsbnd  12752  gcdaddm  12780  modgcd  12787  gcdmultipled  12789  dvdsgcdidd  12790  bezoutlemnewy  12792  bezoutlemaz  12799  bezoutlembz  12800  dvdsmulgcd  12821  rplpwr  12823  uzwodc  12833  lcmval  12860  lcmcllem  12864  lcmid  12877  mulgcddvds  12891  divgcdcoprm0  12898  cncongr1  12900  cncongr2  12901  rpexp  12951  sqrt2irrlem  12959  sqrt2irrap  12979  qmuldeneqnum  12994  numdensq  13001  qden1elz  13004  hashdvds  13022  phiprm  13024  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  fermltl  13035  prmdiv  13036  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  modprm0  13056  modprmn0modprm0  13058  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem15  13080  pcpremul  13095  pceulem  13096  pceu  13097  pczpre  13099  pcdiv  13104  pcqmul  13105  pcqdiv  13109  pcexp  13111  pcaddlem  13141  pcadd  13142  fldivp1  13150  pcfac  13152  pcbc  13153  prmpwdvds  13157  4sqlem5  13184  4sqlem8  13187  4sqlem9  13188  4sqlem10  13189  4sqlemffi  13198  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem14  13206  4sqlem16  13208  4sqlem17  13209  prmlem0  13243  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsgt1  13306  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsf1o  13309  ballotfilemsima  13311  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilem1ri  13330  znnen  13341  mulgsubcl  13992  mulgdirlem  14009  mulgdir  14010  mulgass  14015  mulgmodid  14017  mulgsubdir  14018  gzsumconst  14227  gzsumsnfd  14231  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  zringmulg  15017  zndvds0  15069  znf1o  15070  znunit  15078  logfac  16090  relogbexpap  16155  logbgcd1irraplemap  16166  wilthlem1  16193  ppiqub  16254  chtqub  16257  pcbcctr  16264  bcmono  16265  bposlem5  16276  bposlem6  16277  lgslem1  16285  lgsval2lem  16295  lgsval4a  16307  lgsneg  16309  lgsneg1  16310  lgsmod  16311  lgsdirprm  16319  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsabs1  16324  lgssq  16325  lgssq2  16326  lgsmulsqcoprm  16331  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem1  16346  gausslemma2dlem4  16349  gausslemma2dlem5a  16350  gausslemma2dlem5  16351  gausslemma2dlem6  16352  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquadlem1  16362  lgsquad2lem1  16366  lgsquad3  16369  2lgslem1b  16374  2lgsoddprmlem2  16391  2sqlem3  16402  2sqlem4  16403  2sqlem8a  16407  2sqlem8  16408  clwwlkccatlem  16807  iswomni0  17268