Theorem zssre 12531

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

Syntax hints:   ⊆ wss 3889  ℝcr 11037  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  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 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  suprzcl  12609  zred  12633  suprfinzcl  12643  uzssre  12810  uzwo2  12862  infssuzle  12881  infssuzcl  12882  lbzbi  12886  suprzub  12889  uzwo3  12893  rpnnen1lem3  12929  rpnnen1lem5  12931  fzval2  13464  flval3  13774  uzsup  13822  expcan  14131  ltexp2  14132  seqcoll  14426  limsupgre  15443  rlimclim  15508  isercolllem1  15627  isercolllem2  15628  isercoll  15630  caurcvg  15639  caucvg  15641  summolem2a  15677  summolem2  15678  zsum  15680  fsumcvg3  15691  climfsum  15783  prodmolem2a  15899  prodmolem2  15900  zprod  15902  1arith  16898  pgpssslw  19589  gsumval3  19882  zntoslem  21536  rzgrp  21603  zcld  24779  mbflimsup  25633  ig1pdvds  26145  aacjcl  26293  aalioulem3  26300  uzssico  32857  qqhre  34164  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemiex  34646  erdszelem4  35376  erdszelem8  35380  supfz  35911  inffz  35912  poimirlem31  37972  poimirlem32  37973  irrapxlem1  43250  monotuz  43369  monotoddzzfi  43370  rmyeq0  43381  rmyeq  43382  lermy  43383  fzisoeu  45733  fzssre  45747  uzfissfz  45756  ssuzfz  45779  zssxr  45826  uzssre2  45835  uzred  45871  uzinico  45989  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  fourierdlem25  46560  fourierdlem37  46572  fourierdlem52  46586  fourierdlem64  46598  fourierdlem79  46613  etransclem48  46710  chnsuslle  47311