Theorem zcnd 9468

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℤcz 9345

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8219  df-z 9346

This theorem is referenced by:  qapne  9732  fzm1  10194  fzrevral  10199  fzshftral  10202  nn0disj  10232  fzoss2  10267  fzosubel  10289  fzosubel3  10291  fzocatel  10294  fzosplitsnm1  10304  infssuzex  10342  zsupssdc  10347  qtri3or  10349  exbtwnzlemstep  10356  exbtwnzlemex  10358  rebtwn2zlemstep  10361  rebtwn2z  10363  flqaddz  10406  flqzadd  10407  2tnp1ge0ge0  10410  ceiqm1l  10422  intqfrac2  10430  intfracq  10431  flqdiv  10432  modqvalr  10436  flqpmodeq  10438  modq0  10440  mulqmod0  10441  modqlt  10444  modqdiffl  10446  modqfrac  10448  flqmod  10449  intqfrac  10450  modqmulnn  10453  modqvalp1  10454  modqcyc  10470  modqcyc2  10471  modqadd1  10472  mulqaddmodid  10475  mulp1mod1  10476  modqmul1  10488  modqmul12d  10489  modqnegd  10490  modqmulmodr  10501  modqdi  10503  modqsubdir  10504  modfzo0difsn  10506  modsumfzodifsn  10507  addmodlteq  10509  frecfzen2  10538  uzennn  10547  uzsinds  10555  seq3shft2  10592  monoord2  10597  iseqf1olemab  10613  seq3f1olemqsumkj  10622  seq3f1olemqsum  10624  seqf1oglem1  10630  seqf1oglem2  10631  expaddzaplem  10693  modqexp  10777  sqoddm1div8  10804  bcm1k  10871  bcp1nk  10873  bcpasc  10877  hashfz  10932  hashfzo  10933  hashfzp1  10935  seq3coll  10953  seq3shft  11022  fzomaxdif  11297  climshft2  11490  iserex  11523  iser3shft  11530  serf0  11536  fsumm1  11600  fsumsplitsnun  11603  fsump1  11604  fsumshftm  11629  fisumrev2  11630  telfsumo  11650  fsumparts  11654  binomlem  11667  isumshft  11674  isumsplit  11675  isum1p  11676  divcnv  11681  arisum  11682  trireciplem  11684  cvgratnnlemmn  11709  cvgratnnlemsumlt  11712  mertenslemi1  11719  ntrivcvgap  11732  fprodm1  11782  fprodp1  11784  fprodfac  11799  fprodrev  11803  fprodmodd  11825  eirraplem  11961  moddvds  11983  dvdscmulr  12004  dvdsmulcr  12005  dvds2ln  12008  dvdsadd2b  12024  dvdsaddre2b  12025  fsumdvds  12026  fzocongeq  12042  addmodlteqALT  12043  dvdsexp  12045  dvdsmod  12046  mulmoddvds  12047  3dvds  12048  odd2np1  12057  oddm1even  12059  oexpneg  12061  mulsucdiv2z  12069  zob  12075  ltoddhalfle  12077  divalglemnn  12102  divalglemqt  12103  divalglemex  12106  divalglemeuneg  12107  divalgb  12109  divalgmod  12111  modremain  12113  flodddiv4  12120  bitsp1  12135  bitsfzo  12139  bitsmod  12140  bitsinv1lem  12145  dvdsbnd  12150  gcdaddm  12178  modgcd  12185  gcdmultipled  12187  dvdsgcdidd  12188  bezoutlemnewy  12190  bezoutlemaz  12197  bezoutlembz  12198  dvdsmulgcd  12219  rplpwr  12221  uzwodc  12231  lcmval  12258  lcmcllem  12262  lcmid  12275  mulgcddvds  12289  divgcdcoprm0  12296  cncongr1  12298  cncongr2  12299  rpexp  12348  sqrt2irrlem  12356  sqrt2irrap  12375  qmuldeneqnum  12390  numdensq  12397  qden1elz  12400  hashdvds  12416  phiprm  12418  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  fermltl  12429  prmdiv  12430  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  modprm0  12450  modprmn0modprm0  12452  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem15  12474  pcpremul  12489  pceulem  12490  pceu  12491  pczpre  12493  pcdiv  12498  pcqmul  12499  pcqdiv  12503  pcexp  12505  pcaddlem  12535  pcadd  12536  fldivp1  12544  pcfac  12546  pcbc  12547  prmpwdvds  12551  4sqlem5  12578  4sqlem8  12581  4sqlem9  12582  4sqlem10  12583  4sqlemffi  12592  4sqexercise2  12595  4sqlemsdc  12596  4sqlem11  12597  4sqlem14  12600  4sqlem16  12602  4sqlem17  12603  znnen  12642  mulgsubcl  13344  mulgdirlem  13361  mulgdir  13362  mulgass  13367  mulgmodid  13369  mulgsubdir  13370  gsumfzconst  13549  gsumfzsnfd  13553  zringmulg  14232  zndvds0  14284  znf1o  14285  znunit  14293  relogbexpap  15302  logbgcd1irraplemap  15313  wilthlem1  15324  lgslem1  15349  lgsval2lem  15359  lgsval4a  15371  lgsneg  15373  lgsneg1  15374  lgsmod  15375  lgsdirprm  15383  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsabs1  15388  lgssq  15389  lgssq2  15390  lgsmulsqcoprm  15395  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem1  15410  gausslemma2dlem4  15413  gausslemma2dlem5a  15414  gausslemma2dlem5  15415  gausslemma2dlem6  15416  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquad2lem1  15430  lgsquad3  15433  2lgslem1b  15438  2lgsoddprmlem2  15455  2sqlem3  15466  2sqlem4  15467  2sqlem8a  15471  2sqlem8  15472  iswomni0  15808