Theorem zssre 12626

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

This proof depends on syntax axioms:   ⊆ wss 3902  ℝcr 11127  ℤcz 12619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-neg 11472  df-z 12620

This theorem is used by:  suprzcl  12705  zred  12729  suprfinzcl  12739  uzssre  12913  uzwo2  12965  infssuzle  12984  infssuzcl  12985  lbzbi  12989  suprzub  12992  uzwo3  12996  rpnnen1lem3  13033  rpnnen1lem5  13035  fzval2  13568  flval3  13880  uzsup  13928  expcan  14237  ltexp2  14238  seqcoll  14533  limsupgre  15572  rlimclim  15637  isercolllem1  15756  isercolllem2  15757  isercoll  15759  caurcvg  15768  caucvg  15770  summolem2a  15805  summolem2  15806  zsum  15808  fsumcvg3  15819  climfsum  15911  prodmolem2a  16027  prodmolem2  16028  zprod  16030  1arith  17025  pgpssslw  19747  gsumval3  20040  zntoslem  21775  rzgrp  21842  zcld  25046  mbflimsup  25900  ig1pdvds  26412  aacjcl  26570  aalioulem3  26577  uzssico  33263  qqhre  34538  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemiex  35021  erdszelem4  35781  erdszelem8  35785  supfz  36316  inffz  36317  poimirlem31  38408  poimirlem32  38409  irrapxlem1  43671  monotuz  43790  monotoddzzfi  43791  rmyeq0  43802  rmyeq  43803  lermy  43804  fzisoeu  46141  fzssre  46155  uzfissfz  46164  ssuzfz  46187  zssxr  46234  uzssre2  46243  uzred  46279  uzinico  46397  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  fourierdlem25  46968  fourierdlem37  46980  fourierdlem52  46994  fourierdlem64  47006  fourierdlem79  47021  etransclem48  47118  chnsuslle  47717