Theorem zssre 12603

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

Syntax hints:   ⊆ wss 3931  ℝcr 11136  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-neg 11477  df-z 12597

This theorem is referenced by:  suprzcl  12681  zred  12705  suprfinzcl  12715  uzssre  12882  uzwo2  12936  infssuzle  12955  infssuzcl  12956  lbzbi  12960  suprzub  12963  uzwo3  12967  rpnnen1lem3  13003  rpnnen1lem5  13005  fzval2  13532  flval3  13837  uzsup  13885  expcan  14191  ltexp2  14192  seqcoll  14485  limsupgre  15499  rlimclim  15564  isercolllem1  15683  isercolllem2  15684  isercoll  15686  caurcvg  15695  caucvg  15697  summolem2a  15733  summolem2  15734  zsum  15736  fsumcvg3  15747  climfsum  15838  prodmolem2a  15952  prodmolem2  15953  zprod  15955  1arith  16947  pgpssslw  19600  gsumval3  19893  zntoslem  21529  rzgrp  21595  zcld  24771  mbflimsup  25637  ig1pdvds  26155  aacjcl  26305  aalioulem3  26312  uzssico  32725  qqhre  33980  ballotlemfc0  34454  ballotlemfcc  34455  ballotlemiex  34463  erdszelem4  35158  erdszelem8  35162  supfz  35688  inffz  35689  poimirlem31  37617  poimirlem32  37618  irrapxlem1  42796  monotuz  42916  monotoddzzfi  42917  rmyeq0  42928  rmyeq  42929  lermy  42930  fzisoeu  45269  fzssre  45283  uzfissfz  45294  ssuzfz  45317  zssxr  45365  uzssre2  45375  uzred  45411  uzinico  45530  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  fourierdlem25  46104  fourierdlem37  46116  fourierdlem52  46130  fourierdlem64  46142  fourierdlem79  46157  etransclem48  46254  hoicvr  46520