Theorem zssre 12495

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

Syntax hints:   ⊆ wss 3901  ℝcr 11025  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  suprzcl  12572  zred  12596  suprfinzcl  12606  uzssre  12773  uzwo2  12825  infssuzle  12844  infssuzcl  12845  lbzbi  12849  suprzub  12852  uzwo3  12856  rpnnen1lem3  12892  rpnnen1lem5  12894  fzval2  13426  flval3  13735  uzsup  13783  expcan  14092  ltexp2  14093  seqcoll  14387  limsupgre  15404  rlimclim  15469  isercolllem1  15588  isercolllem2  15589  isercoll  15591  caurcvg  15600  caucvg  15602  summolem2a  15638  summolem2  15639  zsum  15641  fsumcvg3  15652  climfsum  15743  prodmolem2a  15857  prodmolem2  15858  zprod  15860  1arith  16855  pgpssslw  19543  gsumval3  19836  zntoslem  21511  rzgrp  21578  zcld  24758  mbflimsup  25623  ig1pdvds  26141  aacjcl  26291  aalioulem3  26298  uzssico  32864  qqhre  34177  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemiex  34659  erdszelem4  35388  erdszelem8  35392  supfz  35923  inffz  35924  poimirlem31  37848  poimirlem32  37849  irrapxlem1  43060  monotuz  43179  monotoddzzfi  43180  rmyeq0  43191  rmyeq  43192  lermy  43193  fzisoeu  45544  fzssre  45558  uzfissfz  45567  ssuzfz  45590  zssxr  45637  uzssre2  45647  uzred  45683  uzinico  45801  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  fourierdlem25  46372  fourierdlem37  46384  fourierdlem52  46398  fourierdlem64  46410  fourierdlem79  46425  etransclem48  46522  hoicvr  46788  chnsuslle  47121