![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zssre | Structured version Visualization version GIF version |
Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.) |
Ref | Expression |
---|---|
zssre | ⊢ ℤ ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 12437 | . 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℝ) | |
2 | 1 | ssriv 3947 | 1 ⊢ ℤ ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3909 ℝcr 10984 ℤcz 12433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-iota 6444 df-fv 6500 df-ov 7353 df-neg 11322 df-z 12434 |
This theorem is referenced by: suprzcl 12517 zred 12541 suprfinzcl 12551 uzssre 12719 uzwo2 12767 infssuzle 12786 infssuzcl 12787 lbzbi 12791 suprzub 12794 uzwo3 12798 rpnnen1lem3 12834 rpnnen1lem5 12836 fzval2 13357 flval3 13650 uzsup 13698 expcan 14002 ltexp2 14003 seqcoll 14292 limsupgre 15299 rlimclim 15364 isercolllem1 15485 isercolllem2 15486 isercoll 15488 caurcvg 15497 caucvg 15499 summolem2a 15536 summolem2 15537 zsum 15539 fsumcvg3 15550 climfsum 15641 prodmolem2a 15753 prodmolem2 15754 zprod 15756 1arith 16735 pgpssslw 19331 gsumval3 19619 zntoslem 20892 rzgrp 20956 zcld 24104 mbflimsup 24958 ig1pdvds 25469 aacjcl 25615 aalioulem3 25622 uzssico 31488 qqhre 32381 ballotlemfc0 32872 ballotlemfcc 32873 ballotlemiex 32881 erdszelem4 33568 erdszelem8 33572 supfz 34095 inffz 34096 poimirlem31 36040 poimirlem32 36041 irrapxlem1 41047 monotuz 41167 monotoddzzfi 41168 rmyeq0 41179 rmyeq 41180 lermy 41181 fzisoeu 43329 fzssre 43343 uzfissfz 43355 ssuzfz 43378 zssxr 43427 uzssre2 43437 uzred 43473 uzinico 43589 ioodvbdlimc1lem2 43964 ioodvbdlimc2lem 43966 dvnprodlem1 43978 fourierdlem25 44164 fourierdlem37 44176 fourierdlem52 44190 fourierdlem64 44202 fourierdlem79 44217 etransclem48 44314 hoicvr 44580 |
Copyright terms: Public domain | W3C validator |