Theorem zcnd 12705

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ℂcc 11102  ℤcz 12595

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11161

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11448  df-z 12596

This theorem is used by:  zsupss  12965  rpnnen1lem5  13009  fzm1  13640  fzrevral  13645  fzshftral  13648  nn0disj  13677  predfz  13686  fzoss2  13721  elfzo0suble  13740  fzo0addelr  13753  elfzoext  13756  fzosubel  13758  fzosubel3  13760  fzocatel  13763  fzosplitsnm1  13774  elfzom1elp1fzo1  13801  fzom1ne1  13819  2tnp1ge0ge0  13867  quoremz  13893  intfrac2  13896  intfracq  13897  flpmodeq  13912  moddiffl  13920  modmul1  13965  modmul12d  13966  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  uzrdgxfr  14008  fzen2  14010  monoord2  14074  seqf1olem1  14082  seqf1olem2  14083  seqz  14091  expaddzlem  14146  znsqcld  14203  modexp  14279  sqoddm1div8  14284  bcm1k  14356  bcp1nk  14358  bcval5  14359  bcpasc  14362  hashfz  14469  hashfzo  14471  hashfzp1  14473  hashbclem  14494  seqcoll  14506  ccatval3  14621  ccatlid  14629  ccatass  14631  ccatalpha  14636  swrdfv0  14692  swrdfv2  14704  swrds1  14709  ccatswrd  14711  pfxfv  14725  ccatpfx  14743  swrdpfx  14749  pfxccatin12lem2  14773  spllen  14796  revccat  14808  revrev  14809  cshwidxmod  14845  cshwidxm1  14849  cshweqrep  14863  2cshwcshw  14867  cshimadifsn0  14872  swrds2m  14983  seqshft  15127  fzomaxdif  15400  climshft2  15638  iserex  15713  isercoll2  15725  serf0  15737  iseraltlem2  15739  iseraltlem3  15740  iseralt  15741  sumrblem  15767  fsumm1  15807  fsumsplitsnun  15811  fsump1  15812  fsumshftm  15837  fsumrev2  15838  telfsumo  15859  fsumparts  15863  binomlem  15888  isumshft  15898  isumsplit  15899  isum1p  15900  arisum  15919  pwdif  15927  cvgrat  15942  mertenslem1  15943  ntrivcvg  15956  ntrivcvgtail  15959  prodrblem  15988  fprodser  16008  fprodm1  16026  fprodp1  16028  fprodrev  16036  fprodmodd  16056  fallfacval3  16071  fallfacfwd  16094  0fallfac  16095  binomfallfaclem2  16098  fallfacval4  16101  fsumkthpow  16114  eirrlem  16264  sqrt2irrlem  16308  addmulmodb  16327  dvds2ln  16351  dvdsadd2b  16368  fsumdvds  16370  fzocongeq  16386  addmodlteqALT  16387  dvdsexp  16390  dvdsmod  16391  3dvds  16393  fprodfvdvdsd  16396  odd2np1  16403  oddm1even  16405  oexpneg  16407  mod2eq1n2dvds  16409  mulsucdiv2z  16415  zob  16421  ltoddhalfle  16423  sumodd  16450  pwp1fsum  16453  divalglem0  16455  divalglem4  16458  divalglem8  16462  divalgb  16466  divalgmod  16468  modremain  16470  flodddiv4  16477  bitsp1  16493  bitsfzo  16497  bitsmod  16498  bitsinv1lem  16503  bitsf1  16508  sadaddlem  16528  bitsres  16535  bitsuz  16536  bitsshft  16537  smumullem  16554  modgcd  16594  gcdmultipled  16596  dvdsgcdidd  16599  bezoutlem1  16601  bezoutlem2  16602  bezoutlem3  16603  bezoutlem4  16604  dvdsmulgcd  16618  rplpwr  16620  lcmid  16671  absprodnn  16680  mulgcddvds  16717  divgcdcoprm0  16727  cncongr1  16729  cncongr2  16730  dvdszzq  16784  rpexp  16785  prmdvdsbc  16789  qmuldeneqnum  16810  numdensq  16817  qden1elz  16820  numdenexp  16823  hashdvds  16838  phiprm  16840  eulerthlem2  16845  fermltl  16847  prmdiv  16848  prmdiveq  16849  hashgcdlem  16851  odzdvds  16859  vfermltlALT  16866  modprm0  16869  modprmn0modprm0  16871  pythagtriplem6  16885  pythagtriplem7  16886  pythagtriplem15  16893  pcpremul  16907  pceulem  16909  pczpre  16911  pcdiv  16916  pcqmul  16917  pcqdiv  16921  pcexp  16923  pcaddlem  16952  pcadd  16953  fldivp1  16961  pcfac  16963  pcbc  16964  prmpwdvds  16968  prmreclem4  16983  4sqlem5  17006  4sqlem8  17009  4sqlem9  17010  4sqlem10  17011  4sqlem11  17019  4sqlem14  17022  4sqlem16  17024  4sqlem17  17025  vdwapun  17038  vdwnnlem2  17060  prmop1  17102  prmdvdsprmo  17106  prmgaplem7  17121  prmlem0  17169  chnlt  18683  mulgsubcl  19158  mulgdirlem  19175  mulgdir  19176  mulgass  19181  mulgmodid  19183  mulgsubdir  19184  psgnunilem5  19568  psgnunilem2  19569  psgnunilem4  19571  m1expaddsub  19572  psgnuni  19573  odnncl  19619  odmulg  19630  odbezout  19632  sylow1lem1  19672  sylow2alem2  19692  efgsres  19812  efgredleme  19817  efgredlemc  19819  odadd1  19922  odadd2  19923  cyggeninv  19957  gsummptshft  20010  ablfacrp  20142  pgpfac1lem3  20153  fincygsubgodd  20188  srgbinomlem3  20314  srgbinomlem4  20315  zringmulg  21615  zringlpirlem1  21621  zringlpirlem3  21623  prmirredlem  21631  fermltlchr  21688  zndvds0  21709  znf1o  21710  znunit  21722  cayhamlem1  23032  tgpmulg  24259  zdis  24983  uniioombllem3  25753  mbfi1fseqlem4  25886  dvexp3  26146  aareccl  26498  aalioulem1  26504  geolim3  26511  aaliou3lem2  26515  aaliou3lem6  26520  ulmshft  26562  sineq0  26698  efif1olem2  26717  igamz  27221  wilthlem1  27241  wilthlem2  27242  basellem3  27256  mumul  27354  musum  27364  musumsum  27365  muinv  27366  ppiub  27377  chtub  27385  logfac2  27390  chpchtsum  27392  dchrptlem1  27437  pcbcctr  27449  bcmono  27450  bposlem5  27461  bposlem6  27462  lgslem1  27470  lgsval2lem  27480  lgsval4a  27492  lgsneg  27494  lgsneg1  27495  lgsmod  27496  lgsdirprm  27504  lgsdir  27505  lgsdilem2  27506  lgsdi  27507  lgsne0  27508  lgsabs1  27509  lgssq  27510  lgssq2  27511  lgsmulsqcoprm  27516  lgsdirnn0  27517  lgsdinn0  27518  lgsqrlem1  27519  gausslemma2dlem1a  27538  gausslemma2dlem1  27539  gausslemma2dlem4  27542  gausslemma2dlem5a  27543  gausslemma2dlem5  27544  gausslemma2dlem6  27545  gausslemma2d  27547  lgseisenlem1  27548  lgseisenlem2  27549  lgseisenlem3  27550  lgseisenlem4  27551  lgsquadlem1  27553  lgsquad2lem1  27557  lgsquad3  27560  2lgslem1b  27565  2lgsoddprmlem2  27582  2sqlem3  27593  2sqlem4  27594  2sqlem8a  27598  2sqlem8  27599  2sqlem11  27602  2sqblem  27604  2sqn0  27607  2sqmod  27609  dchrisumlem1  27662  dchrmusum2  27667  dchrvmasumlem1  27668  dchrvmasum2lem  27669  mudivsum  27703  mulogsum  27705  mulog2sumlem2  27708  selberglem1  27718  selberglem3  27720  selberg  27721  pntpbnd2  27760  pntlemf  27778  padicabvcxp  27805  axlowdimlem14  29314  axlowdimlem16  29316  pthdadjvtx  30086  crctcshwlkn0lem4  30171  crctcshwlkn0lem5  30172  crctcshlem4  30178  crctcsh  30182  clwwlkccatlem  30349  clwwisshclwws  30375  eucrctshift  30603  fzm1ne1  33142  fzspl  33143  bcm1n  33149  elq2  33165  znumd  33166  zdend  33167  numdenneg  33168  divnumden2  33169  ltesubnnd  33176  ccatf1  33278  swrdrn3  33284  swrdf1  33285  cshwrnid  33290  gsumzrsum  33394  gsummulsubdishift1  33397  cycpmco2lem3  33457  cycpmco2lem4  33458  cycpmco2lem5  33459  cycpmco2lem6  33460  cycpmco2  33462  archiabllem1  33522  archiabllem2c  33524  elrgspnlem1  33571  elrgspnlem2  33572  znfermltl  33690  zringidom  33850  zringfrac  33853  esplyindfv  33975  zconstr  34163  cos9thpiminplylem2  34182  zrhnm  34366  cnzh  34367  rezh  34368  zrhcntr  34378  qqhval2lem  34380  qqhghm  34387  qqhrhm  34388  qqhnm  34389  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemic  34906  ballotlem1c  34907  ballotlemsgt1  34910  ballotlemsdom  34911  ballotlemsel1i  34912  ballotlemsf1o  34913  ballotlemsima  34915  ballotlemfrceq  34928  ballotlemfrcn0  34929  ballotlem1ri  34934  signsplypnf  34946  itgexpif  35002  fsum2dsub  35003  breprexplemc  35028  vtsprod  35035  circlemeth  35036  revpfxsfxrev  35615  swrdrevpfx  35616  revwlk  35625  swrdwlk  35627  divcnvlin  36233  fwddifnp1  36665  knoppndvlem2  37130  knoppndvlem7  37135  knoppndvlem14  37142  knoppndvlem16  37144  ltflcei  38287  poimirlem1  38300  poimirlem2  38301  poimirlem7  38306  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem24  38323  poimirlem31  38330  poimirlem32  38331  fdc  38424  mettrifi  38436  caushft  38440  cntotbnd  38475  fzsplitnd  42777  lcmineqlem6  42829  lcmineqlem18  42841  aks4d1p1p1  42858  aks4d1p8d3  42881  aks4d1p8  42882  primrootscoprmpow  42894  posbezout  42895  primrootscoprbij  42897  primrootspoweq0  42901  hashscontpow1  42916  aks6d1c3  42918  aks6d1c4  42919  aks6d1c5lem1  42931  aks6d1c5lem2  42933  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  aks6d1c6lem3  42967  unitscyglem2  42991  unitscyglem4  42993  sumcubes  43102  oexpreposd  43111  exp11d  43115  dvdsexpb  43124  mzpsubmpt  43502  lzenom  43529  diophun  43532  eqrabdioph  43536  irrapxlem2  43578  irrapxlem3  43579  pellexlem6  43589  pell1234qrreccl  43609  pellfund14  43653  rmxyneg  43675  rmxyadd  43676  rmxp1  43687  rmxm1  43689  rmym1  43690  rmxluc  43691  rmyluc  43692  rmyluc2  43693  rmxdbl  43694  rmydbl  43695  congadd  43721  congsub  43725  congabseq  43729  acongrep  43735  acongeq  43738  jm2.18  43743  jm2.19lem1  43744  jm2.19lem2  43745  jm2.19lem3  43746  jm2.22  43750  jm2.23  43751  jm2.20nn  43752  jm2.25  43754  jm2.26lem3  43756  jm2.27c  43762  nzss  45055  hashnzfz  45058  hashnzfz2  45059  hashnzfzclim  45060  uzmptshftfval  45084  sineq0ALT  45673  fzisoeu  46047  fperiodmul  46051  monoord2xrv  46225  fmul01lt1lem2  46329  sumnnodd  46374  dvdsn1add  46681  dvnmul  46685  dvnprodlem1  46688  stoweidlem11  46753  stoweidlem26  46768  dirkertrigeqlem1  46840  dirkertrigeqlem2  46841  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkeritg  46844  fourierdlem26  46875  fourierdlem48  46896  fourierdlem49  46897  fourierdlem79  46927  fourierdlem91  46939  fourierdlem103  46951  fourierdlem104  46952  fouriersw  46973  etransclem1  46977  etransclem4  46980  etransclem8  46984  etransclem9  46985  etransclem15  46991  etransclem17  46993  etransclem18  46994  etransclem20  46996  etransclem21  46997  etransclem22  46998  etransclem23  46999  etransclem24  47000  etransclem25  47001  etransclem35  47011  etransclem38  47014  etransclem41  47017  etransclem44  47020  etransclem45  47021  etransclem46  47022  etransclem47  47023  etransclem48  47024  chnerlem2  47627  2elfz2melfz  48083  ceilbi  48102  flmrecm1  48108  fldivmod  48109  submodaddmod  48112  zplusmodne  48114  m1modne  48119  minusmod5ne  48120  submodlt  48121  minusmodnep2tmod  48124  m1modmmod  48129  modmkpkne  48132  modmknepk  48133  mod2addne  48135  modm2nep1  48137  modm1nep2  48139  modm1nem2  48140  2timesltsq  48143  fsumsplitsndif  48146  iccpartgtprec  48197  fargshiftf1  48218  fargshiftfo  48219  nprmmul3  48306  mod42tp1mod8  48382  sfprmdvdsmersenne  48383  lighneallem3  48387  lighneallem4b  48389  modexp2m1d  48392  nprmdvdsfacm1lem1  48400  ppivalnnprm  48405  dfodd6  48430  onego  48439  m1expoddALTV  48441  zofldiv2ALTV  48455  oddflALTV  48456  oexpnegALTV  48470  omoeALTV  48478  omeoALTV  48479  epoo  48496  emoo  48497  epee  48498  emee  48499  evensumeven  48500  evenltle  48510  even3prm2  48512  mogoldbblem  48513  fppr2odd  48524  fpprwppr  48532  fpprwpprb  48533  sbgoldbst  48571  sbgoldbaltlem2  48573  sgoldbeven3prm  48576  nnsum3primesprm  48583  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  bgoldbtbndlem2  48599  bgoldbtbndlem4  48601  bgoldbtbnd  48602  gpgedgvtx1  48855  gpgvtxedg0  48856  gpgvtxedg1  48857  gpg5nbgrvtx13starlem2  48865  gpg3nbgrvtx0  48869  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  2zrngamnd  49040  2zrngacmnd  49041  2zrngagrp  49042  2zrngALT  49047  2zrngnmlid  49048  2zrngnmlid2  49050  ztprmneprm  49155  altgsumbcALT  49161  zofldiv2  49339  fllogbd  49368  nnpw2blen  49388  blen1b  49396  blennngt2o2  49400  blennn0e2  49402  dig2nn1st  49413  dignn0flhalflem1  49423