Theorem zssre 12599

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 12596	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
2	1	ssriv 3942	1 ⊢ ℤ ⊆ ℝ

Syntax hints:   ⊆ wss 3906  ℝcr 11100  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593

This theorem is referenced by:  suprzcl  12677  zred  12701  suprfinzcl  12711  uzssre  12885  uzwo2  12937  infssuzle  12956  infssuzcl  12957  lbzbi  12961  suprzub  12964  uzwo3  12968  rpnnen1lem3  13004  rpnnen1lem5  13006  fzval2  13539  flval3  13850  uzsup  13898  expcan  14207  ltexp2  14208  seqcoll  14503  limsupgre  15534  rlimclim  15599  isercolllem1  15718  isercolllem2  15719  isercoll  15721  caurcvg  15730  caucvg  15732  summolem2a  15768  summolem2  15769  zsum  15771  fsumcvg3  15782  climfsum  15874  prodmolem2a  15990  prodmolem2  15991  zprod  15993  1arith  16988  pgpssslw  19685  gsumval3  19978  zntoslem  21687  rzgrp  21754  zcld  24952  mbflimsup  25806  ig1pdvds  26318  aacjcl  26469  aalioulem3  26476  uzssico  33107  qqhre  34388  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemiex  34870  erdszelem4  35664  erdszelem8  35668  supfz  36199  inffz  36200  poimirlem31  38280  poimirlem32  38281  irrapxlem1  43529  monotuz  43648  monotoddzzfi  43649  rmyeq0  43660  rmyeq  43661  lermy  43662  fzisoeu  45999  fzssre  46013  uzfissfz  46022  ssuzfz  46045  zssxr  46092  uzssre2  46101  uzred  46137  uzinico  46255  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  fourierdlem25  46826  fourierdlem37  46838  fourierdlem52  46852  fourierdlem64  46864  fourierdlem79  46879  etransclem48  46976  chnsuslle  47577