Theorem zssre 12681

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

This proof depends on syntax axioms:   ⊆ wss 3899  ℝcr 11180  ℤcz 12674

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-neg 11525  df-z 12675

This theorem is used by:  suprzcl  12760  zred  12784  suprfinzcl  12794  uzssre  12968  uzwo2  13020  infssuzle  13039  infssuzcl  13040  lbzbi  13044  suprzub  13047  uzwo3  13051  rpnnen1lem3  13088  rpnnen1lem5  13090  fzval2  13623  flval3  13935  uzsup  13983  expcan  14292  ltexp2  14293  seqcoll  14589  limsupgre  15628  rlimclim  15693  isercolllem1  15812  isercolllem2  15813  isercoll  15815  caurcvg  15824  caucvg  15826  summolem2a  15861  summolem2  15862  zsum  15864  fsumcvg3  15875  climfsum  15967  prodmolem2a  16081  prodmolem2  16082  zprod  16084  1arith  17085  pgpssslw  19808  gsumval3  20101  zntoslem  21842  rzgrp  21909  zcld  25113  mbflimsup  25967  ig1pdvds  26478  aacjcl  26636  aalioulem3  26643  uzssico  33358  qqhre  34634  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemiex  35117  erdszelem4  35928  erdszelem8  35932  supfz  36463  inffz  36464  poimirlem31  38537  poimirlem32  38538  irrapxlem1  43782  monotuz  43901  monotoddzzfi  43902  rmyeq0  43913  rmyeq  43914  lermy  43915  fzisoeu  46259  fzssre  46273  uzfissfz  46282  ssuzfz  46305  zssxr  46352  uzssre2  46361  uzred  46397  uzinico  46515  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  fourierdlem25  47086  fourierdlem37  47098  fourierdlem52  47112  fourierdlem64  47124  fourierdlem79  47139  etransclem48  47236  chnsuslle  47835