Theorem zssre 12543

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

Syntax hints:   ⊆ wss 3917  ℝcr 11074  ℤcz 12536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537

This theorem is referenced by:  suprzcl  12621  zred  12645  suprfinzcl  12655  uzssre  12822  uzwo2  12878  infssuzle  12897  infssuzcl  12898  lbzbi  12902  suprzub  12905  uzwo3  12909  rpnnen1lem3  12945  rpnnen1lem5  12947  fzval2  13478  flval3  13784  uzsup  13832  expcan  14141  ltexp2  14142  seqcoll  14436  limsupgre  15454  rlimclim  15519  isercolllem1  15638  isercolllem2  15639  isercoll  15641  caurcvg  15650  caucvg  15652  summolem2a  15688  summolem2  15689  zsum  15691  fsumcvg3  15702  climfsum  15793  prodmolem2a  15907  prodmolem2  15908  zprod  15910  1arith  16905  pgpssslw  19551  gsumval3  19844  zntoslem  21473  rzgrp  21539  zcld  24709  mbflimsup  25574  ig1pdvds  26092  aacjcl  26242  aalioulem3  26249  uzssico  32714  qqhre  34017  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemiex  34500  erdszelem4  35188  erdszelem8  35192  supfz  35723  inffz  35724  poimirlem31  37652  poimirlem32  37653  irrapxlem1  42817  monotuz  42937  monotoddzzfi  42938  rmyeq0  42949  rmyeq  42950  lermy  42951  fzisoeu  45305  fzssre  45319  uzfissfz  45329  ssuzfz  45352  zssxr  45400  uzssre2  45410  uzred  45446  uzinico  45564  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  fourierdlem25  46137  fourierdlem37  46149  fourierdlem52  46163  fourierdlem64  46175  fourierdlem79  46190  etransclem48  46287  hoicvr  46553