Theorem zssre 12598

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

Syntax hints:   ⊆ wss 3913  ℝcr 11099  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592

This theorem is referenced by:  suprzcl  12676  zred  12700  suprfinzcl  12710  uzssre  12884  uzwo2  12936  infssuzle  12955  infssuzcl  12956  lbzbi  12960  suprzub  12963  uzwo3  12967  rpnnen1lem3  13003  rpnnen1lem5  13005  fzval2  13538  flval3  13848  uzsup  13896  expcan  14205  ltexp2  14206  seqcoll  14501  limsupgre  15532  rlimclim  15597  isercolllem1  15716  isercolllem2  15717  isercoll  15719  caurcvg  15728  caucvg  15730  summolem2a  15766  summolem2  15767  zsum  15769  fsumcvg3  15780  climfsum  15872  prodmolem2a  15988  prodmolem2  15989  zprod  15991  1arith  16987  pgpssslw  19684  gsumval3  19977  zntoslem  21675  rzgrp  21742  zcld  24940  mbflimsup  25794  ig1pdvds  26306  aacjcl  26457  aalioulem3  26464  uzssico  33070  qqhre  34355  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemiex  34837  erdszelem4  35585  erdszelem8  35589  supfz  36120  inffz  36121  poimirlem31  38190  poimirlem32  38191  irrapxlem1  43441  monotuz  43560  monotoddzzfi  43561  rmyeq0  43572  rmyeq  43573  lermy  43574  fzisoeu  45911  fzssre  45925  uzfissfz  45934  ssuzfz  45957  zssxr  46004  uzssre2  46013  uzred  46049  uzinico  46167  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  fourierdlem25  46738  fourierdlem37  46750  fourierdlem52  46764  fourierdlem64  46776  fourierdlem79  46791  etransclem48  46888  chnsuslle  47489