Theorem zssre 11991

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

Syntax hints:   ⊆ wss 3939  ℝcr 10539  ℤcz 11984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876  df-z 11985

This theorem is referenced by:  suprzcl  12065  zred  12090  suprfinzcl  12100  uzwo2  12315  infssuzle  12334  infssuzcl  12335  lbzbi  12339  suprzub  12342  uzwo3  12346  rpnnen1lem3  12381  rpnnen1lem5  12383  fzval2  12898  flval3  13188  uzsup  13234  expcan  13536  ltexp2  13537  seqcoll  13825  limsupgre  14841  rlimclim  14906  isercolllem1  15024  isercolllem2  15025  isercoll  15027  caurcvg  15036  caucvg  15038  summolem2a  15075  summolem2  15076  zsum  15078  fsumcvg3  15089  climfsum  15178  prodmolem2a  15291  prodmolem2  15292  zprod  15294  1arith  16266  pgpssslw  18742  gsumval3  19030  zntoslem  20706  rzgrp  20770  zcld  23424  mbflimsup  24270  ig1pdvds  24773  aacjcl  24919  aalioulem3  24926  uzssico  30510  qqhre  31265  ballotlemfc0  31754  ballotlemfcc  31755  ballotlemiex  31763  erdszelem4  32445  erdszelem8  32449  supfz  32964  inffz  32965  poimirlem31  34927  poimirlem32  34928  irrapxlem1  39425  monotuz  39544  monotoddzzfi  39545  rmyeq0  39556  rmyeq  39557  lermy  39558  fzisoeu  41573  fzssre  41587  uzfissfz  41600  ssuzfz  41623  uzssre  41675  zssxr  41676  uzssre2  41686  uzred  41723  uzinico  41842  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnprodlem1  42237  fourierdlem25  42424  fourierdlem37  42436  fourierdlem52  42450  fourierdlem64  42462  fourierdlem79  42477  etransclem48  42574  hoicvr  42837