Theorem zssre 11976

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 11973	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
2	1	ssriv 3919	1 ⊢ ℤ ⊆ ℝ

Syntax hints:   ⊆ wss 3881  ℝcr 10525  ℤcz 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  suprzcl  12050  zred  12075  suprfinzcl  12085  uzwo2  12300  infssuzle  12319  infssuzcl  12320  lbzbi  12324  suprzub  12327  uzwo3  12331  rpnnen1lem3  12366  rpnnen1lem5  12368  fzval2  12888  flval3  13180  uzsup  13226  expcan  13529  ltexp2  13530  seqcoll  13818  limsupgre  14830  rlimclim  14895  isercolllem1  15013  isercolllem2  15014  isercoll  15016  caurcvg  15025  caucvg  15027  summolem2a  15064  summolem2  15065  zsum  15067  fsumcvg3  15078  climfsum  15167  prodmolem2a  15280  prodmolem2  15281  zprod  15283  1arith  16253  pgpssslw  18731  gsumval3  19020  zntoslem  20248  rzgrp  20312  zcld  23418  mbflimsup  24270  ig1pdvds  24777  aacjcl  24923  aalioulem3  24930  uzssico  30533  qqhre  31371  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemiex  31869  erdszelem4  32554  erdszelem8  32558  supfz  33073  inffz  33074  poimirlem31  35088  poimirlem32  35089  irrapxlem1  39763  monotuz  39882  monotoddzzfi  39883  rmyeq0  39894  rmyeq  39895  lermy  39896  fzisoeu  41932  fzssre  41946  uzfissfz  41958  ssuzfz  41981  uzssre  42033  zssxr  42034  uzssre2  42044  uzred  42080  uzinico  42197  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnprodlem1  42588  fourierdlem25  42774  fourierdlem37  42786  fourierdlem52  42800  fourierdlem64  42812  fourierdlem79  42827  etransclem48  42924  hoicvr  43187