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

Theorem zssre 12440
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 12437 . 2 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21ssriv 3947 1 ℤ ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3909  cr 10984  cz 12433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-neg 11322  df-z 12434
This theorem is referenced by:  suprzcl  12517  zred  12541  suprfinzcl  12551  uzssre  12719  uzwo2  12767  infssuzle  12786  infssuzcl  12787  lbzbi  12791  suprzub  12794  uzwo3  12798  rpnnen1lem3  12834  rpnnen1lem5  12836  fzval2  13357  flval3  13650  uzsup  13698  expcan  14002  ltexp2  14003  seqcoll  14292  limsupgre  15299  rlimclim  15364  isercolllem1  15485  isercolllem2  15486  isercoll  15488  caurcvg  15497  caucvg  15499  summolem2a  15536  summolem2  15537  zsum  15539  fsumcvg3  15550  climfsum  15641  prodmolem2a  15753  prodmolem2  15754  zprod  15756  1arith  16735  pgpssslw  19331  gsumval3  19619  zntoslem  20892  rzgrp  20956  zcld  24104  mbflimsup  24958  ig1pdvds  25469  aacjcl  25615  aalioulem3  25622  uzssico  31488  qqhre  32381  ballotlemfc0  32872  ballotlemfcc  32873  ballotlemiex  32881  erdszelem4  33568  erdszelem8  33572  supfz  34095  inffz  34096  poimirlem31  36040  poimirlem32  36041  irrapxlem1  41047  monotuz  41167  monotoddzzfi  41168  rmyeq0  41179  rmyeq  41180  lermy  41181  fzisoeu  43329  fzssre  43343  uzfissfz  43355  ssuzfz  43378  zssxr  43427  uzssre2  43437  uzred  43473  uzinico  43589  ioodvbdlimc1lem2  43964  ioodvbdlimc2lem  43966  dvnprodlem1  43978  fourierdlem25  44164  fourierdlem37  44176  fourierdlem52  44190  fourierdlem64  44202  fourierdlem79  44217  etransclem48  44314  hoicvr  44580
  Copyright terms: Public domain W3C validator