Theorem zcnd 9496

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

Syntax hints:   → wi 4   ∈ wcel 2176  ℂcc 7923  ℤcz 9372

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373

This theorem is referenced by:  qapne  9760  fzm1  10222  fzrevral  10227  fzshftral  10230  nn0disj  10260  fzoss2  10296  fzo0addelr  10318  elfzoext  10321  fzosubel  10323  fzosubel3  10325  fzocatel  10328  fzosplitsnm1  10338  infssuzex  10376  zsupssdc  10381  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemex  10392  rebtwn2zlemstep  10395  rebtwn2z  10397  flqaddz  10440  flqzadd  10441  2tnp1ge0ge0  10444  ceiqm1l  10456  intqfrac2  10464  intfracq  10465  flqdiv  10466  modqvalr  10470  flqpmodeq  10472  modq0  10474  mulqmod0  10475  modqlt  10478  modqdiffl  10480  modqfrac  10482  flqmod  10483  intqfrac  10484  modqmulnn  10487  modqvalp1  10488  modqcyc  10504  modqcyc2  10505  modqadd1  10506  mulqaddmodid  10509  mulp1mod1  10510  modqmul1  10522  modqmul12d  10523  modqnegd  10524  modqmulmodr  10535  modqdi  10537  modqsubdir  10538  modfzo0difsn  10540  modsumfzodifsn  10541  addmodlteq  10543  frecfzen2  10572  uzennn  10581  uzsinds  10589  seq3shft2  10626  monoord2  10631  iseqf1olemab  10647  seq3f1olemqsumkj  10656  seq3f1olemqsum  10658  seqf1oglem1  10664  seqf1oglem2  10665  expaddzaplem  10727  modqexp  10811  sqoddm1div8  10838  bcm1k  10905  bcp1nk  10907  bcpasc  10911  hashfz  10966  hashfzo  10967  hashfzp1  10969  seq3coll  10987  ccatval3  11055  ccatlid  11062  ccatass  11064  swrdfv0  11107  swrdfv2  11116  swrds1  11121  ccatswrd  11123  seq3shft  11149  fzomaxdif  11424  climshft2  11617  iserex  11650  iser3shft  11657  serf0  11663  fsumm1  11727  fsumsplitsnun  11730  fsump1  11731  fsumshftm  11756  fisumrev2  11757  telfsumo  11777  fsumparts  11781  binomlem  11794  isumshft  11801  isumsplit  11802  isum1p  11803  divcnv  11808  arisum  11809  trireciplem  11811  cvgratnnlemmn  11836  cvgratnnlemsumlt  11839  mertenslemi1  11846  ntrivcvgap  11859  fprodm1  11909  fprodp1  11911  fprodfac  11926  fprodrev  11930  fprodmodd  11952  eirraplem  12088  moddvds  12110  dvdscmulr  12131  dvdsmulcr  12132  dvds2ln  12135  dvdsadd2b  12151  dvdsaddre2b  12152  fsumdvds  12153  fzocongeq  12169  addmodlteqALT  12170  dvdsexp  12172  dvdsmod  12173  mulmoddvds  12174  3dvds  12175  odd2np1  12184  oddm1even  12186  oexpneg  12188  mulsucdiv2z  12196  zob  12202  ltoddhalfle  12204  divalglemnn  12229  divalglemqt  12230  divalglemex  12233  divalglemeuneg  12234  divalgb  12236  divalgmod  12238  modremain  12240  flodddiv4  12247  bitsp1  12262  bitsfzo  12266  bitsmod  12267  bitsinv1lem  12272  dvdsbnd  12277  gcdaddm  12305  modgcd  12312  gcdmultipled  12314  dvdsgcdidd  12315  bezoutlemnewy  12317  bezoutlemaz  12324  bezoutlembz  12325  dvdsmulgcd  12346  rplpwr  12348  uzwodc  12358  lcmval  12385  lcmcllem  12389  lcmid  12402  mulgcddvds  12416  divgcdcoprm0  12423  cncongr1  12425  cncongr2  12426  rpexp  12475  sqrt2irrlem  12483  sqrt2irrap  12502  qmuldeneqnum  12517  numdensq  12524  qden1elz  12527  hashdvds  12543  phiprm  12545  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  fermltl  12556  prmdiv  12557  prmdiveq  12558  hashgcdlem  12560  odzdvds  12568  modprm0  12577  modprmn0modprm0  12579  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem15  12601  pcpremul  12616  pceulem  12617  pceu  12618  pczpre  12620  pcdiv  12625  pcqmul  12626  pcqdiv  12630  pcexp  12632  pcaddlem  12662  pcadd  12663  fldivp1  12671  pcfac  12673  pcbc  12674  prmpwdvds  12678  4sqlem5  12705  4sqlem8  12708  4sqlem9  12709  4sqlem10  12710  4sqlemffi  12719  4sqexercise2  12722  4sqlemsdc  12723  4sqlem11  12724  4sqlem14  12727  4sqlem16  12729  4sqlem17  12730  znnen  12769  mulgsubcl  13472  mulgdirlem  13489  mulgdir  13490  mulgass  13495  mulgmodid  13497  mulgsubdir  13498  gsumfzconst  13677  gsumfzsnfd  13681  zringmulg  14360  zndvds0  14412  znf1o  14413  znunit  14421  relogbexpap  15430  logbgcd1irraplemap  15441  wilthlem1  15452  lgslem1  15477  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsneg1  15502  lgsmod  15503  lgsdirprm  15511  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsabs1  15516  lgssq  15517  lgssq2  15518  lgsmulsqcoprm  15523  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem1  15538  gausslemma2dlem4  15541  gausslemma2dlem5a  15542  gausslemma2dlem5  15543  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquad2lem1  15558  lgsquad3  15561  2lgslem1b  15566  2lgsoddprmlem2  15583  2sqlem3  15594  2sqlem4  15595  2sqlem8a  15599  2sqlem8  15600  iswomni0  15990