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

Theorem zssre 10862
Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
zssre  |-  ZZ  C_  RR

Proof of Theorem zssre
StepHypRef Expression
1 zre 10859 . 2  |-  ( x  e.  ZZ  ->  x  e.  RR )
21ssriv 3503 1  |-  ZZ  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3471   RRcr 9482   ZZcz 10855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-neg 9799  df-z 10856
This theorem is referenced by:  suprzcl  10931  zred  10957  suprfinzcl  10966  uzwo2  11137  uzinfmi  11152  infmssuzle  11155  infmssuzcl  11156  lbzbi  11161  suprzub  11164  uzwo3  11168  rpnnen1lem3  11201  rpnnen1lem5  11203  fzval2  11666  flval3  11909  uzsup  11948  expcan  12175  ltexp2  12176  seqcoll  12467  limsupgre  13255  rlimclim  13320  isercolllem1  13438  isercolllem2  13439  isercoll  13441  caurcvg  13450  caucvg  13452  summolem2a  13488  summolem2  13489  zsum  13491  fsumcvg3  13502  climfsum  13585  1arith  14295  pgpssslw  16425  gsumval3OLD  16694  gsumval3  16697  zntoslem  18357  zcld  21048  mbflimsup  21803  ig1pdvds  22307  aacjcl  22452  aalioulem3  22459  qqhre  27622  ballotlemfc0  28059  ballotlemfcc  28060  ballotlemiex  28068  erdszelem4  28266  erdszelem8  28270  supfz  28570  inffz  28571  prodmolem2a  28631  prodmolem2  28632  zprod  28634  irrapxlem1  30351  monotuz  30470  monotoddzzfi  30471  rmyeq0  30484  rmyeq  30485  lermy  30486  fzisoeu  31034  ioodvbdlimc1lem2  31219  ioodvbdlimc2lem  31221  fourierdlem25  31389  fourierdlem37  31401  fourierdlem52  31416  fourierdlem79  31443
  Copyright terms: Public domain W3C validator