Theorem zssre 12496

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

Syntax hints:   ⊆ wss 3905  ℝcr 11027  ℤcz 12489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490

This theorem is referenced by:  suprzcl  12574  zred  12598  suprfinzcl  12608  uzssre  12775  uzwo2  12831  infssuzle  12850  infssuzcl  12851  lbzbi  12855  suprzub  12858  uzwo3  12862  rpnnen1lem3  12898  rpnnen1lem5  12900  fzval2  13431  flval3  13737  uzsup  13785  expcan  14094  ltexp2  14095  seqcoll  14389  limsupgre  15406  rlimclim  15471  isercolllem1  15590  isercolllem2  15591  isercoll  15593  caurcvg  15602  caucvg  15604  summolem2a  15640  summolem2  15641  zsum  15643  fsumcvg3  15654  climfsum  15745  prodmolem2a  15859  prodmolem2  15860  zprod  15862  1arith  16857  pgpssslw  19511  gsumval3  19804  zntoslem  21481  rzgrp  21548  zcld  24718  mbflimsup  25583  ig1pdvds  26101  aacjcl  26251  aalioulem3  26258  uzssico  32740  qqhre  33986  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemiex  34469  erdszelem4  35166  erdszelem8  35170  supfz  35701  inffz  35702  poimirlem31  37630  poimirlem32  37631  irrapxlem1  42795  monotuz  42914  monotoddzzfi  42915  rmyeq0  42926  rmyeq  42927  lermy  42928  fzisoeu  45282  fzssre  45296  uzfissfz  45306  ssuzfz  45329  zssxr  45377  uzssre2  45387  uzred  45423  uzinico  45541  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  fourierdlem25  46114  fourierdlem37  46126  fourierdlem52  46140  fourierdlem64  46152  fourierdlem79  46167  etransclem48  46264  hoicvr  46530