Theorem zcnd 12611

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11038  ℤcz 12502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373  df-neg 11381  df-z 12503

This theorem is referenced by:  zsupss  12864  rpnnen1lem5  12908  fzm1  13537  fzrevral  13542  fzshftral  13545  nn0disj  13574  predfz  13583  fzoss2  13617  elfzo0suble  13636  fzo0addelr  13649  elfzoext  13652  fzosubel  13654  fzosubel3  13656  fzocatel  13659  fzosplitsnm1  13670  elfzom1elp1fzo1  13697  fzom1ne1  13715  2tnp1ge0ge0  13763  quoremz  13789  intfrac2  13792  intfracq  13793  flpmodeq  13808  moddiffl  13816  modmul1  13861  modmul12d  13862  modfzo0difsn  13880  modsumfzodifsn  13881  addmodlteq  13883  uzrdgxfr  13904  fzen2  13906  monoord2  13970  seqf1olem1  13978  seqf1olem2  13979  seqz  13987  expaddzlem  14042  znsqcld  14099  modexp  14175  sqoddm1div8  14180  bcm1k  14252  bcp1nk  14254  bcval5  14255  bcpasc  14258  hashfz  14364  hashfzo  14366  hashfzp1  14368  hashbclem  14389  seqcoll  14401  ccatval3  14516  ccatlid  14524  ccatass  14526  ccatalpha  14531  swrdfv0  14587  swrdfv2  14599  swrds1  14604  ccatswrd  14606  pfxfv  14620  ccatpfx  14638  swrdpfx  14644  pfxccatin12lem2  14668  spllen  14691  revccat  14703  revrev  14704  cshwidxmod  14740  cshwidxm1  14744  cshweqrep  14758  2cshwcshw  14762  cshimadifsn0  14767  swrds2m  14878  seqshft  15022  fzomaxdif  15281  climshft2  15519  iserex  15594  isercoll2  15606  serf0  15618  iseraltlem2  15620  iseraltlem3  15621  iseralt  15622  sumrblem  15648  fsumm1  15688  fsumsplitsnun  15692  fsump1  15693  fsumshftm  15718  fsumrev2  15719  telfsumo  15739  fsumparts  15743  binomlem  15766  isumshft  15776  isumsplit  15777  isum1p  15778  arisum  15797  pwdif  15805  cvgrat  15820  mertenslem1  15821  ntrivcvg  15834  ntrivcvgtail  15837  prodrblem  15866  fprodser  15886  fprodm1  15904  fprodp1  15906  fprodrev  15914  fprodmodd  15934  fallfacval3  15949  fallfacfwd  15973  0fallfac  15974  binomfallfaclem2  15977  fallfacval4  15980  fsumkthpow  15993  eirrlem  16143  sqrt2irrlem  16187  addmulmodb  16206  dvds2ln  16230  dvdsadd2b  16247  fsumdvds  16249  fzocongeq  16265  addmodlteqALT  16266  dvdsexp  16269  dvdsmod  16270  3dvds  16272  fprodfvdvdsd  16275  odd2np1  16282  oddm1even  16284  oexpneg  16286  mod2eq1n2dvds  16288  mulsucdiv2z  16294  zob  16300  ltoddhalfle  16302  sumodd  16329  pwp1fsum  16332  divalglem0  16334  divalglem4  16337  divalglem8  16341  divalgb  16345  divalgmod  16347  modremain  16349  flodddiv4  16356  bitsp1  16372  bitsfzo  16376  bitsmod  16377  bitsinv1lem  16382  bitsf1  16387  sadaddlem  16407  bitsres  16414  bitsuz  16415  bitsshft  16416  smumullem  16433  modgcd  16473  gcdmultipled  16475  dvdsgcdidd  16478  bezoutlem1  16480  bezoutlem2  16481  bezoutlem3  16482  bezoutlem4  16483  dvdsmulgcd  16497  rplpwr  16499  lcmid  16550  absprodnn  16559  mulgcddvds  16596  divgcdcoprm0  16606  cncongr1  16608  cncongr2  16609  dvdszzq  16662  rpexp  16663  prmdvdsbc  16667  qmuldeneqnum  16688  numdensq  16695  qden1elz  16698  numdenexp  16701  hashdvds  16716  phiprm  16718  eulerthlem2  16723  fermltl  16725  prmdiv  16726  prmdiveq  16727  hashgcdlem  16729  odzdvds  16737  vfermltlALT  16744  modprm0  16747  modprmn0modprm0  16749  pythagtriplem6  16763  pythagtriplem7  16764  pythagtriplem15  16771  pcpremul  16785  pceulem  16787  pczpre  16789  pcdiv  16794  pcqmul  16795  pcqdiv  16799  pcexp  16801  pcaddlem  16830  pcadd  16831  fldivp1  16839  pcfac  16841  pcbc  16842  prmpwdvds  16846  prmreclem4  16861  4sqlem5  16884  4sqlem8  16887  4sqlem9  16888  4sqlem10  16889  4sqlem11  16897  4sqlem14  16900  4sqlem16  16902  4sqlem17  16903  vdwapun  16916  vdwnnlem2  16938  prmop1  16980  prmdvdsprmo  16984  prmgaplem7  16999  prmlem0  17047  chnlt  18560  mulgsubcl  19035  mulgdirlem  19052  mulgdir  19053  mulgass  19058  mulgmodid  19060  mulgsubdir  19061  psgnunilem5  19440  psgnunilem2  19441  psgnunilem4  19443  m1expaddsub  19444  psgnuni  19445  odnncl  19491  odmulg  19502  odbezout  19504  sylow1lem1  19544  sylow2alem2  19564  efgsres  19684  efgredleme  19689  efgredlemc  19691  odadd1  19794  odadd2  19795  cyggeninv  19829  gsummptshft  19882  ablfacrp  20014  pgpfac1lem3  20025  fincygsubgodd  20060  srgbinomlem3  20180  srgbinomlem4  20181  zringmulg  21428  zringlpirlem1  21434  zringlpirlem3  21436  prmirredlem  21444  fermltlchr  21501  zndvds0  21522  znf1o  21523  znunit  21535  cayhamlem1  22827  tgpmulg  24054  zdis  24778  uniioombllem3  25559  mbfi1fseqlem4  25692  dvexp3  25955  aareccl  26307  aalioulem1  26313  geolim3  26320  aaliou3lem2  26324  aaliou3lem6  26329  ulmshft  26372  sineq0  26506  efif1olem2  26525  igamz  27031  wilthlem1  27051  wilthlem2  27052  basellem3  27066  mumul  27164  musum  27174  musumsum  27175  muinv  27176  ppiub  27188  chtub  27196  logfac2  27201  chpchtsum  27203  dchrptlem1  27248  pcbcctr  27260  bcmono  27261  bposlem5  27272  bposlem6  27273  lgslem1  27281  lgsval2lem  27291  lgsval4a  27303  lgsneg  27305  lgsneg1  27306  lgsmod  27307  lgsdirprm  27315  lgsdir  27316  lgsdilem2  27317  lgsdi  27318  lgsne0  27319  lgsabs1  27320  lgssq  27321  lgssq2  27322  lgsmulsqcoprm  27327  lgsdirnn0  27328  lgsdinn0  27329  lgsqrlem1  27330  gausslemma2dlem1a  27349  gausslemma2dlem1  27350  gausslemma2dlem4  27353  gausslemma2dlem5a  27354  gausslemma2dlem5  27355  gausslemma2dlem6  27356  gausslemma2d  27358  lgseisenlem1  27359  lgseisenlem2  27360  lgseisenlem3  27361  lgseisenlem4  27362  lgsquadlem1  27364  lgsquad2lem1  27368  lgsquad3  27371  2lgslem1b  27376  2lgsoddprmlem2  27393  2sqlem3  27404  2sqlem4  27405  2sqlem8a  27409  2sqlem8  27410  2sqlem11  27413  2sqblem  27415  2sqn0  27418  2sqmod  27420  dchrisumlem1  27473  dchrmusum2  27478  dchrvmasumlem1  27479  dchrvmasum2lem  27480  mudivsum  27514  mulogsum  27516  mulog2sumlem2  27519  selberglem1  27529  selberglem3  27531  selberg  27532  pntpbnd2  27571  pntlemf  27589  padicabvcxp  27616  axlowdimlem14  29046  axlowdimlem16  29048  pthdadjvtx  29819  crctcshwlkn0lem4  29904  crctcshwlkn0lem5  29905  crctcshlem4  29911  crctcsh  29915  clwwlkccatlem  30082  clwwisshclwws  30108  eucrctshift  30336  fzm1ne1  32885  fzspl  32886  bcm1n  32892  elq2  32909  znumd  32910  zdend  32911  numdenneg  32912  divnumden2  32913  ltesubnnd  32920  ccatf1  33048  swrdrn3  33054  swrdf1  33055  cshwrnid  33060  gsumzrsum  33165  gsummulsubdishift1  33168  cycpmco2lem3  33228  cycpmco2lem4  33229  cycpmco2lem5  33230  cycpmco2lem6  33231  cycpmco2  33233  archiabllem1  33293  archiabllem2c  33295  elrgspnlem1  33342  elrgspnlem2  33343  znfermltl  33465  zringidom  33650  zringfrac  33653  esplyindfv  33759  zconstr  33948  cos9thpiminplylem2  33967  zrhnm  34151  cnzh  34152  rezh  34153  zrhcntr  34163  qqhval2lem  34165  qqhghm  34172  qqhrhm  34173  qqhnm  34174  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemic  34691  ballotlem1c  34692  ballotlemsgt1  34695  ballotlemsdom  34696  ballotlemsel1i  34697  ballotlemsf1o  34698  ballotlemsima  34700  ballotlemfrceq  34713  ballotlemfrcn0  34714  ballotlem1ri  34719  signsplypnf  34734  itgexpif  34790  fsum2dsub  34791  breprexplemc  34816  vtsprod  34823  circlemeth  34824  revpfxsfxrev  35338  swrdrevpfx  35339  revwlk  35347  swrdwlk  35349  divcnvlin  35955  fwddifnp1  36387  knoppndvlem2  36741  knoppndvlem7  36746  knoppndvlem14  36753  knoppndvlem16  36755  ltflcei  37888  poimirlem1  37901  poimirlem2  37902  poimirlem7  37907  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem24  37924  poimirlem31  37931  poimirlem32  37932  fdc  38025  mettrifi  38037  caushft  38041  cntotbnd  38076  fzsplitnd  42381  lcmineqlem6  42433  lcmineqlem18  42445  aks4d1p1p1  42462  aks4d1p8d3  42485  aks4d1p8  42486  primrootscoprmpow  42498  posbezout  42499  primrootscoprbij  42501  primrootspoweq0  42505  hashscontpow1  42520  aks6d1c3  42522  aks6d1c4  42523  aks6d1c5lem1  42535  aks6d1c5lem2  42537  sticksstones10  42554  sticksstones12a  42556  sticksstones12  42557  aks6d1c6lem3  42571  unitscyglem2  42595  unitscyglem4  42597  sumcubes  42712  oexpreposd  42721  exp11d  42725  dvdsexpb  42734  mzpsubmpt  43129  lzenom  43156  diophun  43159  eqrabdioph  43163  irrapxlem2  43209  irrapxlem3  43210  pellexlem6  43220  pell1234qrreccl  43240  pellfund14  43284  rmxyneg  43306  rmxyadd  43307  rmxp1  43318  rmxm1  43320  rmym1  43321  rmxluc  43322  rmyluc  43323  rmyluc2  43324  rmxdbl  43325  rmydbl  43326  congadd  43352  congsub  43356  congabseq  43360  acongrep  43366  acongeq  43369  jm2.18  43374  jm2.19lem1  43375  jm2.19lem2  43376  jm2.19lem3  43377  jm2.22  43381  jm2.23  43382  jm2.20nn  43383  jm2.25  43385  jm2.26lem3  43387  jm2.27c  43393  nzss  44702  hashnzfz  44705  hashnzfz2  44706  hashnzfzclim  44707  uzmptshftfval  44731  sineq0ALT  45321  fzisoeu  45691  fperiodmul  45695  monoord2xrv  45870  fmul01lt1lem2  45974  sumnnodd  46019  dvdsn1add  46326  dvnmul  46330  dvnprodlem1  46333  stoweidlem11  46398  stoweidlem26  46413  dirkertrigeqlem1  46485  dirkertrigeqlem2  46486  dirkertrigeqlem3  46487  dirkertrigeq  46488  dirkeritg  46489  fourierdlem26  46520  fourierdlem48  46541  fourierdlem49  46542  fourierdlem79  46572  fourierdlem91  46584  fourierdlem103  46596  fourierdlem104  46597  fouriersw  46618  etransclem1  46622  etransclem4  46625  etransclem8  46629  etransclem9  46630  etransclem15  46636  etransclem17  46638  etransclem18  46639  etransclem20  46641  etransclem21  46642  etransclem22  46643  etransclem23  46644  etransclem24  46645  etransclem25  46646  etransclem35  46656  etransclem38  46659  etransclem41  46662  etransclem44  46665  etransclem45  46666  etransclem46  46667  etransclem47  46668  etransclem48  46669  chnerlem2  47270  2elfz2melfz  47707  ceilbi  47722  fldivmod  47727  submodaddmod  47730  zplusmodne  47732  m1modne  47737  minusmod5ne  47738  submodlt  47739  minusmodnep2tmod  47742  m1modmmod  47747  modmkpkne  47750  modmknepk  47751  mod2addne  47753  modm2nep1  47755  modm1nep2  47757  modm1nem2  47758  fsumsplitsndif  47762  iccpartgtprec  47809  fargshiftf1  47830  fargshiftfo  47831  mod42tp1mod8  47991  sfprmdvdsmersenne  47992  lighneallem3  47996  lighneallem4b  47998  modexp2m1d  48001  dfodd6  48026  onego  48035  m1expoddALTV  48037  zofldiv2ALTV  48051  oddflALTV  48052  oexpnegALTV  48066  omoeALTV  48074  omeoALTV  48075  epoo  48092  emoo  48093  epee  48094  emee  48095  evensumeven  48096  evenltle  48106  even3prm2  48108  mogoldbblem  48109  fppr2odd  48120  fpprwppr  48128  fpprwpprb  48129  sbgoldbst  48167  sbgoldbaltlem2  48169  sgoldbeven3prm  48172  nnsum3primesprm  48179  nnsum4primesodd  48185  nnsum4primesoddALTV  48186  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  bgoldbtbndlem2  48195  bgoldbtbndlem4  48197  bgoldbtbnd  48198  gpgedgvtx1  48451  gpgvtxedg0  48452  gpgvtxedg1  48453  gpg5nbgrvtx13starlem2  48461  gpg3nbgrvtx0  48465  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem2lem3  48505  2zrngamnd  48636  2zrngacmnd  48637  2zrngagrp  48638  2zrngALT  48643  2zrngnmlid  48644  2zrngnmlid2  48646  ztprmneprm  48736  altgsumbcALT  48742  zofldiv2  48920  fllogbd  48949  nnpw2blen  48969  blen1b  48977  blennngt2o2  48981  blennn0e2  48983  dig2nn1st  48994  dignn0flhalflem1  49004