Theorem zssre 12616

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

This proof depends on syntax axioms:   ⊆ wss 3908  ℝcr 11117  ℤcz 12609

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-neg 11462  df-z 12610

This theorem is used by:  suprzcl  12694  zred  12718  suprfinzcl  12728  uzssre  12902  uzwo2  12954  infssuzle  12973  infssuzcl  12974  lbzbi  12978  suprzub  12981  uzwo3  12985  rpnnen1lem3  13021  rpnnen1lem5  13023  fzval2  13556  flval3  13868  uzsup  13916  expcan  14225  ltexp2  14226  seqcoll  14521  limsupgre  15558  rlimclim  15623  isercolllem1  15742  isercolllem2  15743  isercoll  15745  caurcvg  15754  caucvg  15756  summolem2a  15792  summolem2  15793  zsum  15795  fsumcvg3  15806  climfsum  15898  prodmolem2a  16014  prodmolem2  16015  zprod  16017  1arith  17012  pgpssslw  19715  gsumval3  20008  zntoslem  21743  rzgrp  21810  zcld  25008  mbflimsup  25862  ig1pdvds  26374  aacjcl  26527  aalioulem3  26534  uzssico  33166  qqhre  34441  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemiex  34924  erdszelem4  35707  erdszelem8  35711  supfz  36242  inffz  36243  poimirlem31  38343  poimirlem32  38344  irrapxlem1  43590  monotuz  43709  monotoddzzfi  43710  rmyeq0  43721  rmyeq  43722  lermy  43723  fzisoeu  46060  fzssre  46074  uzfissfz  46083  ssuzfz  46106  zssxr  46153  uzssre2  46162  uzred  46198  uzinico  46316  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  fourierdlem25  46887  fourierdlem37  46899  fourierdlem52  46913  fourierdlem64  46925  fourierdlem79  46940  etransclem48  47037  chnsuslle  47638