Theorem zcnd 9748

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8167  ℤcz 9623

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 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 8261

This theorem 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 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-neg 8490  df-z 9624

This theorem is referenced by:  qapne  10018  ltesubnnd  10149  fzsplit3  10436  fzspl  10454  fzm1  10485  fzrevral  10490  fzshftral  10493  nn0disj  10523  fzoss2  10559  fzo0addelr  10585  elfzoext  10588  fzosubel  10590  fzosubel3  10592  fzocatel  10595  fzosplitsnm1  10605  infssuzex  10644  zsupssdc  10651  qtri3or  10653  exbtwnzlemstep  10660  exbtwnzlemex  10662  rebtwn2zlemstep  10665  rebtwn2z  10667  flqaddz  10710  flqzadd  10711  2tnp1ge0ge0  10714  ceiqm1l  10726  intqfrac2  10734  intfracq  10735  flqdiv  10736  modqvalr  10740  flqpmodeq  10742  modq0  10744  mulqmod0  10745  modqlt  10748  modqdiffl  10750  modqfrac  10752  flqmod  10753  intqfrac  10754  modqmulnn  10757  modqvalp1  10758  modqcyc  10774  modqcyc2  10775  modqadd1  10776  mulqaddmodid  10779  mulp1mod1  10780  modqmul1  10792  modqmul12d  10793  modqnegd  10794  modqmulmodr  10805  modqdi  10807  modqsubdir  10808  modfzo0difsn  10810  modsumfzodifsn  10811  addmodlteq  10813  frecfzen2  10842  uzennn  10851  uzsinds  10859  seq3shft2  10896  monoord2  10901  iseqf1olemab  10917  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seqf1oglem1  10934  seqf1oglem2  10935  expaddzaplem  10997  modqexp  11082  sqoddm1div8  11109  bcm1k  11176  bcp1nk  11178  bcpasc  11182  bcm1n  11185  hashfz  11240  hashfzo  11241  hashfzp1  11243  hashfibclem  11260  seq3coll  11272  ccatval3  11345  ccatlid  11352  ccatass  11354  ccatalpha  11359  swrdfv0  11404  swrdfv2  11413  swrds1  11418  ccatswrd  11420  pfxfv  11434  ccatpfx  11451  swrdpfx  11457  pfxccatin12lem2  11481  seq3shft  11581  fzomaxdif  11857  climshft2  12050  iserex  12083  iser3shft  12090  serf0  12096  fsumm1  12161  fsumsplitsnun  12164  fsump1  12165  fsumshftm  12190  fisumrev2  12191  telfsumo  12211  fsumparts  12215  binomlem  12228  isumshft  12235  isumsplit  12236  isum1p  12237  divcnv  12242  arisum  12243  trireciplem  12245  cvgratnnlemmn  12270  cvgratnnlemsumlt  12273  mertenslemi1  12280  ntrivcvgap  12293  fprodm1  12343  fprodp1  12345  fprodfac  12360  fprodrev  12364  fprodmodd  12386  eirraplem  12522  moddvds  12544  dvdscmulr  12565  dvdsmulcr  12566  dvds2ln  12569  dvdsadd2b  12585  dvdsaddre2b  12586  fsumdvds  12587  fzocongeq  12603  addmodlteqALT  12604  dvdsexp  12606  dvdsmod  12607  mulmoddvds  12608  3dvds  12609  odd2np1  12618  oddm1even  12620  oexpneg  12622  mulsucdiv2z  12630  zob  12636  ltoddhalfle  12638  divalglemnn  12663  divalglemqt  12664  divalglemex  12667  divalglemeuneg  12668  divalgb  12670  divalgmod  12672  modremain  12674  flodddiv4  12681  bitsp1  12696  bitsfzo  12700  bitsmod  12701  bitsinv1lem  12706  dvdsbnd  12711  gcdaddm  12739  modgcd  12746  gcdmultipled  12748  dvdsgcdidd  12749  bezoutlemnewy  12751  bezoutlemaz  12758  bezoutlembz  12759  dvdsmulgcd  12780  rplpwr  12782  uzwodc  12792  lcmval  12819  lcmcllem  12823  lcmid  12836  mulgcddvds  12850  divgcdcoprm0  12857  cncongr1  12859  cncongr2  12860  rpexp  12909  sqrt2irrlem  12917  sqrt2irrap  12936  qmuldeneqnum  12951  numdensq  12958  qden1elz  12961  hashdvds  12977  phiprm  12979  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  fermltl  12990  prmdiv  12991  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  modprm0  13011  modprmn0modprm0  13013  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem15  13035  pcpremul  13050  pceulem  13051  pceu  13052  pczpre  13054  pcdiv  13059  pcqmul  13060  pcqdiv  13064  pcexp  13066  pcaddlem  13096  pcadd  13097  fldivp1  13105  pcfac  13107  pcbc  13108  prmpwdvds  13112  4sqlem5  13139  4sqlem8  13142  4sqlem9  13143  4sqlem10  13144  4sqlemffi  13153  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  4sqlem14  13161  4sqlem16  13163  4sqlem17  13164  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsgt1  13232  ballotfilemsdom  13233  ballotfilemsel1i  13234  ballotfilemsf1o  13235  ballotfilemsima  13237  ballotfilemfrceq  13250  ballotfilemfrcn0  13251  ballotfilem1ri  13256  znnen  13267  mulgsubcl  13916  mulgdirlem  13933  mulgdir  13934  mulgass  13939  mulgmodid  13941  mulgsubdir  13942  gzsumconst  14120  gzsumsnfd  14124  gzsumsplit0  14125  gzsumshift  14126  gzsumgsum  14132  zringmulg  14905  zndvds0  14957  znf1o  14958  znunit  14966  logfac  15918  relogbexpap  15983  logbgcd1irraplemap  15994  wilthlem1  16008  lgslem1  16033  lgsval2lem  16043  lgsval4a  16055  lgsneg  16057  lgsneg1  16058  lgsmod  16059  lgsdirprm  16067  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsabs1  16072  lgssq  16073  lgssq2  16074  lgsmulsqcoprm  16079  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem1  16094  gausslemma2dlem4  16097  gausslemma2dlem5a  16098  gausslemma2dlem5  16099  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquadlem1  16110  lgsquad2lem1  16114  lgsquad3  16117  2lgslem1b  16122  2lgsoddprmlem2  16139  2sqlem3  16150  2sqlem4  16151  2sqlem8a  16155  2sqlem8  16156  clwwlkccatlem  16555  iswomni0  17006