Theorem zssre 12472

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

Syntax hints:   ⊆ wss 3902  ℝcr 11002  ℤcz 12465

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11344  df-z 12466

This theorem is referenced by:  suprzcl  12550  zred  12574  suprfinzcl  12584  uzssre  12751  uzwo2  12807  infssuzle  12826  infssuzcl  12827  lbzbi  12831  suprzub  12834  uzwo3  12838  rpnnen1lem3  12874  rpnnen1lem5  12876  fzval2  13407  flval3  13716  uzsup  13764  expcan  14073  ltexp2  14074  seqcoll  14368  limsupgre  15385  rlimclim  15450  isercolllem1  15569  isercolllem2  15570  isercoll  15572  caurcvg  15581  caucvg  15583  summolem2a  15619  summolem2  15620  zsum  15622  fsumcvg3  15633  climfsum  15724  prodmolem2a  15838  prodmolem2  15839  zprod  15841  1arith  16836  pgpssslw  19524  gsumval3  19817  zntoslem  21491  rzgrp  21558  zcld  24727  mbflimsup  25592  ig1pdvds  26110  aacjcl  26260  aalioulem3  26267  uzssico  32762  qqhre  34028  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemiex  34510  erdszelem4  35226  erdszelem8  35230  supfz  35761  inffz  35762  poimirlem31  37690  poimirlem32  37691  irrapxlem1  42854  monotuz  42973  monotoddzzfi  42974  rmyeq0  42985  rmyeq  42986  lermy  42987  fzisoeu  45340  fzssre  45354  uzfissfz  45364  ssuzfz  45387  zssxr  45434  uzssre2  45444  uzred  45480  uzinico  45598  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  fourierdlem25  46169  fourierdlem37  46181  fourierdlem52  46195  fourierdlem64  46207  fourierdlem79  46222  etransclem48  46319  hoicvr  46585