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

Theorem zssre 10896
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 10893 . 2
21ssriv 3507 1
Colors of variables: wff setvar class
Syntax hints:  C_wss 3475   cr 9512   cz 10889
This theorem is referenced by:  suprzcl  10967  zred  10994  suprfinzcl  11003  uzwo2  11175  uzinfmi  11190  infmssuzle  11193  infmssuzcl  11194  lbzbi  11199  suprzub  11202  uzwo3  11206  rpnnen1lem3  11239  rpnnen1lem5  11241  fzval2  11704  flval3  11951  uzsup  11990  expcan  12218  ltexp2  12219  seqcoll  12512  limsupgre  13304  rlimclim  13369  isercolllem1  13487  isercolllem2  13488  isercoll  13490  caurcvg  13499  caucvg  13501  summolem2a  13537  summolem2  13538  zsum  13540  fsumcvg3  13551  climfsum  13634  prodmolem2a  13741  prodmolem2  13742  zprod  13744  1arith  14445  pgpssslw  16634  gsumval3OLD  16908  gsumval3  16911  zntoslem  18595  zcld  21318  mbflimsup  22073  ig1pdvds  22577  aacjcl  22723  aalioulem3  22730  rzgrp  22941  qqhre  27998  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  erdszelem4  28638  erdszelem8  28642  supfz  29107  inffz  29108  irrapxlem1  30758  monotuz  30877  monotoddzzfi  30878  rmyeq0  30891  rmyeq  30892  lermy  30893  fzisoeu  31500  fzssre  31518  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem1  31743  fourierdlem25  31914  fourierdlem37  31926  fourierdlem52  31941  fourierdlem64  31953  fourierdlem79  31968  etransclem48  32065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator