Theorem zcnd 9581

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  ℤcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8102

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  qapne  9846  fzm1  10308  fzrevral  10313  fzshftral  10316  nn0disj  10346  fzoss2  10382  fzo0addelr  10407  elfzoext  10410  fzosubel  10412  fzosubel3  10414  fzocatel  10417  fzosplitsnm1  10427  infssuzex  10465  zsupssdc  10470  qtri3or  10472  exbtwnzlemstep  10479  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  flqaddz  10529  flqzadd  10530  2tnp1ge0ge0  10533  ceiqm1l  10545  intqfrac2  10553  intfracq  10554  flqdiv  10555  modqvalr  10559  flqpmodeq  10561  modq0  10563  mulqmod0  10564  modqlt  10567  modqdiffl  10569  modqfrac  10571  flqmod  10572  intqfrac  10573  modqmulnn  10576  modqvalp1  10577  modqcyc  10593  modqcyc2  10594  modqadd1  10595  mulqaddmodid  10598  mulp1mod1  10599  modqmul1  10611  modqmul12d  10612  modqnegd  10613  modqmulmodr  10624  modqdi  10626  modqsubdir  10627  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecfzen2  10661  uzennn  10670  uzsinds  10678  seq3shft2  10715  monoord2  10720  iseqf1olemab  10736  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seqf1oglem1  10753  seqf1oglem2  10754  expaddzaplem  10816  modqexp  10900  sqoddm1div8  10927  bcm1k  10994  bcp1nk  10996  bcpasc  11000  hashfz  11056  hashfzo  11057  hashfzp1  11059  seq3coll  11077  ccatval3  11147  ccatlid  11154  ccatass  11156  ccatalpha  11161  swrdfv0  11202  swrdfv2  11211  swrds1  11216  ccatswrd  11218  pfxfv  11232  ccatpfx  11249  swrdpfx  11255  pfxccatin12lem2  11279  seq3shft  11365  fzomaxdif  11640  climshft2  11833  iserex  11866  iser3shft  11873  serf0  11879  fsumm1  11943  fsumsplitsnun  11946  fsump1  11947  fsumshftm  11972  fisumrev2  11973  telfsumo  11993  fsumparts  11997  binomlem  12010  isumshft  12017  isumsplit  12018  isum1p  12019  divcnv  12024  arisum  12025  trireciplem  12027  cvgratnnlemmn  12052  cvgratnnlemsumlt  12055  mertenslemi1  12062  ntrivcvgap  12075  fprodm1  12125  fprodp1  12127  fprodfac  12142  fprodrev  12146  fprodmodd  12168  eirraplem  12304  moddvds  12326  dvdscmulr  12347  dvdsmulcr  12348  dvds2ln  12351  dvdsadd2b  12367  dvdsaddre2b  12368  fsumdvds  12369  fzocongeq  12385  addmodlteqALT  12386  dvdsexp  12388  dvdsmod  12389  mulmoddvds  12390  3dvds  12391  odd2np1  12400  oddm1even  12402  oexpneg  12404  mulsucdiv2z  12412  zob  12418  ltoddhalfle  12420  divalglemnn  12445  divalglemqt  12446  divalglemex  12449  divalglemeuneg  12450  divalgb  12452  divalgmod  12454  modremain  12456  flodddiv4  12463  bitsp1  12478  bitsfzo  12482  bitsmod  12483  bitsinv1lem  12488  dvdsbnd  12493  gcdaddm  12521  modgcd  12528  gcdmultipled  12530  dvdsgcdidd  12531  bezoutlemnewy  12533  bezoutlemaz  12540  bezoutlembz  12541  dvdsmulgcd  12562  rplpwr  12564  uzwodc  12574  lcmval  12601  lcmcllem  12605  lcmid  12618  mulgcddvds  12632  divgcdcoprm0  12639  cncongr1  12641  cncongr2  12642  rpexp  12691  sqrt2irrlem  12699  sqrt2irrap  12718  qmuldeneqnum  12733  numdensq  12740  qden1elz  12743  hashdvds  12759  phiprm  12761  eulerthlema  12768  eulerthlemh  12769  eulerthlemth  12770  fermltl  12772  prmdiv  12773  prmdiveq  12774  hashgcdlem  12776  odzdvds  12784  modprm0  12793  modprmn0modprm0  12795  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem15  12817  pcpremul  12832  pceulem  12833  pceu  12834  pczpre  12836  pcdiv  12841  pcqmul  12842  pcqdiv  12846  pcexp  12848  pcaddlem  12878  pcadd  12879  fldivp1  12887  pcfac  12889  pcbc  12890  prmpwdvds  12894  4sqlem5  12921  4sqlem8  12924  4sqlem9  12925  4sqlem10  12926  4sqlemffi  12935  4sqexercise2  12938  4sqlemsdc  12939  4sqlem11  12940  4sqlem14  12943  4sqlem16  12945  4sqlem17  12946  znnen  12985  mulgsubcl  13689  mulgdirlem  13706  mulgdir  13707  mulgass  13712  mulgmodid  13714  mulgsubdir  13715  gsumfzconst  13894  gsumfzsnfd  13898  zringmulg  14578  zndvds0  14630  znf1o  14631  znunit  14639  relogbexpap  15648  logbgcd1irraplemap  15659  wilthlem1  15670  lgslem1  15695  lgsval2lem  15705  lgsval4a  15717  lgsneg  15719  lgsneg1  15720  lgsmod  15721  lgsdirprm  15729  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsabs1  15734  lgssq  15735  lgssq2  15736  lgsmulsqcoprm  15741  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem1  15756  gausslemma2dlem4  15759  gausslemma2dlem5a  15760  gausslemma2dlem5  15761  gausslemma2dlem6  15762  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquad2lem1  15776  lgsquad3  15779  2lgslem1b  15784  2lgsoddprmlem2  15801  2sqlem3  15812  2sqlem4  15813  2sqlem8a  15817  2sqlem8  15818  clwwlkccatlem  16143  iswomni0  16507