Theorem zssre 12620

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

Syntax hints:   ⊆ wss 3951  ℝcr 11154  ℤcz 12613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614

This theorem is referenced by:  suprzcl  12698  zred  12722  suprfinzcl  12732  uzssre  12900  uzwo2  12954  infssuzle  12973  infssuzcl  12974  lbzbi  12978  suprzub  12981  uzwo3  12985  rpnnen1lem3  13021  rpnnen1lem5  13023  fzval2  13550  flval3  13855  uzsup  13903  expcan  14209  ltexp2  14210  seqcoll  14503  limsupgre  15517  rlimclim  15582  isercolllem1  15701  isercolllem2  15702  isercoll  15704  caurcvg  15713  caucvg  15715  summolem2a  15751  summolem2  15752  zsum  15754  fsumcvg3  15765  climfsum  15856  prodmolem2a  15970  prodmolem2  15971  zprod  15973  1arith  16965  pgpssslw  19632  gsumval3  19925  zntoslem  21575  rzgrp  21641  zcld  24835  mbflimsup  25701  ig1pdvds  26219  aacjcl  26369  aalioulem3  26376  uzssico  32786  qqhre  34021  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemiex  34504  erdszelem4  35199  erdszelem8  35203  supfz  35729  inffz  35730  poimirlem31  37658  poimirlem32  37659  irrapxlem1  42833  monotuz  42953  monotoddzzfi  42954  rmyeq0  42965  rmyeq  42966  lermy  42967  fzisoeu  45312  fzssre  45326  uzfissfz  45337  ssuzfz  45360  zssxr  45408  uzssre2  45418  uzred  45454  uzinico  45573  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem25  46147  fourierdlem37  46159  fourierdlem52  46173  fourierdlem64  46185  fourierdlem79  46200  etransclem48  46297  hoicvr  46563