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

Theorem zssre 10941
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 10938 . 2  |-  ( x  e.  ZZ  ->  x  e.  RR )
21ssriv 3435 1  |-  ZZ  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3403   RRcr 9535   ZZcz 10934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-br 4402  df-iota 5545  df-fv 5589  df-ov 6291  df-neg 9860  df-z 10935
This theorem is referenced by:  suprzcl  11012  zred  11037  suprfinzcl  11047  uzwo2  11220  uzinfmiOLD  11236  infssuzle  11241  infssuzcl  11242  infmssuzleOLD  11243  infmssuzclOLD  11244  lbzbi  11249  suprzub  11252  uzwo3  11256  rpnnen1lem3  11289  rpnnen1lem5  11291  fzval2  11784  flval3  12047  uzsup  12087  expcan  12322  ltexp2  12323  seqcoll  12624  limsupgre  13535  limsupgreOLD  13536  rlimclim  13603  isercolllem1  13721  isercolllem2  13722  isercoll  13724  caurcvg  13735  caurcvgOLD  13736  caucvg  13738  summolem2a  13774  summolem2  13775  zsum  13777  fsumcvg3  13788  climfsum  13873  prodmolem2a  13981  prodmolem2  13982  zprod  13984  1arith  14864  pgpssslw  17259  gsumval3  17534  zntoslem  19120  zcld  21824  mbflimsup  22616  mbflimsupOLD  22617  ig1pdvds  23121  ig1pdvdsOLD  23127  aacjcl  23276  aalioulem3  23283  rzgrp  23496  qqhre  28817  ballotlemfc0  29318  ballotlemfcc  29319  ballotlemiex  29327  ballotlemiexOLD  29365  erdszelem4  29910  erdszelem8  29914  supfz  30355  inffz  30356  poimirlem31  31964  poimirlem32  31965  irrapxlem1  35660  monotuz  35783  monotoddzzfi  35784  rmyeq0  35797  rmyeq  35798  lermy  35799  fzisoeu  37512  fzssre  37529  uzfissfz  37543  ssuzfz  37566  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvnprodlem1  37815  fourierdlem25  37988  fourierdlem37  38001  fourierdlem52  38016  fourierdlem64  38028  fourierdlem79  38043  etransclem48OLD  38141  etransclem48  38142  hoicvr  38364
  Copyright terms: Public domain W3C validator