Theorem zssre 12589

Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
zssre	⊢ ℤ ⊆ ℝ

Proof of Theorem zssre

Step	Hyp	Ref	Expression
1		zre 12586	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
2	1	ssriv 3943	1 ⊢ ℤ ⊆ ℝ

Syntax hints:   ⊆ wss 3907  ℝcr 11087  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432  df-z 12583

This theorem is referenced by:  suprzcl  12667  zred  12691  suprfinzcl  12701  uzssre  12875  uzwo2  12927  infssuzle  12946  infssuzcl  12947  lbzbi  12951  suprzub  12954  uzwo3  12958  rpnnen1lem3  12994  rpnnen1lem5  12996  fzval2  13529  flval3  13839  uzsup  13887  expcan  14196  ltexp2  14197  seqcoll  14491  limsupgre  15522  rlimclim  15587  isercolllem1  15706  isercolllem2  15707  isercoll  15709  caurcvg  15718  caucvg  15720  summolem2a  15756  summolem2  15757  zsum  15759  fsumcvg3  15770  climfsum  15862  prodmolem2a  15978  prodmolem2  15979  zprod  15981  1arith  16977  pgpssslw  19675  gsumval3  19968  zntoslem  21666  rzgrp  21733  zcld  24932  mbflimsup  25786  ig1pdvds  26298  aacjcl  26449  aalioulem3  26456  uzssico  33041  qqhre  34327  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemiex  34809  erdszelem4  35557  erdszelem8  35561  supfz  36092  inffz  36093  poimirlem31  38162  poimirlem32  38163  irrapxlem1  43411  monotuz  43530  monotoddzzfi  43531  rmyeq0  43542  rmyeq  43543  lermy  43544  fzisoeu  45877  fzssre  45891  uzfissfz  45900  ssuzfz  45923  zssxr  45970  uzssre2  45979  uzred  46015  uzinico  46133  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  fourierdlem25  46704  fourierdlem37  46716  fourierdlem52  46730  fourierdlem64  46742  fourierdlem79  46757  etransclem48  46854  chnsuslle  47455