Theorem zssre 11712

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

Syntax hints:   ⊆ wss 3799  ℝcr 10252  ℤcz 11705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-ov 6909  df-neg 10589  df-z 11706

This theorem is referenced by:  suprzcl  11786  zred  11811  suprfinzcl  11821  uzwo2  12036  infssuzle  12055  infssuzcl  12056  lbzbi  12060  suprzub  12063  uzwo3  12067  rpnnen1lem3  12102  rpnnen1lem5  12104  fzval2  12623  flval3  12912  uzsup  12958  expcan  13208  ltexp2  13209  seqcoll  13538  limsupgre  14590  rlimclim  14655  isercolllem1  14773  isercolllem2  14774  isercoll  14776  caurcvg  14785  caucvg  14787  summolem2a  14824  summolem2  14825  zsum  14827  fsumcvg3  14838  climfsum  14927  prodmolem2a  15038  prodmolem2  15039  zprod  15041  1arith  16003  pgpssslw  18381  gsumval3  18662  zntoslem  20265  rzgrp  20331  zcld  22987  mbflimsup  23833  ig1pdvds  24336  aacjcl  24482  aalioulem3  24489  uzssico  30094  qqhre  30610  ballotlemfc0  31101  ballotlemfcc  31102  ballotlemiex  31110  erdszelem4  31723  erdszelem8  31727  supfz  32157  inffz  32158  poimirlem31  33985  poimirlem32  33986  irrapxlem1  38231  monotuz  38350  monotoddzzfi  38351  rmyeq0  38364  rmyeq  38365  lermy  38366  fzisoeu  40313  fzssre  40327  uzfissfz  40340  ssuzfz  40363  uzssre  40416  zssxr  40417  uzssre2  40429  uzred  40466  uzinico  40583  ioodvbdlimc1lem2  40943  ioodvbdlimc2lem  40945  dvnprodlem1  40957  fourierdlem25  41144  fourierdlem37  41156  fourierdlem52  41170  fourierdlem64  41182  fourierdlem79  41197  etransclem48  41294  hoicvr  41557