Theorem zcnd 12723

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614

This theorem is referenced by:  zsupss  12979  rpnnen1lem5  13023  fzm1  13647  fzrevral  13652  fzshftral  13655  nn0disj  13684  predfz  13693  fzoss2  13727  elfzo0suble  13746  fzo0addelr  13758  elfzoext  13761  fzosubel  13763  fzosubel3  13765  fzocatel  13768  fzosplitsnm1  13779  elfzom1elp1fzo1  13806  2tnp1ge0ge0  13869  quoremz  13895  intfrac2  13898  intfracq  13899  flpmodeq  13914  moddiffl  13922  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  14202  modexp  14277  sqoddm1div8  14282  bcm1k  14354  bcp1nk  14356  bcval5  14357  bcpasc  14360  hashfz  14466  hashfzo  14468  hashfzp1  14470  hashbclem  14491  seqcoll  14503  ccatval3  14617  ccatlid  14624  ccatass  14626  ccatalpha  14631  swrdfv0  14687  swrdfv2  14699  swrds1  14704  ccatswrd  14706  pfxfv  14720  ccatpfx  14739  swrdpfx  14745  pfxccatin12lem2  14769  spllen  14792  revccat  14804  revrev  14805  cshwidxmod  14841  cshwidxm1  14845  cshweqrep  14859  2cshwcshw  14864  cshimadifsn0  14869  swrds2m  14980  seqshft  15124  fzomaxdif  15382  climshft2  15618  iserex  15693  isercoll2  15705  serf0  15717  iseraltlem2  15719  iseraltlem3  15720  iseralt  15721  sumrblem  15747  fsumm1  15787  fsumsplitsnun  15791  fsump1  15792  fsumshftm  15817  fsumrev2  15818  telfsumo  15838  fsumparts  15842  binomlem  15865  isumshft  15875  isumsplit  15876  isum1p  15877  arisum  15896  pwdif  15904  cvgrat  15919  mertenslem1  15920  ntrivcvg  15933  ntrivcvgtail  15936  prodrblem  15965  fprodser  15985  fprodm1  16003  fprodp1  16005  fprodrev  16013  fprodmodd  16033  fallfacval3  16048  fallfacfwd  16072  0fallfac  16073  binomfallfaclem2  16076  fallfacval4  16079  fsumkthpow  16092  eirrlem  16240  sqrt2irrlem  16284  addmulmodb  16303  dvds2ln  16326  dvdsadd2b  16343  fsumdvds  16345  fzocongeq  16361  addmodlteqALT  16362  dvdsexp  16365  dvdsmod  16366  3dvds  16368  fprodfvdvdsd  16371  odd2np1  16378  oddm1even  16380  oexpneg  16382  mod2eq1n2dvds  16384  mulsucdiv2z  16390  zob  16396  ltoddhalfle  16398  sumodd  16425  pwp1fsum  16428  divalglem0  16430  divalglem4  16433  divalglem8  16437  divalgb  16441  divalgmod  16443  modremain  16445  flodddiv4  16452  bitsp1  16468  bitsfzo  16472  bitsmod  16473  bitsinv1lem  16478  bitsf1  16483  sadaddlem  16503  bitsres  16510  bitsuz  16511  bitsshft  16512  smumullem  16529  modgcd  16569  gcdmultipled  16571  dvdsgcdidd  16574  bezoutlem1  16576  bezoutlem2  16577  bezoutlem3  16578  bezoutlem4  16579  dvdsmulgcd  16593  rplpwr  16595  lcmid  16646  absprodnn  16655  mulgcddvds  16692  divgcdcoprm0  16702  cncongr1  16704  cncongr2  16705  dvdszzq  16758  rpexp  16759  prmdvdsbc  16763  qmuldeneqnum  16784  numdensq  16791  qden1elz  16794  numdenexp  16797  hashdvds  16812  phiprm  16814  eulerthlem2  16819  fermltl  16821  prmdiv  16822  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  vfermltlALT  16840  modprm0  16843  modprmn0modprm0  16845  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem15  16867  pcpremul  16881  pceulem  16883  pczpre  16885  pcdiv  16890  pcqmul  16891  pcqdiv  16895  pcexp  16897  pcaddlem  16926  pcadd  16927  fldivp1  16935  pcfac  16937  pcbc  16938  prmpwdvds  16942  prmreclem4  16957  4sqlem5  16980  4sqlem8  16983  4sqlem9  16984  4sqlem10  16985  4sqlem11  16993  4sqlem14  16996  4sqlem16  16998  4sqlem17  16999  vdwapun  17012  vdwnnlem2  17034  prmop1  17076  prmdvdsprmo  17080  prmgaplem7  17095  prmlem0  17143  mulgsubcl  19106  mulgdirlem  19123  mulgdir  19124  mulgass  19129  mulgmodid  19131  mulgsubdir  19132  psgnunilem5  19512  psgnunilem2  19513  psgnunilem4  19515  m1expaddsub  19516  psgnuni  19517  odnncl  19563  odmulg  19574  odbezout  19576  sylow1lem1  19616  sylow2alem2  19636  efgsres  19756  efgredleme  19761  efgredlemc  19763  odadd1  19866  odadd2  19867  cyggeninv  19901  gsummptshft  19954  ablfacrp  20086  pgpfac1lem3  20097  fincygsubgodd  20132  srgbinomlem3  20225  srgbinomlem4  20226  zringmulg  21467  zringlpirlem1  21473  zringlpirlem3  21475  prmirredlem  21483  fermltlchr  21544  zndvds0  21569  znf1o  21570  znunit  21582  cayhamlem1  22872  tgpmulg  24101  zdis  24838  uniioombllem3  25620  mbfi1fseqlem4  25753  dvexp3  26016  aareccl  26368  aalioulem1  26374  geolim3  26381  aaliou3lem2  26385  aaliou3lem6  26390  ulmshft  26433  sineq0  26566  efif1olem2  26585  igamz  27091  wilthlem1  27111  wilthlem2  27112  basellem3  27126  mumul  27224  musum  27234  musumsum  27235  muinv  27236  ppiub  27248  chtub  27256  logfac2  27261  chpchtsum  27263  dchrptlem1  27308  pcbcctr  27320  bcmono  27321  bposlem5  27332  bposlem6  27333  lgslem1  27341  lgsval2lem  27351  lgsval4a  27363  lgsneg  27365  lgsneg1  27366  lgsmod  27367  lgsdirprm  27375  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  lgsabs1  27380  lgssq  27381  lgssq2  27382  lgsmulsqcoprm  27387  lgsdirnn0  27388  lgsdinn0  27389  lgsqrlem1  27390  gausslemma2dlem1a  27409  gausslemma2dlem1  27410  gausslemma2dlem4  27413  gausslemma2dlem5a  27414  gausslemma2dlem5  27415  gausslemma2dlem6  27416  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquad2lem1  27428  lgsquad3  27431  2lgslem1b  27436  2lgsoddprmlem2  27453  2sqlem3  27464  2sqlem4  27465  2sqlem8a  27469  2sqlem8  27470  2sqlem11  27473  2sqblem  27475  2sqn0  27478  2sqmod  27480  dchrisumlem1  27533  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  mudivsum  27574  mulogsum  27576  mulog2sumlem2  27579  selberglem1  27589  selberglem3  27591  selberg  27592  pntpbnd2  27631  pntlemf  27649  padicabvcxp  27676  axlowdimlem14  28970  axlowdimlem16  28972  pthdadjvtx  29748  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshlem4  29840  crctcsh  29844  clwwlkccatlem  30008  clwwisshclwws  30034  eucrctshift  30262  fzm1ne1  32790  fzspl  32791  bcm1n  32797  fzom1ne1  32803  znumd  32814  zdend  32815  numdenneg  32816  divnumden2  32817  ltesubnnd  32824  ccatf1  32933  swrdrn3  32940  swrdf1  32941  cshwrnid  32946  chnlt  33003  gsumzrsum  33062  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  archiabllem1  33200  archiabllem2c  33202  elrgspnlem1  33246  elrgspnlem2  33247  znfermltl  33394  zringidom  33579  zringfrac  33582  zrhnm  33968  cnzh  33969  rezh  33970  zrhcntr  33980  qqhval2lem  33982  qqhghm  33989  qqhrhm  33990  qqhnm  33991  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemic  34509  ballotlem1c  34510  ballotlemsgt1  34513  ballotlemsdom  34514  ballotlemsel1i  34515  ballotlemsf1o  34516  ballotlemsima  34518  ballotlemfrceq  34531  ballotlemfrcn0  34532  ballotlem1ri  34537  signsplypnf  34565  itgexpif  34621  fsum2dsub  34622  breprexplemc  34647  vtsprod  34654  circlemeth  34655  revpfxsfxrev  35121  swrdrevpfx  35122  revwlk  35130  swrdwlk  35132  divcnvlin  35733  fwddifnp1  36166  knoppndvlem2  36514  knoppndvlem7  36519  knoppndvlem14  36526  knoppndvlem16  36528  ltflcei  37615  poimirlem1  37628  poimirlem2  37629  poimirlem7  37634  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  poimirlem31  37658  poimirlem32  37659  fdc  37752  mettrifi  37764  caushft  37768  cntotbnd  37803  fzsplitnd  41983  lcmineqlem6  42035  lcmineqlem18  42047  aks4d1p1p1  42064  aks4d1p8d3  42087  aks4d1p8  42088  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootspoweq0  42107  hashscontpow1  42122  aks6d1c3  42124  aks6d1c4  42125  aks6d1c5lem1  42137  aks6d1c5lem2  42139  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem3  42173  unitscyglem2  42197  unitscyglem4  42199  metakunt12  42217  metakunt15  42220  metakunt16  42221  metakunt28  42233  sumcubes  42347  oexpreposd  42357  exp11d  42361  dvdsexpb  42370  mzpsubmpt  42754  lzenom  42781  diophun  42784  eqrabdioph  42788  irrapxlem2  42834  irrapxlem3  42835  pellexlem6  42845  pell1234qrreccl  42865  pellfund14  42909  rmxyneg  42932  rmxyadd  42933  rmxp1  42944  rmxm1  42946  rmym1  42947  rmxluc  42948  rmyluc  42949  rmyluc2  42950  rmxdbl  42951  rmydbl  42952  congadd  42978  congsub  42982  congabseq  42986  acongrep  42992  acongeq  42995  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.19lem3  43003  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.25  43011  jm2.26lem3  43013  jm2.27c  43019  nzss  44336  hashnzfz  44339  hashnzfz2  44340  hashnzfzclim  44341  uzmptshftfval  44365  sineq0ALT  44957  fzisoeu  45312  fperiodmul  45316  monoord2xrv  45494  fmul01lt1lem2  45600  sumnnodd  45645  dvdsn1add  45954  dvnmul  45958  dvnprodlem1  45961  stoweidlem11  46026  stoweidlem26  46041  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkeritg  46117  fourierdlem26  46148  fourierdlem48  46169  fourierdlem49  46170  fourierdlem79  46200  fourierdlem91  46212  fourierdlem103  46224  fourierdlem104  46225  fouriersw  46246  etransclem1  46250  etransclem4  46253  etransclem8  46257  etransclem9  46258  etransclem15  46264  etransclem17  46266  etransclem18  46267  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem35  46284  etransclem38  46287  etransclem41  46290  etransclem44  46293  etransclem45  46294  etransclem46  46295  etransclem47  46296  etransclem48  46297  2elfz2melfz  47330  fldivmod  47340  submodaddmod  47343  zplusmodne  47345  m1modne  47350  minusmod5ne  47351  submodlt  47352  minusmodnep2tmod  47355  fsumsplitsndif  47360  iccpartgtprec  47407  fargshiftf1  47428  fargshiftfo  47429  mod42tp1mod8  47589  sfprmdvdsmersenne  47590  lighneallem3  47594  lighneallem4b  47596  modexp2m1d  47599  dfodd6  47624  onego  47633  m1expoddALTV  47635  zofldiv2ALTV  47649  oddflALTV  47650  oexpnegALTV  47664  omoeALTV  47672  omeoALTV  47673  epoo  47690  emoo  47691  epee  47692  emee  47693  evensumeven  47694  evenltle  47704  even3prm2  47706  mogoldbblem  47707  fppr2odd  47718  fpprwppr  47726  fpprwpprb  47727  sbgoldbst  47765  sbgoldbaltlem2  47767  sgoldbeven3prm  47770  nnsum3primesprm  47777  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem2  47793  bgoldbtbndlem4  47795  bgoldbtbnd  47796  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg3nbgrvtxlem  48023  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0  48032  2zrngamnd  48163  2zrngacmnd  48164  2zrngagrp  48165  2zrngALT  48170  2zrngnmlid  48171  2zrngnmlid2  48173  ztprmneprm  48263  altgsumbcALT  48269  m1modmmod  48442  zofldiv2  48452  fllogbd  48481  nnpw2blen  48501  blen1b  48509  blennngt2o2  48513  blennn0e2  48515  dig2nn1st  48526  dignn0flhalflem1  48536