Theorem zcnd 12623

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11025  ℤcz 12513

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 11084

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-neg 11369  df-z 12514

This theorem is referenced by:  zsupss  12876  rpnnen1lem5  12920  fzm1  13550  fzrevral  13555  fzshftral  13558  nn0disj  13587  predfz  13596  fzoss2  13631  elfzo0suble  13650  fzo0addelr  13663  elfzoext  13666  fzosubel  13668  fzosubel3  13670  fzocatel  13673  fzosplitsnm1  13684  elfzom1elp1fzo1  13711  fzom1ne1  13729  2tnp1ge0ge0  13777  quoremz  13803  intfrac2  13806  intfracq  13807  flpmodeq  13822  moddiffl  13830  modmul1  13875  modmul12d  13876  modfzo0difsn  13894  modsumfzodifsn  13895  addmodlteq  13897  uzrdgxfr  13918  fzen2  13920  monoord2  13984  seqf1olem1  13992  seqf1olem2  13993  seqz  14001  expaddzlem  14056  znsqcld  14113  modexp  14189  sqoddm1div8  14194  bcm1k  14266  bcp1nk  14268  bcval5  14269  bcpasc  14272  hashfz  14378  hashfzo  14380  hashfzp1  14382  hashbclem  14403  seqcoll  14415  ccatval3  14530  ccatlid  14538  ccatass  14540  ccatalpha  14545  swrdfv0  14601  swrdfv2  14613  swrds1  14618  ccatswrd  14620  pfxfv  14634  ccatpfx  14652  swrdpfx  14658  pfxccatin12lem2  14682  spllen  14705  revccat  14717  revrev  14718  cshwidxmod  14754  cshwidxm1  14758  cshweqrep  14772  2cshwcshw  14776  cshimadifsn0  14781  swrds2m  14892  seqshft  15036  fzomaxdif  15295  climshft2  15533  iserex  15608  isercoll2  15620  serf0  15632  iseraltlem2  15634  iseraltlem3  15635  iseralt  15636  sumrblem  15662  fsumm1  15702  fsumsplitsnun  15706  fsump1  15707  fsumshftm  15732  fsumrev2  15733  telfsumo  15754  fsumparts  15758  binomlem  15783  isumshft  15793  isumsplit  15794  isum1p  15795  arisum  15814  pwdif  15822  cvgrat  15837  mertenslem1  15838  ntrivcvg  15851  ntrivcvgtail  15854  prodrblem  15883  fprodser  15903  fprodm1  15921  fprodp1  15923  fprodrev  15931  fprodmodd  15951  fallfacval3  15966  fallfacfwd  15990  0fallfac  15991  binomfallfaclem2  15994  fallfacval4  15997  fsumkthpow  16010  eirrlem  16160  sqrt2irrlem  16204  addmulmodb  16223  dvds2ln  16247  dvdsadd2b  16264  fsumdvds  16266  fzocongeq  16282  addmodlteqALT  16283  dvdsexp  16286  dvdsmod  16287  3dvds  16289  fprodfvdvdsd  16292  odd2np1  16299  oddm1even  16301  oexpneg  16303  mod2eq1n2dvds  16305  mulsucdiv2z  16311  zob  16317  ltoddhalfle  16319  sumodd  16346  pwp1fsum  16349  divalglem0  16351  divalglem4  16354  divalglem8  16358  divalgb  16362  divalgmod  16364  modremain  16366  flodddiv4  16373  bitsp1  16389  bitsfzo  16393  bitsmod  16394  bitsinv1lem  16399  bitsf1  16404  sadaddlem  16424  bitsres  16431  bitsuz  16432  bitsshft  16433  smumullem  16450  modgcd  16490  gcdmultipled  16492  dvdsgcdidd  16495  bezoutlem1  16497  bezoutlem2  16498  bezoutlem3  16499  bezoutlem4  16500  dvdsmulgcd  16514  rplpwr  16516  lcmid  16567  absprodnn  16576  mulgcddvds  16613  divgcdcoprm0  16623  cncongr1  16625  cncongr2  16626  dvdszzq  16680  rpexp  16681  prmdvdsbc  16685  qmuldeneqnum  16706  numdensq  16713  qden1elz  16716  numdenexp  16719  hashdvds  16734  phiprm  16736  eulerthlem2  16741  fermltl  16743  prmdiv  16744  prmdiveq  16745  hashgcdlem  16747  odzdvds  16755  vfermltlALT  16762  modprm0  16765  modprmn0modprm0  16767  pythagtriplem6  16781  pythagtriplem7  16782  pythagtriplem15  16789  pcpremul  16803  pceulem  16805  pczpre  16807  pcdiv  16812  pcqmul  16813  pcqdiv  16817  pcexp  16819  pcaddlem  16848  pcadd  16849  fldivp1  16857  pcfac  16859  pcbc  16860  prmpwdvds  16864  prmreclem4  16879  4sqlem5  16902  4sqlem8  16905  4sqlem9  16906  4sqlem10  16907  4sqlem11  16915  4sqlem14  16918  4sqlem16  16920  4sqlem17  16921  vdwapun  16934  vdwnnlem2  16956  prmop1  16998  prmdvdsprmo  17002  prmgaplem7  17017  prmlem0  17065  chnlt  18578  mulgsubcl  19053  mulgdirlem  19070  mulgdir  19071  mulgass  19076  mulgmodid  19078  mulgsubdir  19079  psgnunilem5  19458  psgnunilem2  19459  psgnunilem4  19461  m1expaddsub  19462  psgnuni  19463  odnncl  19509  odmulg  19520  odbezout  19522  sylow1lem1  19562  sylow2alem2  19582  efgsres  19702  efgredleme  19707  efgredlemc  19709  odadd1  19812  odadd2  19813  cyggeninv  19847  gsummptshft  19900  ablfacrp  20032  pgpfac1lem3  20043  fincygsubgodd  20078  srgbinomlem3  20198  srgbinomlem4  20199  zringmulg  21444  zringlpirlem1  21450  zringlpirlem3  21452  prmirredlem  21460  fermltlchr  21517  zndvds0  21538  znf1o  21539  znunit  21551  cayhamlem1  22839  tgpmulg  24066  zdis  24790  uniioombllem3  25560  mbfi1fseqlem4  25693  dvexp3  25953  aareccl  26301  aalioulem1  26307  geolim3  26314  aaliou3lem2  26318  aaliou3lem6  26323  ulmshft  26366  sineq0  26499  efif1olem2  26518  igamz  27023  wilthlem1  27043  wilthlem2  27044  basellem3  27058  mumul  27156  musum  27166  musumsum  27167  muinv  27168  ppiub  27179  chtub  27187  logfac2  27192  chpchtsum  27194  dchrptlem1  27239  pcbcctr  27251  bcmono  27252  bposlem5  27263  bposlem6  27264  lgslem1  27272  lgsval2lem  27282  lgsval4a  27294  lgsneg  27296  lgsneg1  27297  lgsmod  27298  lgsdirprm  27306  lgsdir  27307  lgsdilem2  27308  lgsdi  27309  lgsne0  27310  lgsabs1  27311  lgssq  27312  lgssq2  27313  lgsmulsqcoprm  27318  lgsdirnn0  27319  lgsdinn0  27320  lgsqrlem1  27321  gausslemma2dlem1a  27340  gausslemma2dlem1  27341  gausslemma2dlem4  27344  gausslemma2dlem5a  27345  gausslemma2dlem5  27346  gausslemma2dlem6  27347  gausslemma2d  27349  lgseisenlem1  27350  lgseisenlem2  27351  lgseisenlem3  27352  lgseisenlem4  27353  lgsquadlem1  27355  lgsquad2lem1  27359  lgsquad3  27362  2lgslem1b  27367  2lgsoddprmlem2  27384  2sqlem3  27395  2sqlem4  27396  2sqlem8a  27400  2sqlem8  27401  2sqlem11  27404  2sqblem  27406  2sqn0  27409  2sqmod  27411  dchrisumlem1  27464  dchrmusum2  27469  dchrvmasumlem1  27470  dchrvmasum2lem  27471  mudivsum  27505  mulogsum  27507  mulog2sumlem2  27510  selberglem1  27520  selberglem3  27522  selberg  27523  pntpbnd2  27562  pntlemf  27580  padicabvcxp  27607  axlowdimlem14  29036  axlowdimlem16  29038  pthdadjvtx  29809  crctcshwlkn0lem4  29894  crctcshwlkn0lem5  29895  crctcshlem4  29901  crctcsh  29905  clwwlkccatlem  30072  clwwisshclwws  30098  eucrctshift  30326  fzm1ne1  32874  fzspl  32875  bcm1n  32881  elq2  32898  znumd  32899  zdend  32900  numdenneg  32901  divnumden2  32902  ltesubnnd  32909  ccatf1  33022  swrdrn3  33028  swrdf1  33029  cshwrnid  33034  gsumzrsum  33139  gsummulsubdishift1  33142  cycpmco2lem3  33202  cycpmco2lem4  33203  cycpmco2lem5  33204  cycpmco2lem6  33205  cycpmco2  33207  archiabllem1  33267  archiabllem2c  33269  elrgspnlem1  33316  elrgspnlem2  33317  znfermltl  33439  zringidom  33624  zringfrac  33627  esplyindfv  33733  zconstr  33922  cos9thpiminplylem2  33941  zrhnm  34125  cnzh  34126  rezh  34127  zrhcntr  34137  qqhval2lem  34139  qqhghm  34146  qqhrhm  34147  qqhnm  34148  ballotlemfc0  34651  ballotlemfcc  34652  ballotlemic  34665  ballotlem1c  34666  ballotlemsgt1  34669  ballotlemsdom  34670  ballotlemsel1i  34671  ballotlemsf1o  34672  ballotlemsima  34674  ballotlemfrceq  34687  ballotlemfrcn0  34688  ballotlem1ri  34693  signsplypnf  34708  itgexpif  34764  fsum2dsub  34765  breprexplemc  34790  vtsprod  34797  circlemeth  34798  revpfxsfxrev  35312  swrdrevpfx  35313  revwlk  35321  swrdwlk  35323  divcnvlin  35929  fwddifnp1  36361  knoppndvlem2  36779  knoppndvlem7  36784  knoppndvlem14  36791  knoppndvlem16  36793  ltflcei  37933  poimirlem1  37946  poimirlem2  37947  poimirlem7  37952  poimirlem16  37961  poimirlem17  37962  poimirlem19  37964  poimirlem20  37965  poimirlem24  37969  poimirlem31  37976  poimirlem32  37977  fdc  38070  mettrifi  38082  caushft  38086  cntotbnd  38121  fzsplitnd  42425  lcmineqlem6  42477  lcmineqlem18  42489  aks4d1p1p1  42506  aks4d1p8d3  42529  aks4d1p8  42530  primrootscoprmpow  42542  posbezout  42543  primrootscoprbij  42545  primrootspoweq0  42549  hashscontpow1  42564  aks6d1c3  42566  aks6d1c4  42567  aks6d1c5lem1  42579  aks6d1c5lem2  42581  sticksstones10  42598  sticksstones12a  42600  sticksstones12  42601  aks6d1c6lem3  42615  unitscyglem2  42639  unitscyglem4  42641  sumcubes  42749  oexpreposd  42758  exp11d  42762  dvdsexpb  42771  mzpsubmpt  43179  lzenom  43206  diophun  43209  eqrabdioph  43213  irrapxlem2  43259  irrapxlem3  43260  pellexlem6  43270  pell1234qrreccl  43290  pellfund14  43334  rmxyneg  43356  rmxyadd  43357  rmxp1  43368  rmxm1  43370  rmym1  43371  rmxluc  43372  rmyluc  43373  rmyluc2  43374  rmxdbl  43375  rmydbl  43376  congadd  43402  congsub  43406  congabseq  43410  acongrep  43416  acongeq  43419  jm2.18  43424  jm2.19lem1  43425  jm2.19lem2  43426  jm2.19lem3  43427  jm2.22  43431  jm2.23  43432  jm2.20nn  43433  jm2.25  43435  jm2.26lem3  43437  jm2.27c  43443  nzss  44752  hashnzfz  44755  hashnzfz2  44756  hashnzfzclim  44757  uzmptshftfval  44781  sineq0ALT  45371  fzisoeu  45741  fperiodmul  45745  monoord2xrv  45919  fmul01lt1lem2  46023  sumnnodd  46068  dvdsn1add  46375  dvnmul  46379  dvnprodlem1  46382  stoweidlem11  46447  stoweidlem26  46462  dirkertrigeqlem1  46534  dirkertrigeqlem2  46535  dirkertrigeqlem3  46536  dirkertrigeq  46537  dirkeritg  46538  fourierdlem26  46569  fourierdlem48  46590  fourierdlem49  46591  fourierdlem79  46621  fourierdlem91  46633  fourierdlem103  46645  fourierdlem104  46646  fouriersw  46667  etransclem1  46671  etransclem4  46674  etransclem8  46678  etransclem9  46679  etransclem15  46685  etransclem17  46687  etransclem18  46688  etransclem20  46690  etransclem21  46691  etransclem22  46692  etransclem23  46693  etransclem24  46694  etransclem25  46695  etransclem35  46705  etransclem38  46708  etransclem41  46711  etransclem44  46714  etransclem45  46715  etransclem46  46716  etransclem47  46717  etransclem48  46718  chnerlem2  47319  2elfz2melfz  47768  ceilbi  47787  flmrecm1  47793  fldivmod  47794  submodaddmod  47797  zplusmodne  47799  m1modne  47804  minusmod5ne  47805  submodlt  47806  minusmodnep2tmod  47809  m1modmmod  47814  modmkpkne  47817  modmknepk  47818  mod2addne  47820  modm2nep1  47822  modm1nep2  47824  modm1nem2  47825  2timesltsq  47828  fsumsplitsndif  47831  iccpartgtprec  47882  fargshiftf1  47903  fargshiftfo  47904  nprmmul3  47991  mod42tp1mod8  48067  sfprmdvdsmersenne  48068  lighneallem3  48072  lighneallem4b  48074  modexp2m1d  48077  nprmdvdsfacm1lem1  48085  ppivalnnprm  48090  dfodd6  48115  onego  48124  m1expoddALTV  48126  zofldiv2ALTV  48140  oddflALTV  48141  oexpnegALTV  48155  omoeALTV  48163  omeoALTV  48164  epoo  48181  emoo  48182  epee  48183  emee  48184  evensumeven  48185  evenltle  48195  even3prm2  48197  mogoldbblem  48198  fppr2odd  48209  fpprwppr  48217  fpprwpprb  48218  sbgoldbst  48256  sbgoldbaltlem2  48258  sgoldbeven3prm  48261  nnsum3primesprm  48268  nnsum4primesodd  48274  nnsum4primesoddALTV  48275  nnsum4primeseven  48278  nnsum4primesevenALTV  48279  bgoldbtbndlem2  48284  bgoldbtbndlem4  48286  bgoldbtbnd  48287  gpgedgvtx1  48540  gpgvtxedg0  48541  gpgvtxedg1  48542  gpg5nbgrvtx13starlem2  48550  gpg3nbgrvtx0  48554  pgnbgreunbgrlem2lem1  48592  pgnbgreunbgrlem2lem2  48593  pgnbgreunbgrlem2lem3  48594  2zrngamnd  48725  2zrngacmnd  48726  2zrngagrp  48727  2zrngALT  48732  2zrngnmlid  48733  2zrngnmlid2  48735  ztprmneprm  48825  altgsumbcALT  48831  zofldiv2  49009  fllogbd  49038  nnpw2blen  49058  blen1b  49066  blennngt2o2  49070  blennn0e2  49072  dig2nn1st  49083  dignn0flhalflem1  49093