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

Theorem zssre 11596
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 11593 . 2 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
21ssriv 3748 1 ℤ ⊆ ℝ
Colors of variables: wff setvar class
Syntax hints:  wss 3715  cr 10147  cz 11589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-neg 10481  df-z 11590
This theorem is referenced by:  suprzcl  11669  zred  11694  suprfinzcl  11704  uzwo2  11965  infssuzle  11984  infssuzcl  11985  lbzbi  11989  suprzub  11992  uzwo3  11996  rpnnen1lem3  12029  rpnnen1lem5  12031  rpnnen1lem3OLD  12035  rpnnen1lem5OLD  12037  fzval2  12542  flval3  12830  uzsup  12876  expcan  13127  ltexp2  13128  seqcoll  13460  limsupgre  14431  rlimclim  14496  isercolllem1  14614  isercolllem2  14615  isercoll  14617  caurcvg  14626  caucvg  14628  summolem2a  14665  summolem2  14666  zsum  14668  fsumcvg3  14679  climfsum  14771  prodmolem2a  14883  prodmolem2  14884  zprod  14886  1arith  15853  pgpssslw  18249  gsumval3  18528  zntoslem  20127  zcld  22837  mbflimsup  23652  ig1pdvds  24155  aacjcl  24301  aalioulem3  24308  rzgrp  24520  uzssico  29876  qqhre  30394  ballotlemfc0  30884  ballotlemfcc  30885  ballotlemiex  30893  erdszelem4  31504  erdszelem8  31508  supfz  31941  inffz  31942  inffzOLD  31943  poimirlem31  33771  poimirlem32  33772  irrapxlem1  37906  monotuz  38026  monotoddzzfi  38027  rmyeq0  38040  rmyeq  38041  lermy  38042  fzisoeu  40031  fzssre  40045  uzfissfz  40058  ssuzfz  40081  uzssre  40136  zssxr  40137  uzssre2  40149  uzred  40186  uzinico  40308  ioodvbdlimc1lem2  40668  ioodvbdlimc2lem  40670  dvnprodlem1  40682  fourierdlem25  40870  fourierdlem37  40882  fourierdlem52  40896  fourierdlem64  40908  fourierdlem79  40923  etransclem48  41020  hoicvr  41286
  Copyright terms: Public domain W3C validator