Theorem zcnd 9701

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  ℤcz 9577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-rab 2529  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578

This theorem is referenced by:  qapne  9971  fzm1  10434  fzrevral  10439  fzshftral  10442  nn0disj  10472  fzoss2  10508  fzo0addelr  10534  elfzoext  10537  fzosubel  10539  fzosubel3  10541  fzocatel  10544  fzosplitsnm1  10554  infssuzex  10593  zsupssdc  10598  qtri3or  10600  exbtwnzlemstep  10607  exbtwnzlemex  10609  rebtwn2zlemstep  10612  rebtwn2z  10614  flqaddz  10657  flqzadd  10658  2tnp1ge0ge0  10661  ceiqm1l  10673  intqfrac2  10681  intfracq  10682  flqdiv  10683  modqvalr  10687  flqpmodeq  10689  modq0  10691  mulqmod0  10692  modqlt  10695  modqdiffl  10697  modqfrac  10699  flqmod  10700  intqfrac  10701  modqmulnn  10704  modqvalp1  10705  modqcyc  10721  modqcyc2  10722  modqadd1  10723  mulqaddmodid  10726  mulp1mod1  10727  modqmul1  10739  modqmul12d  10740  modqnegd  10741  modqmulmodr  10752  modqdi  10754  modqsubdir  10755  modfzo0difsn  10757  modsumfzodifsn  10758  addmodlteq  10760  frecfzen2  10789  uzennn  10798  uzsinds  10806  seq3shft2  10843  monoord2  10848  iseqf1olemab  10864  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seqf1oglem1  10881  seqf1oglem2  10882  expaddzaplem  10944  modqexp  11028  sqoddm1div8  11055  bcm1k  11122  bcp1nk  11124  bcpasc  11128  bcm1n  11131  hashfz  11186  hashfzo  11187  hashfzp1  11189  hashfibclem  11206  seq3coll  11214  ccatval3  11287  ccatlid  11294  ccatass  11296  ccatalpha  11301  swrdfv0  11346  swrdfv2  11355  swrds1  11360  ccatswrd  11362  pfxfv  11376  ccatpfx  11393  swrdpfx  11399  pfxccatin12lem2  11423  seq3shft  11523  fzomaxdif  11798  climshft2  11991  iserex  12024  iser3shft  12031  serf0  12037  fsumm1  12102  fsumsplitsnun  12105  fsump1  12106  fsumshftm  12131  fisumrev2  12132  telfsumo  12152  fsumparts  12156  binomlem  12169  isumshft  12176  isumsplit  12177  isum1p  12178  divcnv  12183  arisum  12184  trireciplem  12186  cvgratnnlemmn  12211  cvgratnnlemsumlt  12214  mertenslemi1  12221  ntrivcvgap  12234  fprodm1  12284  fprodp1  12286  fprodfac  12301  fprodrev  12305  fprodmodd  12327  eirraplem  12463  moddvds  12485  dvdscmulr  12506  dvdsmulcr  12507  dvds2ln  12510  dvdsadd2b  12526  dvdsaddre2b  12527  fsumdvds  12528  fzocongeq  12544  addmodlteqALT  12545  dvdsexp  12547  dvdsmod  12548  mulmoddvds  12549  3dvds  12550  odd2np1  12559  oddm1even  12561  oexpneg  12563  mulsucdiv2z  12571  zob  12577  ltoddhalfle  12579  divalglemnn  12604  divalglemqt  12605  divalglemex  12608  divalglemeuneg  12609  divalgb  12611  divalgmod  12613  modremain  12615  flodddiv4  12622  bitsp1  12637  bitsfzo  12641  bitsmod  12642  bitsinv1lem  12647  dvdsbnd  12652  gcdaddm  12680  modgcd  12687  gcdmultipled  12689  dvdsgcdidd  12690  bezoutlemnewy  12692  bezoutlemaz  12699  bezoutlembz  12700  dvdsmulgcd  12721  rplpwr  12723  uzwodc  12733  lcmval  12760  lcmcllem  12764  lcmid  12777  mulgcddvds  12791  divgcdcoprm0  12798  cncongr1  12800  cncongr2  12801  rpexp  12850  sqrt2irrlem  12858  sqrt2irrap  12877  qmuldeneqnum  12892  numdensq  12899  qden1elz  12902  hashdvds  12918  phiprm  12920  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  fermltl  12931  prmdiv  12932  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  modprm0  12952  modprmn0modprm0  12954  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem15  12976  pcpremul  12991  pceulem  12992  pceu  12993  pczpre  12995  pcdiv  13000  pcqmul  13001  pcqdiv  13005  pcexp  13007  pcaddlem  13037  pcadd  13038  fldivp1  13046  pcfac  13048  pcbc  13049  prmpwdvds  13053  4sqlem5  13080  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqlemffi  13094  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem14  13102  4sqlem16  13104  4sqlem17  13105  znnen  13149  mulgsubcl  13853  mulgdirlem  13870  mulgdir  13871  mulgass  13876  mulgmodid  13878  mulgsubdir  13879  gsumfzconst  14058  gsumfzsnfd  14062  gsumsplit0  14063  zringmulg  14746  zndvds0  14798  znf1o  14799  znunit  14807  relogbexpap  15823  logbgcd1irraplemap  15834  wilthlem1  15848  lgslem1  15873  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsneg1  15898  lgsmod  15899  lgsdirprm  15907  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsabs1  15912  lgssq  15913  lgssq2  15914  lgsmulsqcoprm  15919  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem1  15934  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquadlem1  15950  lgsquad2lem1  15954  lgsquad3  15957  2lgslem1b  15962  2lgsoddprmlem2  15979  2sqlem3  15990  2sqlem4  15991  2sqlem8a  15995  2sqlem8  15996  clwwlkccatlem  16395  iswomni0  16836  gsumgfsumlem  16865  gsumgfsum  16866