Theorem zssre 12183

Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
zssre	⊢ ℤ ⊆ ℝ

Proof of Theorem zssre

Step	Hyp	Ref	Expression
1		zre 12180	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
2	1	ssriv 3905	1 ⊢ ℤ ⊆ ℝ

Syntax hints:   ⊆ wss 3866  ℝcr 10728  ℤcz 12176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388  df-ov 7216  df-neg 11065  df-z 12177

This theorem is referenced by:  suprzcl  12257  zred  12282  suprfinzcl  12292  uzssre  12460  uzwo2  12508  infssuzle  12527  infssuzcl  12528  lbzbi  12532  suprzub  12535  uzwo3  12539  rpnnen1lem3  12575  rpnnen1lem5  12577  fzval2  13098  flval3  13390  uzsup  13436  expcan  13739  ltexp2  13740  seqcoll  14030  limsupgre  15042  rlimclim  15107  isercolllem1  15228  isercolllem2  15229  isercoll  15231  caurcvg  15240  caucvg  15242  summolem2a  15279  summolem2  15280  zsum  15282  fsumcvg3  15293  climfsum  15384  prodmolem2a  15496  prodmolem2  15497  zprod  15499  1arith  16480  pgpssslw  19003  gsumval3  19292  zntoslem  20521  rzgrp  20585  zcld  23710  mbflimsup  24563  ig1pdvds  25074  aacjcl  25220  aalioulem3  25227  uzssico  30825  qqhre  31682  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemiex  32180  erdszelem4  32869  erdszelem8  32873  supfz  33412  inffz  33413  poimirlem31  35545  poimirlem32  35546  irrapxlem1  40347  monotuz  40466  monotoddzzfi  40467  rmyeq0  40478  rmyeq  40479  lermy  40480  fzisoeu  42512  fzssre  42526  uzfissfz  42538  ssuzfz  42561  zssxr  42610  uzssre2  42620  uzred  42656  uzinico  42773  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  dvnprodlem1  43162  fourierdlem25  43348  fourierdlem37  43360  fourierdlem52  43374  fourierdlem64  43386  fourierdlem79  43401  etransclem48  43498  hoicvr  43761