Theorem zcnd 12646

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℤcz 12536

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 2702  ax-resscn 11132

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537

This theorem is referenced by:  zsupss  12903  rpnnen1lem5  12947  fzm1  13575  fzrevral  13580  fzshftral  13583  nn0disj  13612  predfz  13621  fzoss2  13655  elfzo0suble  13674  fzo0addelr  13687  elfzoext  13690  fzosubel  13692  fzosubel3  13694  fzocatel  13697  fzosplitsnm1  13708  elfzom1elp1fzo1  13735  2tnp1ge0ge0  13798  quoremz  13824  intfrac2  13827  intfracq  13828  flpmodeq  13843  moddiffl  13851  modmul1  13896  modmul12d  13897  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  uzrdgxfr  13939  fzen2  13941  monoord2  14005  seqf1olem1  14013  seqf1olem2  14014  seqz  14022  expaddzlem  14077  znsqcld  14134  modexp  14210  sqoddm1div8  14215  bcm1k  14287  bcp1nk  14289  bcval5  14290  bcpasc  14293  hashfz  14399  hashfzo  14401  hashfzp1  14403  hashbclem  14424  seqcoll  14436  ccatval3  14551  ccatlid  14558  ccatass  14560  ccatalpha  14565  swrdfv0  14621  swrdfv2  14633  swrds1  14638  ccatswrd  14640  pfxfv  14654  ccatpfx  14673  swrdpfx  14679  pfxccatin12lem2  14703  spllen  14726  revccat  14738  revrev  14739  cshwidxmod  14775  cshwidxm1  14779  cshweqrep  14793  2cshwcshw  14798  cshimadifsn0  14803  swrds2m  14914  seqshft  15058  fzomaxdif  15317  climshft2  15555  iserex  15630  isercoll2  15642  serf0  15654  iseraltlem2  15656  iseraltlem3  15657  iseralt  15658  sumrblem  15684  fsumm1  15724  fsumsplitsnun  15728  fsump1  15729  fsumshftm  15754  fsumrev2  15755  telfsumo  15775  fsumparts  15779  binomlem  15802  isumshft  15812  isumsplit  15813  isum1p  15814  arisum  15833  pwdif  15841  cvgrat  15856  mertenslem1  15857  ntrivcvg  15870  ntrivcvgtail  15873  prodrblem  15902  fprodser  15922  fprodm1  15940  fprodp1  15942  fprodrev  15950  fprodmodd  15970  fallfacval3  15985  fallfacfwd  16009  0fallfac  16010  binomfallfaclem2  16013  fallfacval4  16016  fsumkthpow  16029  eirrlem  16179  sqrt2irrlem  16223  addmulmodb  16242  dvds2ln  16266  dvdsadd2b  16283  fsumdvds  16285  fzocongeq  16301  addmodlteqALT  16302  dvdsexp  16305  dvdsmod  16306  3dvds  16308  fprodfvdvdsd  16311  odd2np1  16318  oddm1even  16320  oexpneg  16322  mod2eq1n2dvds  16324  mulsucdiv2z  16330  zob  16336  ltoddhalfle  16338  sumodd  16365  pwp1fsum  16368  divalglem0  16370  divalglem4  16373  divalglem8  16377  divalgb  16381  divalgmod  16383  modremain  16385  flodddiv4  16392  bitsp1  16408  bitsfzo  16412  bitsmod  16413  bitsinv1lem  16418  bitsf1  16423  sadaddlem  16443  bitsres  16450  bitsuz  16451  bitsshft  16452  smumullem  16469  modgcd  16509  gcdmultipled  16511  dvdsgcdidd  16514  bezoutlem1  16516  bezoutlem2  16517  bezoutlem3  16518  bezoutlem4  16519  dvdsmulgcd  16533  rplpwr  16535  lcmid  16586  absprodnn  16595  mulgcddvds  16632  divgcdcoprm0  16642  cncongr1  16644  cncongr2  16645  dvdszzq  16698  rpexp  16699  prmdvdsbc  16703  qmuldeneqnum  16724  numdensq  16731  qden1elz  16734  numdenexp  16737  hashdvds  16752  phiprm  16754  eulerthlem2  16759  fermltl  16761  prmdiv  16762  prmdiveq  16763  hashgcdlem  16765  odzdvds  16773  vfermltlALT  16780  modprm0  16783  modprmn0modprm0  16785  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem15  16807  pcpremul  16821  pceulem  16823  pczpre  16825  pcdiv  16830  pcqmul  16831  pcqdiv  16835  pcexp  16837  pcaddlem  16866  pcadd  16867  fldivp1  16875  pcfac  16877  pcbc  16878  prmpwdvds  16882  prmreclem4  16897  4sqlem5  16920  4sqlem8  16923  4sqlem9  16924  4sqlem10  16925  4sqlem11  16933  4sqlem14  16936  4sqlem16  16938  4sqlem17  16939  vdwapun  16952  vdwnnlem2  16974  prmop1  17016  prmdvdsprmo  17020  prmgaplem7  17035  prmlem0  17083  mulgsubcl  19027  mulgdirlem  19044  mulgdir  19045  mulgass  19050  mulgmodid  19052  mulgsubdir  19053  psgnunilem5  19431  psgnunilem2  19432  psgnunilem4  19434  m1expaddsub  19435  psgnuni  19436  odnncl  19482  odmulg  19493  odbezout  19495  sylow1lem1  19535  sylow2alem2  19555  efgsres  19675  efgredleme  19680  efgredlemc  19682  odadd1  19785  odadd2  19786  cyggeninv  19820  gsummptshft  19873  ablfacrp  20005  pgpfac1lem3  20016  fincygsubgodd  20051  srgbinomlem3  20144  srgbinomlem4  20145  zringmulg  21373  zringlpirlem1  21379  zringlpirlem3  21381  prmirredlem  21389  fermltlchr  21446  zndvds0  21467  znf1o  21468  znunit  21480  cayhamlem1  22760  tgpmulg  23987  zdis  24712  uniioombllem3  25493  mbfi1fseqlem4  25626  dvexp3  25889  aareccl  26241  aalioulem1  26247  geolim3  26254  aaliou3lem2  26258  aaliou3lem6  26263  ulmshft  26306  sineq0  26440  efif1olem2  26459  igamz  26965  wilthlem1  26985  wilthlem2  26986  basellem3  27000  mumul  27098  musum  27108  musumsum  27109  muinv  27110  ppiub  27122  chtub  27130  logfac2  27135  chpchtsum  27137  dchrptlem1  27182  pcbcctr  27194  bcmono  27195  bposlem5  27206  bposlem6  27207  lgslem1  27215  lgsval2lem  27225  lgsval4a  27237  lgsneg  27239  lgsneg1  27240  lgsmod  27241  lgsdirprm  27249  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  lgsabs1  27254  lgssq  27255  lgssq2  27256  lgsmulsqcoprm  27261  lgsdirnn0  27262  lgsdinn0  27263  lgsqrlem1  27264  gausslemma2dlem1a  27283  gausslemma2dlem1  27284  gausslemma2dlem4  27287  gausslemma2dlem5a  27288  gausslemma2dlem5  27289  gausslemma2dlem6  27290  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquad2lem1  27302  lgsquad3  27305  2lgslem1b  27310  2lgsoddprmlem2  27327  2sqlem3  27338  2sqlem4  27339  2sqlem8a  27343  2sqlem8  27344  2sqlem11  27347  2sqblem  27349  2sqn0  27352  2sqmod  27354  dchrisumlem1  27407  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  mudivsum  27448  mulogsum  27450  mulog2sumlem2  27453  selberglem1  27463  selberglem3  27465  selberg  27466  pntpbnd2  27505  pntlemf  27523  padicabvcxp  27550  axlowdimlem14  28889  axlowdimlem16  28891  pthdadjvtx  29665  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshlem4  29757  crctcsh  29761  clwwlkccatlem  29925  clwwisshclwws  29951  eucrctshift  30179  fzm1ne1  32718  fzspl  32719  bcm1n  32725  fzom1ne1  32731  elq2  32743  znumd  32744  zdend  32745  numdenneg  32746  divnumden2  32747  ltesubnnd  32754  ccatf1  32877  swrdrn3  32884  swrdf1  32885  cshwrnid  32890  chnlt  32946  gsumzrsum  33006  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  archiabllem1  33154  archiabllem2c  33156  elrgspnlem1  33200  elrgspnlem2  33201  znfermltl  33344  zringidom  33529  zringfrac  33532  zconstr  33761  cos9thpiminplylem2  33780  zrhnm  33964  cnzh  33965  rezh  33966  zrhcntr  33976  qqhval2lem  33978  qqhghm  33985  qqhrhm  33986  qqhnm  33987  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemic  34505  ballotlem1c  34506  ballotlemsgt1  34509  ballotlemsdom  34510  ballotlemsel1i  34511  ballotlemsf1o  34512  ballotlemsima  34514  ballotlemfrceq  34527  ballotlemfrcn0  34528  ballotlem1ri  34533  signsplypnf  34548  itgexpif  34604  fsum2dsub  34605  breprexplemc  34630  vtsprod  34637  circlemeth  34638  revpfxsfxrev  35110  swrdrevpfx  35111  revwlk  35119  swrdwlk  35121  divcnvlin  35727  fwddifnp1  36160  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem14  36520  knoppndvlem16  36522  ltflcei  37609  poimirlem1  37622  poimirlem2  37623  poimirlem7  37628  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem24  37645  poimirlem31  37652  poimirlem32  37653  fdc  37746  mettrifi  37758  caushft  37762  cntotbnd  37797  fzsplitnd  41977  lcmineqlem6  42029  lcmineqlem18  42041  aks4d1p1p1  42058  aks4d1p8d3  42081  aks4d1p8  42082  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij  42097  primrootspoweq0  42101  hashscontpow1  42116  aks6d1c3  42118  aks6d1c4  42119  aks6d1c5lem1  42131  aks6d1c5lem2  42133  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem3  42167  unitscyglem2  42191  unitscyglem4  42193  sumcubes  42308  oexpreposd  42317  exp11d  42321  dvdsexpb  42330  mzpsubmpt  42738  lzenom  42765  diophun  42768  eqrabdioph  42772  irrapxlem2  42818  irrapxlem3  42819  pellexlem6  42829  pell1234qrreccl  42849  pellfund14  42893  rmxyneg  42916  rmxyadd  42917  rmxp1  42928  rmxm1  42930  rmym1  42931  rmxluc  42932  rmyluc  42933  rmyluc2  42934  rmxdbl  42935  rmydbl  42936  congadd  42962  congsub  42966  congabseq  42970  acongrep  42976  acongeq  42979  jm2.18  42984  jm2.19lem1  42985  jm2.19lem2  42986  jm2.19lem3  42987  jm2.22  42991  jm2.23  42992  jm2.20nn  42993  jm2.25  42995  jm2.26lem3  42997  jm2.27c  43003  nzss  44313  hashnzfz  44316  hashnzfz2  44317  hashnzfzclim  44318  uzmptshftfval  44342  sineq0ALT  44933  fzisoeu  45305  fperiodmul  45309  monoord2xrv  45486  fmul01lt1lem2  45590  sumnnodd  45635  dvdsn1add  45944  dvnmul  45948  dvnprodlem1  45951  stoweidlem11  46016  stoweidlem26  46031  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkeritg  46107  fourierdlem26  46138  fourierdlem48  46159  fourierdlem49  46160  fourierdlem79  46190  fourierdlem91  46202  fourierdlem103  46214  fourierdlem104  46215  fouriersw  46236  etransclem1  46240  etransclem4  46243  etransclem8  46247  etransclem9  46248  etransclem15  46254  etransclem17  46256  etransclem18  46257  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem35  46274  etransclem38  46277  etransclem41  46280  etransclem44  46283  etransclem45  46284  etransclem46  46285  etransclem47  46286  etransclem48  46287  2elfz2melfz  47323  ceilbi  47338  fldivmod  47343  submodaddmod  47346  zplusmodne  47348  m1modne  47353  minusmod5ne  47354  submodlt  47355  minusmodnep2tmod  47358  m1modmmod  47363  modmkpkne  47366  modmknepk  47367  mod2addne  47369  modm2nep1  47371  modm1nep2  47373  modm1nem2  47374  fsumsplitsndif  47378  iccpartgtprec  47425  fargshiftf1  47446  fargshiftfo  47447  mod42tp1mod8  47607  sfprmdvdsmersenne  47608  lighneallem3  47612  lighneallem4b  47614  modexp2m1d  47617  dfodd6  47642  onego  47651  m1expoddALTV  47653  zofldiv2ALTV  47667  oddflALTV  47668  oexpnegALTV  47682  omoeALTV  47690  omeoALTV  47691  epoo  47708  emoo  47709  epee  47710  emee  47711  evensumeven  47712  evenltle  47722  even3prm2  47724  mogoldbblem  47725  fppr2odd  47736  fpprwppr  47744  fpprwpprb  47745  sbgoldbst  47783  sbgoldbaltlem2  47785  sgoldbeven3prm  47788  nnsum3primesprm  47795  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem2  47811  bgoldbtbndlem4  47813  bgoldbtbnd  47814  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  gpg5nbgrvtx13starlem2  48067  gpg3nbgrvtx0  48071  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  2zrngamnd  48239  2zrngacmnd  48240  2zrngagrp  48241  2zrngALT  48246  2zrngnmlid  48247  2zrngnmlid2  48249  ztprmneprm  48339  altgsumbcALT  48345  zofldiv2  48524  fllogbd  48553  nnpw2blen  48573  blen1b  48581  blennngt2o2  48585  blennn0e2  48587  dig2nn1st  48598  dignn0flhalflem1  48608