MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zssre Structured version   Visualization version   GIF version

Theorem zssre 11977
Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
zssre ℤ ⊆ ℝ

Proof of Theorem zssre
StepHypRef Expression
1 zre 11974 . 2 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21ssriv 3975 1 ℤ ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3940  cr 10525  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360  df-ov 7151  df-neg 10862  df-z 11971
This theorem is referenced by:  suprzcl  12051  zred  12076  suprfinzcl  12086  uzwo2  12301  infssuzle  12320  infssuzcl  12321  lbzbi  12325  suprzub  12328  uzwo3  12332  rpnnen1lem3  12368  rpnnen1lem5  12370  fzval2  12885  flval3  13175  uzsup  13221  expcan  13523  ltexp2  13524  seqcoll  13812  limsupgre  14828  rlimclim  14893  isercolllem1  15011  isercolllem2  15012  isercoll  15014  caurcvg  15023  caucvg  15025  summolem2a  15062  summolem2  15063  zsum  15065  fsumcvg3  15076  climfsum  15165  prodmolem2a  15278  prodmolem2  15279  zprod  15281  1arith  16253  pgpssslw  18659  gsumval3  18947  zntoslem  20619  rzgrp  20683  zcld  23336  mbflimsup  24182  ig1pdvds  24685  aacjcl  24831  aalioulem3  24838  uzssico  30420  qqhre  31147  ballotlemfc0  31636  ballotlemfcc  31637  ballotlemiex  31645  erdszelem4  32325  erdszelem8  32329  supfz  32844  inffz  32845  poimirlem31  34790  poimirlem32  34791  irrapxlem1  39284  monotuz  39403  monotoddzzfi  39404  rmyeq0  39415  rmyeq  39416  lermy  39417  fzisoeu  41432  fzssre  41446  uzfissfz  41459  ssuzfz  41482  uzssre  41534  zssxr  41535  uzssre2  41545  uzred  41582  uzinico  41701  ioodvbdlimc1lem2  42082  ioodvbdlimc2lem  42084  dvnprodlem1  42096  fourierdlem25  42283  fourierdlem37  42295  fourierdlem52  42309  fourierdlem64  42321  fourierdlem79  42336  etransclem48  42433  hoicvr  42696
  Copyright terms: Public domain W3C validator