Theorem zssre 12522

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

Syntax hints:   ⊆ wss 3890  ℝcr 11028  ℤcz 12515

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516

This theorem is referenced by:  suprzcl  12600  zred  12624  suprfinzcl  12634  uzssre  12801  uzwo2  12853  infssuzle  12872  infssuzcl  12873  lbzbi  12877  suprzub  12880  uzwo3  12884  rpnnen1lem3  12920  rpnnen1lem5  12922  fzval2  13455  flval3  13765  uzsup  13813  expcan  14122  ltexp2  14123  seqcoll  14417  limsupgre  15434  rlimclim  15499  isercolllem1  15618  isercolllem2  15619  isercoll  15621  caurcvg  15630  caucvg  15632  summolem2a  15668  summolem2  15669  zsum  15671  fsumcvg3  15682  climfsum  15774  prodmolem2a  15890  prodmolem2  15891  zprod  15893  1arith  16889  pgpssslw  19580  gsumval3  19873  zntoslem  21546  rzgrp  21613  zcld  24789  mbflimsup  25643  ig1pdvds  26155  aacjcl  26304  aalioulem3  26311  uzssico  32872  qqhre  34180  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemiex  34662  erdszelem4  35392  erdszelem8  35396  supfz  35927  inffz  35928  poimirlem31  37986  poimirlem32  37987  irrapxlem1  43268  monotuz  43387  monotoddzzfi  43388  rmyeq0  43399  rmyeq  43400  lermy  43401  fzisoeu  45751  fzssre  45765  uzfissfz  45774  ssuzfz  45797  zssxr  45844  uzssre2  45853  uzred  45889  uzinico  46007  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  fourierdlem25  46578  fourierdlem37  46590  fourierdlem52  46604  fourierdlem64  46616  fourierdlem79  46631  etransclem48  46728  chnsuslle  47327