Theorem zssre 12646

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

Syntax hints:   ⊆ wss 3976  ℝcr 11183  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  suprzcl  12723  zred  12747  suprfinzcl  12757  uzssre  12925  uzwo2  12977  infssuzle  12996  infssuzcl  12997  lbzbi  13001  suprzub  13004  uzwo3  13008  rpnnen1lem3  13044  rpnnen1lem5  13046  fzval2  13570  flval3  13866  uzsup  13914  expcan  14219  ltexp2  14220  seqcoll  14513  limsupgre  15527  rlimclim  15592  isercolllem1  15713  isercolllem2  15714  isercoll  15716  caurcvg  15725  caucvg  15727  summolem2a  15763  summolem2  15764  zsum  15766  fsumcvg3  15777  climfsum  15868  prodmolem2a  15982  prodmolem2  15983  zprod  15985  1arith  16974  pgpssslw  19656  gsumval3  19949  zntoslem  21598  rzgrp  21664  zcld  24854  mbflimsup  25720  ig1pdvds  26239  aacjcl  26387  aalioulem3  26394  uzssico  32789  qqhre  33966  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  erdszelem4  35162  erdszelem8  35166  supfz  35691  inffz  35692  poimirlem31  37611  poimirlem32  37612  irrapxlem1  42778  monotuz  42898  monotoddzzfi  42899  rmyeq0  42910  rmyeq  42911  lermy  42912  fzisoeu  45215  fzssre  45229  uzfissfz  45241  ssuzfz  45264  zssxr  45312  uzssre2  45322  uzred  45358  uzinico  45478  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem1  45867  fourierdlem25  46053  fourierdlem37  46065  fourierdlem52  46079  fourierdlem64  46091  fourierdlem79  46106  etransclem48  46203  hoicvr  46469