Theorem zcnd 12615

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  ℤcz 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  zsupss  12872  rpnnen1lem5  12916  fzm1  13544  fzrevral  13549  fzshftral  13552  nn0disj  13581  predfz  13590  fzoss2  13624  elfzo0suble  13643  fzo0addelr  13656  elfzoext  13659  fzosubel  13661  fzosubel3  13663  fzocatel  13666  fzosplitsnm1  13677  elfzom1elp1fzo1  13704  2tnp1ge0ge0  13767  quoremz  13793  intfrac2  13796  intfracq  13797  flpmodeq  13812  moddiffl  13820  modmul1  13865  modmul12d  13866  modfzo0difsn  13884  modsumfzodifsn  13885  addmodlteq  13887  uzrdgxfr  13908  fzen2  13910  monoord2  13974  seqf1olem1  13982  seqf1olem2  13983  seqz  13991  expaddzlem  14046  znsqcld  14103  modexp  14179  sqoddm1div8  14184  bcm1k  14256  bcp1nk  14258  bcval5  14259  bcpasc  14262  hashfz  14368  hashfzo  14370  hashfzp1  14372  hashbclem  14393  seqcoll  14405  ccatval3  14520  ccatlid  14527  ccatass  14529  ccatalpha  14534  swrdfv0  14590  swrdfv2  14602  swrds1  14607  ccatswrd  14609  pfxfv  14623  ccatpfx  14642  swrdpfx  14648  pfxccatin12lem2  14672  spllen  14695  revccat  14707  revrev  14708  cshwidxmod  14744  cshwidxm1  14748  cshweqrep  14762  2cshwcshw  14767  cshimadifsn0  14772  swrds2m  14883  seqshft  15027  fzomaxdif  15286  climshft2  15524  iserex  15599  isercoll2  15611  serf0  15623  iseraltlem2  15625  iseraltlem3  15626  iseralt  15627  sumrblem  15653  fsumm1  15693  fsumsplitsnun  15697  fsump1  15698  fsumshftm  15723  fsumrev2  15724  telfsumo  15744  fsumparts  15748  binomlem  15771  isumshft  15781  isumsplit  15782  isum1p  15783  arisum  15802  pwdif  15810  cvgrat  15825  mertenslem1  15826  ntrivcvg  15839  ntrivcvgtail  15842  prodrblem  15871  fprodser  15891  fprodm1  15909  fprodp1  15911  fprodrev  15919  fprodmodd  15939  fallfacval3  15954  fallfacfwd  15978  0fallfac  15979  binomfallfaclem2  15982  fallfacval4  15985  fsumkthpow  15998  eirrlem  16148  sqrt2irrlem  16192  addmulmodb  16211  dvds2ln  16235  dvdsadd2b  16252  fsumdvds  16254  fzocongeq  16270  addmodlteqALT  16271  dvdsexp  16274  dvdsmod  16275  3dvds  16277  fprodfvdvdsd  16280  odd2np1  16287  oddm1even  16289  oexpneg  16291  mod2eq1n2dvds  16293  mulsucdiv2z  16299  zob  16305  ltoddhalfle  16307  sumodd  16334  pwp1fsum  16337  divalglem0  16339  divalglem4  16342  divalglem8  16346  divalgb  16350  divalgmod  16352  modremain  16354  flodddiv4  16361  bitsp1  16377  bitsfzo  16381  bitsmod  16382  bitsinv1lem  16387  bitsf1  16392  sadaddlem  16412  bitsres  16419  bitsuz  16420  bitsshft  16421  smumullem  16438  modgcd  16478  gcdmultipled  16480  dvdsgcdidd  16483  bezoutlem1  16485  bezoutlem2  16486  bezoutlem3  16487  bezoutlem4  16488  dvdsmulgcd  16502  rplpwr  16504  lcmid  16555  absprodnn  16564  mulgcddvds  16601  divgcdcoprm0  16611  cncongr1  16613  cncongr2  16614  dvdszzq  16667  rpexp  16668  prmdvdsbc  16672  qmuldeneqnum  16693  numdensq  16700  qden1elz  16703  numdenexp  16706  hashdvds  16721  phiprm  16723  eulerthlem2  16728  fermltl  16730  prmdiv  16731  prmdiveq  16732  hashgcdlem  16734  odzdvds  16742  vfermltlALT  16749  modprm0  16752  modprmn0modprm0  16754  pythagtriplem6  16768  pythagtriplem7  16769  pythagtriplem15  16776  pcpremul  16790  pceulem  16792  pczpre  16794  pcdiv  16799  pcqmul  16800  pcqdiv  16804  pcexp  16806  pcaddlem  16835  pcadd  16836  fldivp1  16844  pcfac  16846  pcbc  16847  prmpwdvds  16851  prmreclem4  16866  4sqlem5  16889  4sqlem8  16892  4sqlem9  16893  4sqlem10  16894  4sqlem11  16902  4sqlem14  16905  4sqlem16  16907  4sqlem17  16908  vdwapun  16921  vdwnnlem2  16943  prmop1  16985  prmdvdsprmo  16989  prmgaplem7  17004  prmlem0  17052  mulgsubcl  19002  mulgdirlem  19019  mulgdir  19020  mulgass  19025  mulgmodid  19027  mulgsubdir  19028  psgnunilem5  19408  psgnunilem2  19409  psgnunilem4  19411  m1expaddsub  19412  psgnuni  19413  odnncl  19459  odmulg  19470  odbezout  19472  sylow1lem1  19512  sylow2alem2  19532  efgsres  19652  efgredleme  19657  efgredlemc  19659  odadd1  19762  odadd2  19763  cyggeninv  19797  gsummptshft  19850  ablfacrp  19982  pgpfac1lem3  19993  fincygsubgodd  20028  srgbinomlem3  20148  srgbinomlem4  20149  zringmulg  21398  zringlpirlem1  21404  zringlpirlem3  21406  prmirredlem  21414  fermltlchr  21471  zndvds0  21492  znf1o  21493  znunit  21505  cayhamlem1  22786  tgpmulg  24013  zdis  24738  uniioombllem3  25519  mbfi1fseqlem4  25652  dvexp3  25915  aareccl  26267  aalioulem1  26273  geolim3  26280  aaliou3lem2  26284  aaliou3lem6  26289  ulmshft  26332  sineq0  26466  efif1olem2  26485  igamz  26991  wilthlem1  27011  wilthlem2  27012  basellem3  27026  mumul  27124  musum  27134  musumsum  27135  muinv  27136  ppiub  27148  chtub  27156  logfac2  27161  chpchtsum  27163  dchrptlem1  27208  pcbcctr  27220  bcmono  27221  bposlem5  27232  bposlem6  27233  lgslem1  27241  lgsval2lem  27251  lgsval4a  27263  lgsneg  27265  lgsneg1  27266  lgsmod  27267  lgsdirprm  27275  lgsdir  27276  lgsdilem2  27277  lgsdi  27278  lgsne0  27279  lgsabs1  27280  lgssq  27281  lgssq2  27282  lgsmulsqcoprm  27287  lgsdirnn0  27288  lgsdinn0  27289  lgsqrlem1  27290  gausslemma2dlem1a  27309  gausslemma2dlem1  27310  gausslemma2dlem4  27313  gausslemma2dlem5a  27314  gausslemma2dlem5  27315  gausslemma2dlem6  27316  gausslemma2d  27318  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgsquadlem1  27324  lgsquad2lem1  27328  lgsquad3  27331  2lgslem1b  27336  2lgsoddprmlem2  27353  2sqlem3  27364  2sqlem4  27365  2sqlem8a  27369  2sqlem8  27370  2sqlem11  27373  2sqblem  27375  2sqn0  27378  2sqmod  27380  dchrisumlem1  27433  dchrmusum2  27438  dchrvmasumlem1  27439  dchrvmasum2lem  27440  mudivsum  27474  mulogsum  27476  mulog2sumlem2  27479  selberglem1  27489  selberglem3  27491  selberg  27492  pntpbnd2  27531  pntlemf  27549  padicabvcxp  27576  axlowdimlem14  28935  axlowdimlem16  28937  pthdadjvtx  29708  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshlem4  29800  crctcsh  29804  clwwlkccatlem  29968  clwwisshclwws  29994  eucrctshift  30222  fzm1ne1  32761  fzspl  32762  bcm1n  32768  fzom1ne1  32774  elq2  32786  znumd  32787  zdend  32788  numdenneg  32789  divnumden2  32790  ltesubnnd  32797  ccatf1  32920  swrdrn3  32927  swrdf1  32928  cshwrnid  32933  chnlt  32985  gsumzrsum  33042  cycpmco2lem3  33100  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2  33105  archiabllem1  33162  archiabllem2c  33164  elrgspnlem1  33209  elrgspnlem2  33210  znfermltl  33330  zringidom  33515  zringfrac  33518  zconstr  33747  cos9thpiminplylem2  33766  zrhnm  33950  cnzh  33951  rezh  33952  zrhcntr  33962  qqhval2lem  33964  qqhghm  33971  qqhrhm  33972  qqhnm  33973  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemic  34491  ballotlem1c  34492  ballotlemsgt1  34495  ballotlemsdom  34496  ballotlemsel1i  34497  ballotlemsf1o  34498  ballotlemsima  34500  ballotlemfrceq  34513  ballotlemfrcn0  34514  ballotlem1ri  34519  signsplypnf  34534  itgexpif  34590  fsum2dsub  34591  breprexplemc  34616  vtsprod  34623  circlemeth  34624  revpfxsfxrev  35096  swrdrevpfx  35097  revwlk  35105  swrdwlk  35107  divcnvlin  35713  fwddifnp1  36146  knoppndvlem2  36494  knoppndvlem7  36499  knoppndvlem14  36506  knoppndvlem16  36508  ltflcei  37595  poimirlem1  37608  poimirlem2  37609  poimirlem7  37614  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem24  37631  poimirlem31  37638  poimirlem32  37639  fdc  37732  mettrifi  37744  caushft  37748  cntotbnd  37783  fzsplitnd  41963  lcmineqlem6  42015  lcmineqlem18  42027  aks4d1p1p1  42044  aks4d1p8d3  42067  aks4d1p8  42068  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  hashscontpow1  42102  aks6d1c3  42104  aks6d1c4  42105  aks6d1c5lem1  42117  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  unitscyglem2  42177  unitscyglem4  42179  sumcubes  42294  oexpreposd  42303  exp11d  42307  dvdsexpb  42316  mzpsubmpt  42724  lzenom  42751  diophun  42754  eqrabdioph  42758  irrapxlem2  42804  irrapxlem3  42805  pellexlem6  42815  pell1234qrreccl  42835  pellfund14  42879  rmxyneg  42902  rmxyadd  42903  rmxp1  42914  rmxm1  42916  rmym1  42917  rmxluc  42918  rmyluc  42919  rmyluc2  42920  rmxdbl  42921  rmydbl  42922  congadd  42948  congsub  42952  congabseq  42956  acongrep  42962  acongeq  42965  jm2.18  42970  jm2.19lem1  42971  jm2.19lem2  42972  jm2.19lem3  42973  jm2.22  42977  jm2.23  42978  jm2.20nn  42979  jm2.25  42981  jm2.26lem3  42983  jm2.27c  42989  nzss  44299  hashnzfz  44302  hashnzfz2  44303  hashnzfzclim  44304  uzmptshftfval  44328  sineq0ALT  44919  fzisoeu  45291  fperiodmul  45295  monoord2xrv  45472  fmul01lt1lem2  45576  sumnnodd  45621  dvdsn1add  45930  dvnmul  45934  dvnprodlem1  45937  stoweidlem11  46002  stoweidlem26  46017  dirkertrigeqlem1  46089  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkeritg  46093  fourierdlem26  46124  fourierdlem48  46145  fourierdlem49  46146  fourierdlem79  46176  fourierdlem91  46188  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem1  46226  etransclem4  46229  etransclem8  46233  etransclem9  46234  etransclem15  46240  etransclem17  46242  etransclem18  46243  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem23  46248  etransclem24  46249  etransclem25  46250  etransclem35  46260  etransclem38  46263  etransclem41  46266  etransclem44  46269  etransclem45  46270  etransclem46  46271  etransclem47  46272  etransclem48  46273  2elfz2melfz  47312  ceilbi  47327  fldivmod  47332  submodaddmod  47335  zplusmodne  47337  m1modne  47342  minusmod5ne  47343  submodlt  47344  minusmodnep2tmod  47347  m1modmmod  47352  modmkpkne  47355  modmknepk  47356  mod2addne  47358  modm2nep1  47360  modm1nep2  47362  modm1nem2  47363  fsumsplitsndif  47367  iccpartgtprec  47414  fargshiftf1  47435  fargshiftfo  47436  mod42tp1mod8  47596  sfprmdvdsmersenne  47597  lighneallem3  47601  lighneallem4b  47603  modexp2m1d  47606  dfodd6  47631  onego  47640  m1expoddALTV  47642  zofldiv2ALTV  47656  oddflALTV  47657  oexpnegALTV  47671  omoeALTV  47679  omeoALTV  47680  epoo  47697  emoo  47698  epee  47699  emee  47700  evensumeven  47701  evenltle  47711  even3prm2  47713  mogoldbblem  47714  fppr2odd  47725  fpprwppr  47733  fpprwpprb  47734  sbgoldbst  47772  sbgoldbaltlem2  47774  sgoldbeven3prm  47777  nnsum3primesprm  47784  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  bgoldbtbndlem2  47800  bgoldbtbndlem4  47802  bgoldbtbnd  47803  gpgedgvtx1  48046  gpgvtxedg0  48047  gpgvtxedg1  48048  gpg5nbgrvtx13starlem2  48056  gpg3nbgrvtx0  48060  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  2zrngamnd  48228  2zrngacmnd  48229  2zrngagrp  48230  2zrngALT  48235  2zrngnmlid  48236  2zrngnmlid2  48238  ztprmneprm  48328  altgsumbcALT  48334  zofldiv2  48513  fllogbd  48542  nnpw2blen  48562  blen1b  48570  blennngt2o2  48574  blennn0e2  48576  dig2nn1st  48587  dignn0flhalflem1  48597