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

Theorem zssre 11608
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 11605 . 2 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21ssriv 3762 1 ℤ ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3729  cr 10158  cz 11601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rex 3070  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-iota 6005  df-fv 6050  df-ov 6815  df-neg 10492  df-z 11602
This theorem is referenced by:  suprzcl  11681  zred  11706  suprfinzcl  11716  uzwo2  11977  infssuzle  11996  infssuzcl  11997  lbzbi  12001  suprzub  12004  uzwo3  12008  rpnnen1lem3  12041  rpnnen1lem5  12043  fzval2  12558  flval3  12846  uzsup  12892  expcan  13142  ltexp2  13143  seqcoll  13472  limsupgre  14442  rlimclim  14507  isercolllem1  14625  isercolllem2  14626  isercoll  14628  caurcvg  14637  caucvg  14639  summolem2a  14676  summolem2  14677  zsum  14679  fsumcvg3  14690  climfsum  14781  prodmolem2a  14893  prodmolem2  14894  zprod  14896  1arith  15858  pgpssslw  18256  gsumval3  18535  zntoslem  20140  zcld  22856  mbflimsup  23674  ig1pdvds  24177  aacjcl  24323  aalioulem3  24330  rzgrp  24542  uzssico  29903  qqhre  30421  ballotlemfc0  30911  ballotlemfcc  30912  ballotlemiex  30920  erdszelem4  31531  erdszelem8  31535  supfz  31968  inffz  31969  inffzOLD  31970  poimirlem31  33790  poimirlem32  33791  irrapxlem1  37927  monotuz  38047  monotoddzzfi  38048  rmyeq0  38061  rmyeq  38062  lermy  38063  fzisoeu  40039  fzssre  40053  uzfissfz  40066  ssuzfz  40089  uzssre  40143  zssxr  40144  uzssre2  40156  uzred  40193  uzinico  40311  ioodvbdlimc1lem2  40671  ioodvbdlimc2lem  40673  dvnprodlem1  40685  fourierdlem25  40872  fourierdlem37  40884  fourierdlem52  40898  fourierdlem64  40910  fourierdlem79  40925  etransclem48  41022  hoicvr  41288
  Copyright terms: Public domain W3C validator