Theorem zssre 12565

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

Syntax hints:   ⊆ wss 3949  ℝcr 11109  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559

This theorem is referenced by:  suprzcl  12642  zred  12666  suprfinzcl  12676  uzssre  12844  uzwo2  12896  infssuzle  12915  infssuzcl  12916  lbzbi  12920  suprzub  12923  uzwo3  12927  rpnnen1lem3  12963  rpnnen1lem5  12965  fzval2  13487  flval3  13780  uzsup  13828  expcan  14134  ltexp2  14135  seqcoll  14425  limsupgre  15425  rlimclim  15490  isercolllem1  15611  isercolllem2  15612  isercoll  15614  caurcvg  15623  caucvg  15625  summolem2a  15661  summolem2  15662  zsum  15664  fsumcvg3  15675  climfsum  15766  prodmolem2a  15878  prodmolem2  15879  zprod  15881  1arith  16860  pgpssslw  19482  gsumval3  19775  zntoslem  21112  rzgrp  21176  zcld  24329  mbflimsup  25183  ig1pdvds  25694  aacjcl  25840  aalioulem3  25847  uzssico  31995  qqhre  33000  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemiex  33500  erdszelem4  34185  erdszelem8  34189  supfz  34698  inffz  34699  poimirlem31  36519  poimirlem32  36520  irrapxlem1  41560  monotuz  41680  monotoddzzfi  41681  rmyeq0  41692  rmyeq  41693  lermy  41694  fzisoeu  44010  fzssre  44024  uzfissfz  44036  ssuzfz  44059  zssxr  44107  uzssre2  44117  uzred  44153  uzinico  44273  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem1  44662  fourierdlem25  44848  fourierdlem37  44860  fourierdlem52  44874  fourierdlem64  44886  fourierdlem79  44901  etransclem48  44998  hoicvr  45264