Theorem zssre 12572

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

Syntax hints:   ⊆ wss 3904  ℝcr 11069  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-neg 11414  df-z 12566

This theorem is referenced by:  suprzcl  12650  zred  12674  suprfinzcl  12684  uzssre  12858  uzwo2  12910  infssuzle  12929  infssuzcl  12930  lbzbi  12934  suprzub  12937  uzwo3  12941  rpnnen1lem3  12977  rpnnen1lem5  12979  fzval2  13512  flval3  13822  uzsup  13870  expcan  14179  ltexp2  14180  seqcoll  14474  limsupgre  15491  rlimclim  15556  isercolllem1  15675  isercolllem2  15676  isercoll  15678  caurcvg  15687  caucvg  15689  summolem2a  15725  summolem2  15726  zsum  15728  fsumcvg3  15739  climfsum  15831  prodmolem2a  15947  prodmolem2  15948  zprod  15950  1arith  16946  pgpssslw  19637  gsumval3  19930  zntoslem  21588  rzgrp  21655  zcld  24854  mbflimsup  25708  ig1pdvds  26220  aacjcl  26368  aalioulem3  26375  uzssico  32936  qqhre  34278  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemiex  34760  erdszelem4  35508  erdszelem8  35512  supfz  36043  inffz  36044  poimirlem31  38114  poimirlem32  38115  irrapxlem1  43363  monotuz  43482  monotoddzzfi  43483  rmyeq0  43494  rmyeq  43495  lermy  43496  fzisoeu  45843  fzssre  45857  uzfissfz  45866  ssuzfz  45889  zssxr  45936  uzssre2  45945  uzred  45981  uzinico  46099  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  fourierdlem25  46670  fourierdlem37  46682  fourierdlem52  46696  fourierdlem64  46708  fourierdlem79  46723  etransclem48  46820  chnsuslle  47421