Theorem zcnd 9393

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

Syntax hints:   → wi 4   ∈ wcel 2159  ℂcc 7826  ℤcz 9270

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170  ax-resscn 7920

This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-rex 2473  df-rab 2476  df-v 2753  df-un 3147  df-in 3149  df-ss 3156  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-br 4018  df-iota 5192  df-fv 5238  df-ov 5893  df-neg 8148  df-z 9271

This theorem is referenced by:  qapne  9656  fzm1  10117  fzrevral  10122  fzshftral  10125  nn0disj  10155  fzoss2  10189  fzosubel  10211  fzosubel3  10213  fzocatel  10216  fzosplitsnm1  10226  qtri3or  10260  exbtwnzlemstep  10265  exbtwnzlemex  10267  rebtwn2zlemstep  10270  rebtwn2z  10272  flqaddz  10314  flqzadd  10315  2tnp1ge0ge0  10318  ceiqm1l  10328  intqfrac2  10336  intfracq  10337  flqdiv  10338  modqvalr  10342  flqpmodeq  10344  modq0  10346  mulqmod0  10347  modqlt  10350  modqdiffl  10352  modqfrac  10354  flqmod  10355  intqfrac  10356  modqmulnn  10359  modqvalp1  10360  modqcyc  10376  modqcyc2  10377  modqadd1  10378  mulqaddmodid  10381  mulp1mod1  10382  modqmul1  10394  modqmul12d  10395  modqnegd  10396  modqmulmodr  10407  modqdi  10409  modqsubdir  10410  modfzo0difsn  10412  modsumfzodifsn  10413  addmodlteq  10415  frecfzen2  10444  uzennn  10453  uzsinds  10459  seq3shft2  10490  monoord2  10494  iseqf1olemab  10506  seq3f1olemqsumkj  10515  seq3f1olemqsum  10517  expaddzaplem  10580  modqexp  10664  sqoddm1div8  10691  bcm1k  10757  bcp1nk  10759  bcpasc  10763  hashfz  10818  hashfzo  10819  hashfzp1  10821  seq3coll  10839  seq3shft  10864  fzomaxdif  11139  climshft2  11331  iserex  11364  iser3shft  11371  serf0  11377  fsumm1  11441  fsumsplitsnun  11444  fsump1  11445  fsumshftm  11470  fisumrev2  11471  telfsumo  11491  fsumparts  11495  binomlem  11508  isumshft  11515  isumsplit  11516  isum1p  11517  divcnv  11522  arisum  11523  trireciplem  11525  cvgratnnlemmn  11550  cvgratnnlemsumlt  11553  mertenslemi1  11560  ntrivcvgap  11573  fprodm1  11623  fprodp1  11625  fprodfac  11640  fprodrev  11644  fprodmodd  11666  eirraplem  11801  moddvds  11823  dvdscmulr  11844  dvdsmulcr  11845  dvds2ln  11848  dvdsadd2b  11864  dvdsaddre2b  11865  fzocongeq  11881  addmodlteqALT  11882  dvdsexp  11884  dvdsmod  11885  mulmoddvds  11886  odd2np1  11895  oddm1even  11897  oexpneg  11899  mulsucdiv2z  11907  zob  11913  ltoddhalfle  11915  divalglemnn  11940  divalglemqt  11941  divalglemex  11944  divalglemeuneg  11945  divalgb  11947  divalgmod  11949  modremain  11951  flodddiv4  11956  infssuzex  11967  zsupssdc  11972  dvdsbnd  11974  gcdaddm  12002  modgcd  12009  gcdmultipled  12011  dvdsgcdidd  12012  bezoutlemnewy  12014  bezoutlemaz  12021  bezoutlembz  12022  dvdsmulgcd  12043  rplpwr  12045  uzwodc  12055  lcmval  12080  lcmcllem  12084  lcmid  12097  mulgcddvds  12111  divgcdcoprm0  12118  cncongr1  12120  cncongr2  12121  rpexp  12170  sqrt2irrlem  12178  sqrt2irrap  12197  qmuldeneqnum  12212  numdensq  12219  qden1elz  12222  hashdvds  12238  phiprm  12240  eulerthlema  12247  eulerthlemh  12248  eulerthlemth  12249  fermltl  12251  prmdiv  12252  prmdiveq  12253  hashgcdlem  12255  odzdvds  12262  modprm0  12271  modprmn0modprm0  12273  pythagtriplem6  12287  pythagtriplem7  12288  pythagtriplem15  12295  pcpremul  12310  pceulem  12311  pceu  12312  pczpre  12314  pcdiv  12319  pcqmul  12320  pcqdiv  12324  pcexp  12326  pcaddlem  12355  pcadd  12356  fldivp1  12363  pcfac  12365  pcbc  12366  prmpwdvds  12370  4sqlem5  12397  4sqlem8  12400  4sqlem9  12401  4sqlem10  12402  znnen  12416  mulgsubcl  13041  mulgdirlem  13058  mulgdir  13059  mulgass  13064  mulgmodid  13066  mulgsubdir  13067  zringmulg  13857  relogbexpap  14759  logbgcd1irraplemap  14770  lgslem1  14784  lgsval2lem  14794  lgsval4a  14806  lgsneg  14808  lgsneg1  14809  lgsmod  14810  lgsdirprm  14818  lgsdir  14819  lgsdilem2  14820  lgsdi  14821  lgsne0  14822  lgsabs1  14823  lgssq  14824  lgssq2  14825  lgsmulsqcoprm  14830  lgsdirnn0  14831  lgsdinn0  14832  lgseisenlem1  14833  lgseisenlem2  14834  2lgsoddprmlem2  14837  2sqlem3  14847  2sqlem4  14848  2sqlem8a  14852  2sqlem8  14853  iswomni0  15183