Theorem zcnd 12626

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11028  ℤcz 12516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-resscn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-iota 6442  df-fv 6494  df-ov 7360  df-neg 11372  df-z 12517

This theorem is referenced by:  zsupss  12879  rpnnen1lem5  12923  fzm1  13553  fzrevral  13558  fzshftral  13561  nn0disj  13590  predfz  13599  fzoss2  13634  elfzo0suble  13653  fzo0addelr  13666  elfzoext  13669  fzosubel  13671  fzosubel3  13673  fzocatel  13676  fzosplitsnm1  13687  elfzom1elp1fzo1  13714  fzom1ne1  13732  2tnp1ge0ge0  13780  quoremz  13806  intfrac2  13809  intfracq  13810  flpmodeq  13825  moddiffl  13833  modmul1  13878  modmul12d  13879  modfzo0difsn  13897  modsumfzodifsn  13898  addmodlteq  13900  uzrdgxfr  13921  fzen2  13923  monoord2  13987  seqf1olem1  13995  seqf1olem2  13996  seqz  14004  expaddzlem  14059  znsqcld  14116  modexp  14192  sqoddm1div8  14197  bcm1k  14269  bcp1nk  14271  bcval5  14272  bcpasc  14275  hashfz  14381  hashfzo  14383  hashfzp1  14385  hashbclem  14406  seqcoll  14418  ccatval3  14533  ccatlid  14541  ccatass  14543  ccatalpha  14548  swrdfv0  14604  swrdfv2  14616  swrds1  14621  ccatswrd  14623  pfxfv  14637  ccatpfx  14655  swrdpfx  14661  pfxccatin12lem2  14685  spllen  14708  revccat  14720  revrev  14721  cshwidxmod  14757  cshwidxm1  14761  cshweqrep  14775  2cshwcshw  14779  cshimadifsn0  14784  swrds2m  14895  seqshft  15039  fzomaxdif  15298  climshft2  15536  iserex  15611  isercoll2  15623  serf0  15635  iseraltlem2  15637  iseraltlem3  15638  iseralt  15639  sumrblem  15665  fsumm1  15705  fsumsplitsnun  15709  fsump1  15710  fsumshftm  15735  fsumrev2  15736  telfsumo  15757  fsumparts  15761  binomlem  15786  isumshft  15796  isumsplit  15797  isum1p  15798  arisum  15817  pwdif  15825  cvgrat  15840  mertenslem1  15841  ntrivcvg  15854  ntrivcvgtail  15857  prodrblem  15886  fprodser  15906  fprodm1  15924  fprodp1  15926  fprodrev  15934  fprodmodd  15954  fallfacval3  15969  fallfacfwd  15993  0fallfac  15994  binomfallfaclem2  15997  fallfacval4  16000  fsumkthpow  16013  eirrlem  16163  sqrt2irrlem  16207  addmulmodb  16226  dvds2ln  16250  dvdsadd2b  16267  fsumdvds  16269  fzocongeq  16285  addmodlteqALT  16286  dvdsexp  16289  dvdsmod  16290  3dvds  16292  fprodfvdvdsd  16295  odd2np1  16302  oddm1even  16304  oexpneg  16306  mod2eq1n2dvds  16308  mulsucdiv2z  16314  zob  16320  ltoddhalfle  16322  sumodd  16349  pwp1fsum  16352  divalglem0  16354  divalglem4  16357  divalglem8  16361  divalgb  16365  divalgmod  16367  modremain  16369  flodddiv4  16376  bitsp1  16392  bitsfzo  16396  bitsmod  16397  bitsinv1lem  16402  bitsf1  16407  sadaddlem  16427  bitsres  16434  bitsuz  16435  bitsshft  16436  smumullem  16453  modgcd  16493  gcdmultipled  16495  dvdsgcdidd  16498  bezoutlem1  16500  bezoutlem2  16501  bezoutlem3  16502  bezoutlem4  16503  dvdsmulgcd  16517  rplpwr  16519  lcmid  16570  absprodnn  16579  mulgcddvds  16616  divgcdcoprm0  16626  cncongr1  16628  cncongr2  16629  dvdszzq  16683  rpexp  16684  prmdvdsbc  16688  qmuldeneqnum  16709  numdensq  16716  qden1elz  16719  numdenexp  16722  hashdvds  16737  phiprm  16739  eulerthlem2  16744  fermltl  16746  prmdiv  16747  prmdiveq  16748  hashgcdlem  16750  odzdvds  16758  vfermltlALT  16765  modprm0  16768  modprmn0modprm0  16770  pythagtriplem6  16784  pythagtriplem7  16785  pythagtriplem15  16792  pcpremul  16806  pceulem  16808  pczpre  16810  pcdiv  16815  pcqmul  16816  pcqdiv  16820  pcexp  16822  pcaddlem  16851  pcadd  16852  fldivp1  16860  pcfac  16862  pcbc  16863  prmpwdvds  16867  prmreclem4  16882  4sqlem5  16905  4sqlem8  16908  4sqlem9  16909  4sqlem10  16910  4sqlem11  16918  4sqlem14  16921  4sqlem16  16923  4sqlem17  16924  vdwapun  16937  vdwnnlem2  16959  prmop1  17001  prmdvdsprmo  17005  prmgaplem7  17020  prmlem0  17068  chnlt  18581  mulgsubcl  19056  mulgdirlem  19073  mulgdir  19074  mulgass  19079  mulgmodid  19081  mulgsubdir  19082  psgnunilem5  19461  psgnunilem2  19462  psgnunilem4  19464  m1expaddsub  19465  psgnuni  19466  odnncl  19512  odmulg  19523  odbezout  19525  sylow1lem1  19565  sylow2alem2  19585  efgsres  19705  efgredleme  19710  efgredlemc  19712  odadd1  19815  odadd2  19816  cyggeninv  19850  gsummptshft  19903  ablfacrp  20035  pgpfac1lem3  20046  fincygsubgodd  20081  srgbinomlem3  20201  srgbinomlem4  20202  zringmulg  21432  zringlpirlem1  21438  zringlpirlem3  21440  prmirredlem  21448  fermltlchr  21505  zndvds0  21526  znf1o  21527  znunit  21539  cayhamlem1  22850  tgpmulg  24077  zdis  24801  uniioombllem3  25571  mbfi1fseqlem4  25704  dvexp3  25964  aareccl  26311  aalioulem1  26317  geolim3  26324  aaliou3lem2  26328  aaliou3lem6  26333  ulmshft  26374  sineq0  26507  efif1olem2  26526  igamz  27030  wilthlem1  27050  wilthlem2  27051  basellem3  27065  mumul  27163  musum  27173  musumsum  27174  muinv  27175  ppiub  27186  chtub  27194  logfac2  27199  chpchtsum  27201  dchrptlem1  27246  pcbcctr  27258  bcmono  27259  bposlem5  27270  bposlem6  27271  lgslem1  27279  lgsval2lem  27289  lgsval4a  27301  lgsneg  27303  lgsneg1  27304  lgsmod  27305  lgsdirprm  27313  lgsdir  27314  lgsdilem2  27315  lgsdi  27316  lgsne0  27317  lgsabs1  27318  lgssq  27319  lgssq2  27320  lgsmulsqcoprm  27325  lgsdirnn0  27326  lgsdinn0  27327  lgsqrlem1  27328  gausslemma2dlem1a  27347  gausslemma2dlem1  27348  gausslemma2dlem4  27351  gausslemma2dlem5a  27352  gausslemma2dlem5  27353  gausslemma2dlem6  27354  gausslemma2d  27356  lgseisenlem1  27357  lgseisenlem2  27358  lgseisenlem3  27359  lgseisenlem4  27360  lgsquadlem1  27362  lgsquad2lem1  27366  lgsquad3  27369  2lgslem1b  27374  2lgsoddprmlem2  27391  2sqlem3  27402  2sqlem4  27403  2sqlem8a  27407  2sqlem8  27408  2sqlem11  27411  2sqblem  27413  2sqn0  27416  2sqmod  27418  dchrisumlem1  27471  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  mudivsum  27512  mulogsum  27514  mulog2sumlem2  27517  selberglem1  27527  selberglem3  27529  selberg  27530  pntpbnd2  27569  pntlemf  27587  padicabvcxp  27614  axlowdimlem14  29043  axlowdimlem16  29045  pthdadjvtx  29815  crctcshwlkn0lem4  29900  crctcshwlkn0lem5  29901  crctcshlem4  29907  crctcsh  29911  clwwlkccatlem  30078  clwwisshclwws  30104  eucrctshift  30332  fzm1ne1  32881  fzspl  32882  bcm1n  32888  elq2  32905  znumd  32906  zdend  32907  numdenneg  32908  divnumden2  32909  ltesubnnd  32916  ccatf1  33029  swrdrn3  33035  swrdf1  33036  cshwrnid  33041  gsumzrsum  33147  gsummulsubdishift1  33150  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2  33215  archiabllem1  33275  archiabllem2c  33277  elrgspnlem1  33324  elrgspnlem2  33325  znfermltl  33450  zringidom  33643  zringfrac  33646  esplyindfv  33769  zconstr  33957  cos9thpiminplylem2  33976  zrhnm  34160  cnzh  34161  rezh  34162  zrhcntr  34172  qqhval2lem  34174  qqhghm  34181  qqhrhm  34182  qqhnm  34183  ballotlemfc0  34686  ballotlemfcc  34687  ballotlemic  34700  ballotlem1c  34701  ballotlemsgt1  34704  ballotlemsdom  34705  ballotlemsel1i  34706  ballotlemsf1o  34707  ballotlemsima  34709  ballotlemfrceq  34722  ballotlemfrcn0  34723  ballotlem1ri  34728  signsplypnf  34743  itgexpif  34799  fsum2dsub  34800  breprexplemc  34825  vtsprod  34832  circlemeth  34833  revpfxsfxrev  35353  swrdrevpfx  35354  revwlk  35362  swrdwlk  35364  divcnvlin  35970  fwddifnp1  36402  knoppndvlem2  36828  knoppndvlem7  36833  knoppndvlem14  36840  knoppndvlem16  36842  ltflcei  37984  poimirlem1  37997  poimirlem2  37998  poimirlem7  38003  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem24  38020  poimirlem31  38027  poimirlem32  38028  fdc  38121  mettrifi  38133  caushft  38137  cntotbnd  38172  fzsplitnd  42476  lcmineqlem6  42528  lcmineqlem18  42540  aks4d1p1p1  42557  aks4d1p8d3  42580  aks4d1p8  42581  primrootscoprmpow  42593  posbezout  42594  primrootscoprbij  42596  primrootspoweq0  42600  hashscontpow1  42615  aks6d1c3  42617  aks6d1c4  42618  aks6d1c5lem1  42630  aks6d1c5lem2  42632  sticksstones10  42649  sticksstones12a  42651  sticksstones12  42652  aks6d1c6lem3  42666  unitscyglem2  42690  unitscyglem4  42692  sumcubes  42799  oexpreposd  42808  exp11d  42812  dvdsexpb  42821  mzpsubmpt  43201  lzenom  43228  diophun  43231  eqrabdioph  43235  irrapxlem2  43277  irrapxlem3  43278  pellexlem6  43288  pell1234qrreccl  43308  pellfund14  43352  rmxyneg  43374  rmxyadd  43375  rmxp1  43386  rmxm1  43388  rmym1  43389  rmxluc  43390  rmyluc  43391  rmyluc2  43392  rmxdbl  43393  rmydbl  43394  congadd  43420  congsub  43424  congabseq  43428  acongrep  43434  acongeq  43437  jm2.18  43442  jm2.19lem1  43443  jm2.19lem2  43444  jm2.19lem3  43445  jm2.22  43449  jm2.23  43450  jm2.20nn  43451  jm2.25  43453  jm2.26lem3  43455  jm2.27c  43461  nzss  44770  hashnzfz  44773  hashnzfz2  44774  hashnzfzclim  44775  uzmptshftfval  44799  sineq0ALT  45389  fzisoeu  45756  fperiodmul  45760  monoord2xrv  45934  fmul01lt1lem2  46038  sumnnodd  46083  dvdsn1add  46390  dvnmul  46394  dvnprodlem1  46397  stoweidlem11  46462  stoweidlem26  46477  dirkertrigeqlem1  46549  dirkertrigeqlem2  46550  dirkertrigeqlem3  46551  dirkertrigeq  46552  dirkeritg  46553  fourierdlem26  46584  fourierdlem48  46605  fourierdlem49  46606  fourierdlem79  46636  fourierdlem91  46648  fourierdlem103  46660  fourierdlem104  46661  fouriersw  46682  etransclem1  46686  etransclem4  46689  etransclem8  46693  etransclem9  46694  etransclem15  46700  etransclem17  46702  etransclem18  46703  etransclem20  46705  etransclem21  46706  etransclem22  46707  etransclem23  46708  etransclem24  46709  etransclem25  46710  etransclem35  46720  etransclem38  46723  etransclem41  46726  etransclem44  46729  etransclem45  46730  etransclem46  46731  etransclem47  46732  etransclem48  46733  chnerlem2  47336  2elfz2melfz  47789  ceilbi  47808  flmrecm1  47814  fldivmod  47815  submodaddmod  47818  zplusmodne  47820  m1modne  47825  minusmod5ne  47826  submodlt  47827  minusmodnep2tmod  47830  m1modmmod  47835  modmkpkne  47838  modmknepk  47839  mod2addne  47841  modm2nep1  47843  modm1nep2  47845  modm1nem2  47846  2timesltsq  47849  fsumsplitsndif  47852  iccpartgtprec  47903  fargshiftf1  47924  fargshiftfo  47925  nprmmul3  48012  mod42tp1mod8  48088  sfprmdvdsmersenne  48089  lighneallem3  48093  lighneallem4b  48095  modexp2m1d  48098  nprmdvdsfacm1lem1  48106  ppivalnnprm  48111  dfodd6  48136  onego  48145  m1expoddALTV  48147  zofldiv2ALTV  48161  oddflALTV  48162  oexpnegALTV  48176  omoeALTV  48184  omeoALTV  48185  epoo  48202  emoo  48203  epee  48204  emee  48205  evensumeven  48206  evenltle  48216  even3prm2  48218  mogoldbblem  48219  fppr2odd  48230  fpprwppr  48238  fpprwpprb  48239  sbgoldbst  48277  sbgoldbaltlem2  48279  sgoldbeven3prm  48282  nnsum3primesprm  48289  nnsum4primesodd  48295  nnsum4primesoddALTV  48296  nnsum4primeseven  48299  nnsum4primesevenALTV  48300  bgoldbtbndlem2  48305  bgoldbtbndlem4  48307  bgoldbtbnd  48308  gpgedgvtx1  48561  gpgvtxedg0  48562  gpgvtxedg1  48563  gpg5nbgrvtx13starlem2  48571  gpg3nbgrvtx0  48575  pgnbgreunbgrlem2lem1  48613  pgnbgreunbgrlem2lem2  48614  pgnbgreunbgrlem2lem3  48615  2zrngamnd  48746  2zrngacmnd  48747  2zrngagrp  48748  2zrngALT  48753  2zrngnmlid  48754  2zrngnmlid2  48756  ztprmneprm  48846  altgsumbcALT  48852  zofldiv2  49030  fllogbd  49059  nnpw2blen  49079  blen1b  49087  blennngt2o2  49091  blennn0e2  49093  dig2nn1st  49104  dignn0flhalflem1  49114