Theorem zssre 12536

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

Syntax hints:   ⊆ wss 3914  ℝcr 11067  ℤcz 12529

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  suprzcl  12614  zred  12638  suprfinzcl  12648  uzssre  12815  uzwo2  12871  infssuzle  12890  infssuzcl  12891  lbzbi  12895  suprzub  12898  uzwo3  12902  rpnnen1lem3  12938  rpnnen1lem5  12940  fzval2  13471  flval3  13777  uzsup  13825  expcan  14134  ltexp2  14135  seqcoll  14429  limsupgre  15447  rlimclim  15512  isercolllem1  15631  isercolllem2  15632  isercoll  15634  caurcvg  15643  caucvg  15645  summolem2a  15681  summolem2  15682  zsum  15684  fsumcvg3  15695  climfsum  15786  prodmolem2a  15900  prodmolem2  15901  zprod  15903  1arith  16898  pgpssslw  19544  gsumval3  19837  zntoslem  21466  rzgrp  21532  zcld  24702  mbflimsup  25567  ig1pdvds  26085  aacjcl  26235  aalioulem3  26242  uzssico  32707  qqhre  34010  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemiex  34493  erdszelem4  35181  erdszelem8  35185  supfz  35716  inffz  35717  poimirlem31  37645  poimirlem32  37646  irrapxlem1  42810  monotuz  42930  monotoddzzfi  42931  rmyeq0  42942  rmyeq  42943  lermy  42944  fzisoeu  45298  fzssre  45312  uzfissfz  45322  ssuzfz  45345  zssxr  45393  uzssre2  45403  uzred  45439  uzinico  45557  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  fourierdlem25  46130  fourierdlem37  46142  fourierdlem52  46156  fourierdlem64  46168  fourierdlem79  46183  etransclem48  46280  hoicvr  46546