Theorem zssre 12727

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

This proof depends on syntax axioms:   ⊆ wss 3900  ℝcr 11226  ℤcz 12720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-neg 11571  df-z 12721

This theorem is used by:  suprzcl  12806  zred  12830  suprfinzcl  12840  uzssre  13014  uzwo2  13066  infssuzle  13085  infssuzcl  13086  lbzbi  13090  suprzub  13093  uzwo3  13097  rpnnen1lem3  13134  rpnnen1lem5  13136  fzval2  13669  fzssre  13686  flval3  13982  uzsup  14030  expcan  14339  ltexp2  14340  seqcoll  14636  limsupgre  15677  rlimclim  15742  isercolllem1  15861  isercolllem2  15862  isercoll  15864  caurcvg  15873  caucvg  15875  summolem2a  15910  summolem2  15911  zsum  15913  fsumcvg3  15924  climfsum  16016  prodmolem2a  16130  prodmolem2  16131  zprod  16133  1arith  17134  pgpssslw  19858  gsumval3  20151  zntoslem  21892  rzgrp  21959  zcld  25163  mbflimsup  26017  ig1pdvds  26528  aacjcl  26684  aalioulem3  26691  uzssico  33446  qqhre  34722  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemiex  35204  erdszelem4  36126  erdszelem8  36130  supfz  36672  inffz  36673  poimirlem31  38761  poimirlem32  38762  irrapxlem1  44022  monotuz  44141  monotoddzzfi  44142  rmyeq0  44153  rmyeq  44154  lermy  44155  fzisoeu  46521  uzfissfz  46543  ssuzfz  46566  zssxr  46613  uzssre2  46622  uzred  46658  uzinico  46776  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  fourierdlem25  47347  fourierdlem37  47359  fourierdlem52  47373  fourierdlem64  47385  fourierdlem79  47400  etransclem48  47497  chnsuslle  48096