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

Theorem zssre 11220
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 11217 . 2 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21ssriv 3571 1 ℤ ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3539  cr 9792  cz 11213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-neg 10121  df-z 11214
This theorem is referenced by:  suprzcl  11292  zred  11317  suprfinzcl  11327  uzwo2  11587  infssuzle  11606  infssuzcl  11607  lbzbi  11611  suprzub  11614  uzwo3  11618  rpnnen1lem3  11651  rpnnen1lem5  11653  rpnnen1lem3OLD  11657  rpnnen1lem5OLD  11659  fzval2  12158  flval3  12436  uzsup  12482  expcan  12733  ltexp2  12734  seqcoll  13060  limsupgre  14009  rlimclim  14074  isercolllem1  14192  isercolllem2  14193  isercoll  14195  caurcvg  14204  caucvg  14206  summolem2a  14242  summolem2  14243  zsum  14245  fsumcvg3  14256  climfsum  14342  prodmolem2a  14452  prodmolem2  14453  zprod  14455  1arith  15418  pgpssslw  17801  gsumval3  18080  zntoslem  19672  zcld  22372  mbflimsup  23184  ig1pdvds  23685  aacjcl  23831  aalioulem3  23838  rzgrp  24049  qqhre  29226  ballotlemfc0  29715  ballotlemfcc  29716  ballotlemiex  29724  erdszelem4  30264  erdszelem8  30268  supfz  30700  inffz  30701  inffzOLD  30702  poimirlem31  32434  poimirlem32  32435  irrapxlem1  36228  monotuz  36348  monotoddzzfi  36349  rmyeq0  36362  rmyeq  36363  lermy  36364  fzisoeu  38279  fzssre  38294  uzfissfz  38307  ssuzfz  38330  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnprodlem1  38660  fourierdlem25  38849  fourierdlem37  38861  fourierdlem52  38875  fourierdlem64  38887  fourierdlem79  38902  etransclem48  38999  hoicvr  39262
  Copyright terms: Public domain W3C validator