Theorem zcnd 12091

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10537  ℤcz 11984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-neg 10875  df-z 11985

This theorem is referenced by:  zsupss  12340  rpnnen1lem5  12383  fzm1  12990  fzrevral  12995  fzshftral  12998  nn0disj  13026  predfz  13035  fzoss2  13068  fzo0addelr  13095  fzosubel  13099  fzosubel3  13101  fzocatel  13104  fzosplitsnm1  13115  elfzom1elp1fzo1  13140  2tnp1ge0ge0  13202  quoremz  13226  intfrac2  13229  intfracq  13230  flpmodeq  13245  moddiffl  13253  modmul1  13295  modmul12d  13296  modfzo0difsn  13314  modsumfzodifsn  13315  addmodlteq  13317  uzrdgxfr  13338  fzen2  13340  monoord2  13404  seqf1olem1  13412  seqf1olem2  13413  seqz  13421  expaddzlem  13475  znsqcld  13529  modexp  13602  sqoddm1div8  13607  bcm1k  13678  bcp1nk  13680  bcval5  13681  bcpasc  13684  hashfz  13791  hashfzo  13793  hashfzp1  13795  hashbclem  13813  seqcoll  13825  ccatval3  13935  ccatlid  13942  ccatass  13944  ccatalpha  13949  swrdfv0  14013  swrdfv2  14025  swrds1  14030  ccatswrd  14032  pfxfv  14046  ccatpfx  14065  swrdpfx  14071  pfxccatin12lem2  14095  spllen  14118  revccat  14130  revrev  14131  cshwidxmod  14167  cshwidxm1  14171  cshweqrep  14185  2cshwcshw  14189  cshimadifsn0  14194  swrds2m  14305  seqshft  14446  fzomaxdif  14705  climshft2  14941  iserex  15015  isercoll2  15027  serf0  15039  iseraltlem2  15041  iseraltlem3  15042  iseralt  15043  sumrblem  15070  fsumm1  15108  fsumsplitsnun  15112  fsump1  15113  fsumshftm  15138  fsumrev2  15139  telfsumo  15159  fsumparts  15163  binomlem  15186  isumshft  15196  isumsplit  15197  isum1p  15198  arisum  15217  pwdif  15225  cvgrat  15241  mertenslem1  15242  ntrivcvg  15255  ntrivcvgtail  15258  prodrblem  15285  fprodser  15305  fprodm1  15323  fprodp1  15325  fprodrev  15333  fprodmodd  15353  fallfacval3  15368  fallfacfwd  15392  0fallfac  15393  binomfallfaclem2  15396  fallfacval4  15399  fsumkthpow  15412  eirrlem  15559  sqrt2irrlem  15603  dvds2ln  15644  dvdsadd2b  15658  fsumdvds  15660  fzocongeq  15676  addmodlteqALT  15677  dvdsexp  15679  dvdsmod  15680  3dvds  15682  fprodfvdvdsd  15685  odd2np1  15692  oddm1even  15694  oexpneg  15696  mod2eq1n2dvds  15698  mulsucdiv2z  15704  zob  15710  ltoddhalfle  15712  sumodd  15741  pwp1fsum  15744  divalglem0  15746  divalglem4  15749  divalglem8  15753  divalgb  15757  divalgmod  15759  modremain  15761  flodddiv4  15766  bitsp1  15782  bitsfzo  15786  bitsmod  15787  bitsinv1lem  15792  bitsf1  15797  sadaddlem  15817  bitsres  15824  bitsuz  15825  bitsshft  15826  smumullem  15843  modgcd  15882  gcdmultipled  15884  dvdsgcdidd  15887  bezoutlem1  15889  bezoutlem2  15890  bezoutlem3  15891  bezoutlem4  15892  dvdsmulgcd  15907  rplpwr  15909  lcmid  15955  absprodnn  15964  mulgcddvds  16001  divgcdcoprm0  16011  cncongr1  16013  cncongr2  16014  rpexp  16066  qmuldeneqnum  16089  numdensq  16096  qden1elz  16099  hashdvds  16114  phiprm  16116  eulerthlem2  16121  fermltl  16123  prmdiv  16124  prmdiveq  16125  hashgcdlem  16127  odzdvds  16134  vfermltlALT  16141  modprm0  16144  modprmn0modprm0  16146  pythagtriplem6  16160  pythagtriplem7  16161  pythagtriplem15  16168  pcpremul  16182  pceulem  16184  pczpre  16186  pcdiv  16191  pcqmul  16192  pcqdiv  16196  pcexp  16198  pcaddlem  16226  pcadd  16227  fldivp1  16235  pcfac  16237  pcbc  16238  prmpwdvds  16242  prmreclem4  16257  4sqlem5  16280  4sqlem8  16283  4sqlem9  16284  4sqlem10  16285  4sqlem11  16293  4sqlem14  16296  4sqlem16  16298  4sqlem17  16299  vdwapun  16312  vdwnnlem2  16334  prmop1  16376  prmdvdsprmo  16380  prmgaplem7  16395  prmlem0  16441  mulgsubcl  18244  mulgdirlem  18260  mulgdir  18261  mulgass  18266  mulgmodid  18268  mulgsubdir  18269  psgnunilem5  18624  psgnunilem2  18625  psgnunilem4  18627  m1expaddsub  18628  psgnuni  18629  odnncl  18675  odmulg  18685  odbezout  18687  sylow1lem1  18725  sylow2alem2  18745  efgsres  18866  efgredleme  18871  efgredlemc  18873  odadd1  18970  odadd2  18971  cyggeninv  19004  gsummptshft  19058  ablfacrp  19190  pgpfac1lem3  19201  fincygsubgodd  19236  srgbinomlem3  19294  srgbinomlem4  19295  zringmulg  20627  zringlpirlem1  20633  zringlpirlem3  20635  prmirredlem  20642  zndvds0  20699  znf1o  20700  znunit  20712  cayhamlem1  21476  tgpmulg  22703  zdis  23426  uniioombllem3  24188  mbfi1fseqlem4  24321  dvexp3  24577  aareccl  24917  aalioulem1  24923  geolim3  24930  aaliou3lem2  24934  aaliou3lem6  24939  ulmshft  24980  sineq0  25111  efif1olem2  25129  igamz  25627  wilthlem1  25647  wilthlem2  25648  basellem3  25662  mumul  25760  musum  25770  musumsum  25771  muinv  25772  ppiub  25782  chtub  25790  logfac2  25795  chpchtsum  25797  dchrptlem1  25842  pcbcctr  25854  bcmono  25855  bposlem5  25866  bposlem6  25867  lgslem1  25875  lgsval2lem  25885  lgsval4a  25897  lgsneg  25899  lgsneg1  25900  lgsmod  25901  lgsdirprm  25909  lgsdir  25910  lgsdilem2  25911  lgsdi  25912  lgsne0  25913  lgsabs1  25914  lgssq  25915  lgssq2  25916  lgsmulsqcoprm  25921  lgsdirnn0  25922  lgsdinn0  25923  lgsqrlem1  25924  gausslemma2dlem1a  25943  gausslemma2dlem1  25944  gausslemma2dlem4  25947  gausslemma2dlem5a  25948  gausslemma2dlem5  25949  gausslemma2dlem6  25950  gausslemma2d  25952  lgseisenlem1  25953  lgseisenlem2  25954  lgseisenlem3  25955  lgseisenlem4  25956  lgsquadlem1  25958  lgsquad2lem1  25962  lgsquad3  25965  2lgslem1b  25970  2lgsoddprmlem2  25987  2sqlem3  25998  2sqlem4  25999  2sqlem8a  26003  2sqlem8  26004  2sqlem11  26007  2sqblem  26009  2sqn0  26012  2sqmod  26014  dchrisumlem1  26067  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasum2lem  26074  mudivsum  26108  mulogsum  26110  mulog2sumlem2  26113  selberglem1  26123  selberglem3  26125  selberg  26126  pntpbnd2  26165  pntlemf  26183  padicabvcxp  26210  axlowdimlem14  26743  axlowdimlem16  26745  pthdadjvtx  27513  crctcshwlkn0lem4  27593  crctcshwlkn0lem5  27594  crctcshlem4  27600  crctcsh  27604  clwwlkccatlem  27769  clwwisshclwws  27795  eucrctshift  28024  fzm1ne1  30514  fzspl  30515  bcm1n  30520  fzom1ne1  30526  dvdszzq  30533  prmdvdsbc  30534  numdenneg  30535  divnumden2  30536  ltesubnnd  30540  ccatf1  30627  swrdrn3  30631  swrdf1  30632  cshwrnid  30637  cycpmco2lem3  30772  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2  30777  archiabllem1  30824  archiabllem2c  30826  zrhnm  31212  cnzh  31213  rezh  31214  qqhval2lem  31224  qqhghm  31231  qqhrhm  31232  qqhnm  31233  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemic  31766  ballotlem1c  31767  ballotlemsgt1  31770  ballotlemsdom  31771  ballotlemsel1i  31772  ballotlemsf1o  31773  ballotlemsima  31775  ballotlemfrceq  31788  ballotlemfrcn0  31789  ballotlem1ri  31794  signsplypnf  31822  itgexpif  31879  fsum2dsub  31880  breprexplemc  31905  vtsprod  31912  circlemeth  31913  revpfxsfxrev  32364  swrdrevpfx  32365  revwlk  32373  swrdwlk  32375  divcnvlin  32966  fwddifnp1  33628  knoppndvlem2  33854  knoppndvlem7  33859  knoppndvlem14  33866  knoppndvlem16  33868  ltflcei  34882  poimirlem1  34895  poimirlem2  34896  poimirlem7  34901  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem24  34918  poimirlem31  34925  poimirlem32  34926  fdc  35022  mettrifi  35034  caushft  35038  cntotbnd  35076  oexpreposd  39186  numdenexp  39193  exp11d  39196  mzpsubmpt  39347  lzenom  39374  diophun  39377  eqrabdioph  39381  irrapxlem2  39427  irrapxlem3  39428  pellexlem6  39438  pell1234qrreccl  39458  pellfund14  39502  rmxyneg  39524  rmxyadd  39525  rmxp1  39536  rmxm1  39538  rmym1  39539  rmxluc  39540  rmyluc  39541  rmyluc2  39542  rmxdbl  39543  rmydbl  39544  congadd  39570  congsub  39574  congabseq  39578  acongrep  39584  acongeq  39587  jm2.18  39592  jm2.19lem1  39593  jm2.19lem2  39594  jm2.19lem3  39595  jm2.22  39599  jm2.23  39600  jm2.20nn  39601  jm2.25  39603  jm2.26lem3  39605  jm2.27c  39611  nzss  40656  hashnzfz  40659  hashnzfz2  40660  hashnzfzclim  40661  uzmptshftfval  40685  sineq0ALT  41278  fzisoeu  41574  fperiodmul  41578  monoord2xrv  41767  fmul01lt1lem2  41873  sumnnodd  41918  dvdsn1add  42231  dvnmul  42235  dvnprodlem1  42238  stoweidlem11  42303  stoweidlem26  42318  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkeritg  42394  fourierdlem26  42425  fourierdlem48  42446  fourierdlem49  42447  fourierdlem79  42477  fourierdlem91  42489  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  etransclem1  42527  etransclem4  42530  etransclem8  42534  etransclem9  42535  etransclem15  42541  etransclem17  42543  etransclem18  42544  etransclem20  42546  etransclem21  42547  etransclem22  42548  etransclem23  42549  etransclem24  42550  etransclem25  42551  etransclem35  42561  etransclem38  42564  etransclem41  42567  etransclem44  42570  etransclem45  42571  etransclem46  42572  etransclem47  42573  etransclem48  42574  2elfz2melfz  43525  fsumsplitsndif  43540  iccpartgtprec  43587  fargshiftf1  43608  fargshiftfo  43609  mod42tp1mod8  43774  sfprmdvdsmersenne  43775  lighneallem3  43779  lighneallem4b  43781  modexp2m1d  43784  dfodd6  43809  onego  43818  m1expoddALTV  43820  zofldiv2ALTV  43834  oddflALTV  43835  oexpnegALTV  43849  omoeALTV  43857  omeoALTV  43858  epoo  43875  emoo  43876  epee  43877  emee  43878  evensumeven  43879  evenltle  43889  even3prm2  43891  mogoldbblem  43892  fppr2odd  43903  fpprwppr  43911  fpprwpprb  43912  sbgoldbst  43950  sbgoldbaltlem2  43952  sgoldbeven3prm  43955  nnsum3primesprm  43962  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  bgoldbtbndlem2  43978  bgoldbtbndlem4  43980  bgoldbtbnd  43981  2zrngamnd  44219  2zrngacmnd  44220  2zrngagrp  44221  2zrngALT  44226  2zrngnmlid  44227  2zrngnmlid2  44229  ztprmneprm  44402  altgsumbcALT  44408  fldivmod  44585  m1modmmod  44588  zofldiv2  44598  fllogbd  44627  nnpw2blen  44647  blen1b  44655  blennngt2o2  44659  blennn0e2  44661  dig2nn1st  44672  dignn0flhalflem1  44682