Theorem zssre 12515

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

Syntax hints:   ⊆ wss 3913  ℝcr 11059  ℤcz 12508

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-neg 11397  df-z 12509

This theorem is referenced by:  suprzcl  12592  zred  12616  suprfinzcl  12626  uzssre  12794  uzwo2  12846  infssuzle  12865  infssuzcl  12866  lbzbi  12870  suprzub  12873  uzwo3  12877  rpnnen1lem3  12913  rpnnen1lem5  12915  fzval2  13437  flval3  13730  uzsup  13778  expcan  14084  ltexp2  14085  seqcoll  14375  limsupgre  15375  rlimclim  15440  isercolllem1  15561  isercolllem2  15562  isercoll  15564  caurcvg  15573  caucvg  15575  summolem2a  15611  summolem2  15612  zsum  15614  fsumcvg3  15625  climfsum  15716  prodmolem2a  15828  prodmolem2  15829  zprod  15831  1arith  16810  pgpssslw  19410  gsumval3  19698  zntoslem  21000  rzgrp  21064  zcld  24213  mbflimsup  25067  ig1pdvds  25578  aacjcl  25724  aalioulem3  25731  uzssico  31755  qqhre  32690  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemiex  33190  erdszelem4  33875  erdszelem8  33879  supfz  34387  inffz  34388  poimirlem31  36182  poimirlem32  36183  irrapxlem1  41203  monotuz  41323  monotoddzzfi  41324  rmyeq0  41335  rmyeq  41336  lermy  41337  fzisoeu  43655  fzssre  43669  uzfissfz  43681  ssuzfz  43704  zssxr  43752  uzssre2  43762  uzred  43798  uzinico  43918  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnprodlem1  44307  fourierdlem25  44493  fourierdlem37  44505  fourierdlem52  44519  fourierdlem64  44531  fourierdlem79  44546  etransclem48  44643  hoicvr  44909