Theorem zcnd 9310

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7747  ℤcz 9187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-rab 2452  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188

This theorem is referenced by:  qapne  9573  fzm1  10031  fzrevral  10036  fzshftral  10039  nn0disj  10069  fzoss2  10103  fzosubel  10125  fzosubel3  10127  fzocatel  10130  fzosplitsnm1  10140  qtri3or  10174  exbtwnzlemstep  10179  exbtwnzlemex  10181  rebtwn2zlemstep  10184  rebtwn2z  10186  flqaddz  10228  flqzadd  10229  2tnp1ge0ge0  10232  ceiqm1l  10242  intqfrac2  10250  intfracq  10251  flqdiv  10252  modqvalr  10256  flqpmodeq  10258  modq0  10260  mulqmod0  10261  modqlt  10264  modqdiffl  10266  modqfrac  10268  flqmod  10269  intqfrac  10270  modqmulnn  10273  modqvalp1  10274  modqcyc  10290  modqcyc2  10291  modqadd1  10292  mulqaddmodid  10295  mulp1mod1  10296  modqmul1  10308  modqmul12d  10309  modqnegd  10310  modqmulmodr  10321  modqdi  10323  modqsubdir  10324  modfzo0difsn  10326  modsumfzodifsn  10327  addmodlteq  10329  frecfzen2  10358  uzennn  10367  uzsinds  10373  seq3shft2  10404  monoord2  10408  iseqf1olemab  10420  seq3f1olemqsumkj  10429  seq3f1olemqsum  10431  expaddzaplem  10494  modqexp  10577  sqoddm1div8  10604  bcm1k  10669  bcp1nk  10671  bcpasc  10675  hashfz  10730  hashfzo  10731  hashfzp1  10733  seq3coll  10751  seq3shft  10776  fzomaxdif  11051  climshft2  11243  iserex  11276  iser3shft  11283  serf0  11289  fsumm1  11353  fsumsplitsnun  11356  fsump1  11357  fsumshftm  11382  fisumrev2  11383  telfsumo  11403  fsumparts  11407  binomlem  11420  isumshft  11427  isumsplit  11428  isum1p  11429  divcnv  11434  arisum  11435  trireciplem  11437  cvgratnnlemmn  11462  cvgratnnlemsumlt  11465  mertenslemi1  11472  ntrivcvgap  11485  fprodm1  11535  fprodp1  11537  fprodfac  11552  fprodrev  11556  fprodmodd  11578  eirraplem  11713  moddvds  11735  dvdscmulr  11756  dvdsmulcr  11757  dvds2ln  11760  dvdsadd2b  11776  fzocongeq  11792  addmodlteqALT  11793  dvdsexp  11795  dvdsmod  11796  mulmoddvds  11797  odd2np1  11806  oddm1even  11808  oexpneg  11810  mulsucdiv2z  11818  zob  11824  ltoddhalfle  11826  divalglemnn  11851  divalglemqt  11852  divalglemex  11855  divalglemeuneg  11856  divalgb  11858  divalgmod  11860  modremain  11862  flodddiv4  11867  infssuzex  11878  zsupssdc  11883  dvdsbnd  11885  gcdaddm  11913  modgcd  11920  gcdmultipled  11922  dvdsgcdidd  11923  bezoutlemnewy  11925  bezoutlemaz  11932  bezoutlembz  11933  dvdsmulgcd  11954  rplpwr  11956  uzwodc  11966  lcmval  11991  lcmcllem  11995  lcmid  12008  mulgcddvds  12022  divgcdcoprm0  12029  cncongr1  12031  cncongr2  12032  rpexp  12081  sqrt2irrlem  12089  sqrt2irrap  12108  qmuldeneqnum  12123  numdensq  12130  qden1elz  12133  hashdvds  12149  phiprm  12151  eulerthlema  12158  eulerthlemh  12159  eulerthlemth  12160  fermltl  12162  prmdiv  12163  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  modprm0  12182  modprmn0modprm0  12184  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem15  12206  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pcdiv  12230  pcqmul  12231  pcqdiv  12235  pcexp  12237  pcaddlem  12266  pcadd  12267  fldivp1  12274  pcfac  12276  pcbc  12277  prmpwdvds  12281  4sqlem5  12308  4sqlem8  12311  4sqlem9  12312  4sqlem10  12313  znnen  12327  relogbexpap  13476  logbgcd1irraplemap  13487  lgslem1  13501  lgsval2lem  13511  lgsval4a  13523  lgsneg  13525  lgsneg1  13526  lgsmod  13527  lgsdirprm  13535  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsabs1  13540  lgssq  13541  lgssq2  13542  lgsmulsqcoprm  13547  lgsdirnn0  13548  lgsdinn0  13549  2sqlem3  13553  2sqlem4  13554  2sqlem8a  13558  2sqlem8  13559  iswomni0  13890