Theorem zssre 12529

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

Syntax hints:   ⊆ wss 3890  ℝcr 11035  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523

This theorem is referenced by:  suprzcl  12607  zred  12631  suprfinzcl  12641  uzssre  12808  uzwo2  12860  infssuzle  12879  infssuzcl  12880  lbzbi  12884  suprzub  12887  uzwo3  12891  rpnnen1lem3  12927  rpnnen1lem5  12929  fzval2  13462  flval3  13772  uzsup  13820  expcan  14129  ltexp2  14130  seqcoll  14424  limsupgre  15441  rlimclim  15506  isercolllem1  15625  isercolllem2  15626  isercoll  15628  caurcvg  15637  caucvg  15639  summolem2a  15675  summolem2  15676  zsum  15678  fsumcvg3  15689  climfsum  15781  prodmolem2a  15897  prodmolem2  15898  zprod  15900  1arith  16896  pgpssslw  19587  gsumval3  19880  zntoslem  21538  rzgrp  21605  zcld  24804  mbflimsup  25658  ig1pdvds  26170  aacjcl  26318  aalioulem3  26325  uzssico  32883  qqhre  34211  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemiex  34693  erdszelem4  35429  erdszelem8  35433  supfz  35964  inffz  35965  poimirlem31  38025  poimirlem32  38026  irrapxlem1  43274  monotuz  43393  monotoddzzfi  43394  rmyeq0  43405  rmyeq  43406  lermy  43407  fzisoeu  45755  fzssre  45769  uzfissfz  45778  ssuzfz  45801  zssxr  45848  uzssre2  45857  uzred  45893  uzinico  46011  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  fourierdlem25  46582  fourierdlem37  46594  fourierdlem52  46608  fourierdlem64  46620  fourierdlem79  46635  etransclem48  46732  chnsuslle  47333