Theorem zcnd 9466

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℤcz 9343

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7988

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8217  df-z 9344

This theorem is referenced by:  qapne  9730  fzm1  10192  fzrevral  10197  fzshftral  10200  nn0disj  10230  fzoss2  10265  fzosubel  10287  fzosubel3  10289  fzocatel  10292  fzosplitsnm1  10302  infssuzex  10340  zsupssdc  10345  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemex  10356  rebtwn2zlemstep  10359  rebtwn2z  10361  flqaddz  10404  flqzadd  10405  2tnp1ge0ge0  10408  ceiqm1l  10420  intqfrac2  10428  intfracq  10429  flqdiv  10430  modqvalr  10434  flqpmodeq  10436  modq0  10438  mulqmod0  10439  modqlt  10442  modqdiffl  10444  modqfrac  10446  flqmod  10447  intqfrac  10448  modqmulnn  10451  modqvalp1  10452  modqcyc  10468  modqcyc2  10469  modqadd1  10470  mulqaddmodid  10473  mulp1mod1  10474  modqmul1  10486  modqmul12d  10487  modqnegd  10488  modqmulmodr  10499  modqdi  10501  modqsubdir  10502  modfzo0difsn  10504  modsumfzodifsn  10505  addmodlteq  10507  frecfzen2  10536  uzennn  10545  uzsinds  10553  seq3shft2  10590  monoord2  10595  iseqf1olemab  10611  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seqf1oglem1  10628  seqf1oglem2  10629  expaddzaplem  10691  modqexp  10775  sqoddm1div8  10802  bcm1k  10869  bcp1nk  10871  bcpasc  10875  hashfz  10930  hashfzo  10931  hashfzp1  10933  seq3coll  10951  seq3shft  11020  fzomaxdif  11295  climshft2  11488  iserex  11521  iser3shft  11528  serf0  11534  fsumm1  11598  fsumsplitsnun  11601  fsump1  11602  fsumshftm  11627  fisumrev2  11628  telfsumo  11648  fsumparts  11652  binomlem  11665  isumshft  11672  isumsplit  11673  isum1p  11674  divcnv  11679  arisum  11680  trireciplem  11682  cvgratnnlemmn  11707  cvgratnnlemsumlt  11710  mertenslemi1  11717  ntrivcvgap  11730  fprodm1  11780  fprodp1  11782  fprodfac  11797  fprodrev  11801  fprodmodd  11823  eirraplem  11959  moddvds  11981  dvdscmulr  12002  dvdsmulcr  12003  dvds2ln  12006  dvdsadd2b  12022  dvdsaddre2b  12023  fsumdvds  12024  fzocongeq  12040  addmodlteqALT  12041  dvdsexp  12043  dvdsmod  12044  mulmoddvds  12045  3dvds  12046  odd2np1  12055  oddm1even  12057  oexpneg  12059  mulsucdiv2z  12067  zob  12073  ltoddhalfle  12075  divalglemnn  12100  divalglemqt  12101  divalglemex  12104  divalglemeuneg  12105  divalgb  12107  divalgmod  12109  modremain  12111  flodddiv4  12118  bitsp1  12133  bitsfzo  12137  bitsmod  12138  bitsinv1lem  12143  dvdsbnd  12148  gcdaddm  12176  modgcd  12183  gcdmultipled  12185  dvdsgcdidd  12186  bezoutlemnewy  12188  bezoutlemaz  12195  bezoutlembz  12196  dvdsmulgcd  12217  rplpwr  12219  uzwodc  12229  lcmval  12256  lcmcllem  12260  lcmid  12273  mulgcddvds  12287  divgcdcoprm0  12294  cncongr1  12296  cncongr2  12297  rpexp  12346  sqrt2irrlem  12354  sqrt2irrap  12373  qmuldeneqnum  12388  numdensq  12395  qden1elz  12398  hashdvds  12414  phiprm  12416  eulerthlema  12423  eulerthlemh  12424  eulerthlemth  12425  fermltl  12427  prmdiv  12428  prmdiveq  12429  hashgcdlem  12431  odzdvds  12439  modprm0  12448  modprmn0modprm0  12450  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem15  12472  pcpremul  12487  pceulem  12488  pceu  12489  pczpre  12491  pcdiv  12496  pcqmul  12497  pcqdiv  12501  pcexp  12503  pcaddlem  12533  pcadd  12534  fldivp1  12542  pcfac  12544  pcbc  12545  prmpwdvds  12549  4sqlem5  12576  4sqlem8  12579  4sqlem9  12580  4sqlem10  12581  4sqlemffi  12590  4sqexercise2  12593  4sqlemsdc  12594  4sqlem11  12595  4sqlem14  12598  4sqlem16  12600  4sqlem17  12601  znnen  12640  mulgsubcl  13342  mulgdirlem  13359  mulgdir  13360  mulgass  13365  mulgmodid  13367  mulgsubdir  13368  gsumfzconst  13547  gsumfzsnfd  13551  zringmulg  14230  zndvds0  14282  znf1o  14283  znunit  14291  relogbexpap  15278  logbgcd1irraplemap  15289  wilthlem1  15300  lgslem1  15325  lgsval2lem  15335  lgsval4a  15347  lgsneg  15349  lgsneg1  15350  lgsmod  15351  lgsdirprm  15359  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgsabs1  15364  lgssq  15365  lgssq2  15366  lgsmulsqcoprm  15371  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem1  15386  gausslemma2dlem4  15389  gausslemma2dlem5a  15390  gausslemma2dlem5  15391  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquad2lem1  15406  lgsquad3  15409  2lgslem1b  15414  2lgsoddprmlem2  15431  2sqlem3  15442  2sqlem4  15443  2sqlem8a  15447  2sqlem8  15448  iswomni0  15782