Theorem zssre 12617

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

Syntax hints:   ⊆ wss 3962  ℝcr 11151  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  suprzcl  12695  zred  12719  suprfinzcl  12729  uzssre  12897  uzwo2  12951  infssuzle  12970  infssuzcl  12971  lbzbi  12975  suprzub  12978  uzwo3  12982  rpnnen1lem3  13018  rpnnen1lem5  13020  fzval2  13546  flval3  13851  uzsup  13899  expcan  14205  ltexp2  14206  seqcoll  14499  limsupgre  15513  rlimclim  15578  isercolllem1  15697  isercolllem2  15698  isercoll  15700  caurcvg  15709  caucvg  15711  summolem2a  15747  summolem2  15748  zsum  15750  fsumcvg3  15761  climfsum  15852  prodmolem2a  15966  prodmolem2  15967  zprod  15969  1arith  16960  pgpssslw  19646  gsumval3  19939  zntoslem  21592  rzgrp  21658  zcld  24848  mbflimsup  25714  ig1pdvds  26233  aacjcl  26383  aalioulem3  26390  uzssico  32792  qqhre  33982  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemiex  34482  erdszelem4  35178  erdszelem8  35182  supfz  35708  inffz  35709  poimirlem31  37637  poimirlem32  37638  irrapxlem1  42809  monotuz  42929  monotoddzzfi  42930  rmyeq0  42941  rmyeq  42942  lermy  42943  fzisoeu  45250  fzssre  45264  uzfissfz  45275  ssuzfz  45298  zssxr  45346  uzssre2  45356  uzred  45392  uzinico  45512  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  fourierdlem25  46087  fourierdlem37  46099  fourierdlem52  46113  fourierdlem64  46125  fourierdlem79  46140  etransclem48  46237  hoicvr  46503