Theorem zssre 12507

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

Syntax hints:   ⊆ wss 3903  ℝcr 11037  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  suprzcl  12584  zred  12608  suprfinzcl  12618  uzssre  12785  uzwo2  12837  infssuzle  12856  infssuzcl  12857  lbzbi  12861  suprzub  12864  uzwo3  12868  rpnnen1lem3  12904  rpnnen1lem5  12906  fzval2  13438  flval3  13747  uzsup  13795  expcan  14104  ltexp2  14105  seqcoll  14399  limsupgre  15416  rlimclim  15481  isercolllem1  15600  isercolllem2  15601  isercoll  15603  caurcvg  15612  caucvg  15614  summolem2a  15650  summolem2  15651  zsum  15653  fsumcvg3  15664  climfsum  15755  prodmolem2a  15869  prodmolem2  15870  zprod  15872  1arith  16867  pgpssslw  19555  gsumval3  19848  zntoslem  21523  rzgrp  21590  zcld  24770  mbflimsup  25635  ig1pdvds  26153  aacjcl  26303  aalioulem3  26310  uzssico  32874  qqhre  34197  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemiex  34679  erdszelem4  35407  erdszelem8  35411  supfz  35942  inffz  35943  poimirlem31  37896  poimirlem32  37897  irrapxlem1  43173  monotuz  43292  monotoddzzfi  43293  rmyeq0  43304  rmyeq  43305  lermy  43306  fzisoeu  45656  fzssre  45670  uzfissfz  45679  ssuzfz  45702  zssxr  45749  uzssre2  45759  uzred  45795  uzinico  45913  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  fourierdlem25  46484  fourierdlem37  46496  fourierdlem52  46510  fourierdlem64  46522  fourierdlem79  46537  etransclem48  46634  hoicvr  46900  chnsuslle  47233