Theorem zssre 12482

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

Syntax hints:   ⊆ wss 3898  ℝcr 11012  ℤcz 12475

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-neg 11354  df-z 12476

This theorem is referenced by:  suprzcl  12559  zred  12583  suprfinzcl  12593  uzssre  12760  uzwo2  12812  infssuzle  12831  infssuzcl  12832  lbzbi  12836  suprzub  12839  uzwo3  12843  rpnnen1lem3  12879  rpnnen1lem5  12881  fzval2  13412  flval3  13721  uzsup  13769  expcan  14078  ltexp2  14079  seqcoll  14373  limsupgre  15390  rlimclim  15455  isercolllem1  15574  isercolllem2  15575  isercoll  15577  caurcvg  15586  caucvg  15588  summolem2a  15624  summolem2  15625  zsum  15627  fsumcvg3  15638  climfsum  15729  prodmolem2a  15843  prodmolem2  15844  zprod  15846  1arith  16841  pgpssslw  19528  gsumval3  19821  zntoslem  21495  rzgrp  21562  zcld  24730  mbflimsup  25595  ig1pdvds  26113  aacjcl  26263  aalioulem3  26270  uzssico  32771  qqhre  34054  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemiex  34536  erdszelem4  35259  erdszelem8  35263  supfz  35794  inffz  35795  poimirlem31  37711  poimirlem32  37712  irrapxlem1  42939  monotuz  43058  monotoddzzfi  43059  rmyeq0  43070  rmyeq  43071  lermy  43072  fzisoeu  45425  fzssre  45439  uzfissfz  45449  ssuzfz  45472  zssxr  45519  uzssre2  45529  uzred  45565  uzinico  45683  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  fourierdlem25  46254  fourierdlem37  46266  fourierdlem52  46280  fourierdlem64  46292  fourierdlem79  46307  etransclem48  46404  hoicvr  46670  chnsuslle  47003