Theorem zssre 12595

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

Syntax hints:   ⊆ wss 3926  ℝcr 11128  ℤcz 12588

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-neg 11469  df-z 12589

This theorem is referenced by:  suprzcl  12673  zred  12697  suprfinzcl  12707  uzssre  12874  uzwo2  12928  infssuzle  12947  infssuzcl  12948  lbzbi  12952  suprzub  12955  uzwo3  12959  rpnnen1lem3  12995  rpnnen1lem5  12997  fzval2  13527  flval3  13832  uzsup  13880  expcan  14187  ltexp2  14188  seqcoll  14482  limsupgre  15497  rlimclim  15562  isercolllem1  15681  isercolllem2  15682  isercoll  15684  caurcvg  15693  caucvg  15695  summolem2a  15731  summolem2  15732  zsum  15734  fsumcvg3  15745  climfsum  15836  prodmolem2a  15950  prodmolem2  15951  zprod  15953  1arith  16947  pgpssslw  19595  gsumval3  19888  zntoslem  21517  rzgrp  21583  zcld  24753  mbflimsup  25619  ig1pdvds  26137  aacjcl  26287  aalioulem3  26294  uzssico  32761  qqhre  34051  ballotlemfc0  34525  ballotlemfcc  34526  ballotlemiex  34534  erdszelem4  35216  erdszelem8  35220  supfz  35746  inffz  35747  poimirlem31  37675  poimirlem32  37676  irrapxlem1  42845  monotuz  42965  monotoddzzfi  42966  rmyeq0  42977  rmyeq  42978  lermy  42979  fzisoeu  45329  fzssre  45343  uzfissfz  45353  ssuzfz  45376  zssxr  45424  uzssre2  45434  uzred  45470  uzinico  45588  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  fourierdlem25  46161  fourierdlem37  46173  fourierdlem52  46187  fourierdlem64  46199  fourierdlem79  46214  etransclem48  46311  hoicvr  46577