Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > zssre | Structured version Visualization version Unicode 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 11381 | . 2 | |
2 | 1 | ssriv 3607 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wss 3574 cr 9935 cz 11377 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-neg 10269 df-z 11378 |
This theorem is referenced by: suprzcl 11457 zred 11482 suprfinzcl 11492 uzwo2 11752 infssuzle 11771 infssuzcl 11772 lbzbi 11776 suprzub 11779 uzwo3 11783 rpnnen1lem3 11816 rpnnen1lem5 11818 rpnnen1lem3OLD 11822 rpnnen1lem5OLD 11824 fzval2 12329 flval3 12616 uzsup 12662 expcan 12913 ltexp2 12914 seqcoll 13248 limsupgre 14212 rlimclim 14277 isercolllem1 14395 isercolllem2 14396 isercoll 14398 caurcvg 14407 caucvg 14409 summolem2a 14446 summolem2 14447 zsum 14449 fsumcvg3 14460 climfsum 14552 prodmolem2a 14664 prodmolem2 14665 zprod 14667 1arith 15631 pgpssslw 18029 gsumval3 18308 zntoslem 19905 zcld 22616 mbflimsup 23433 ig1pdvds 23936 aacjcl 24082 aalioulem3 24089 rzgrp 24300 uzssico 29546 qqhre 30064 ballotlemfc0 30554 ballotlemfcc 30555 ballotlemiex 30563 erdszelem4 31176 erdszelem8 31180 supfz 31613 inffz 31614 inffzOLD 31615 poimirlem31 33440 poimirlem32 33441 irrapxlem1 37386 monotuz 37506 monotoddzzfi 37507 rmyeq0 37520 rmyeq 37521 lermy 37522 fzisoeu 39514 fzssre 39529 uzfissfz 39542 ssuzfz 39565 uzssre 39620 zssxr 39621 uzssre2 39633 uzred 39670 uzinico 39787 ioodvbdlimc1lem2 40147 ioodvbdlimc2lem 40149 dvnprodlem1 40161 fourierdlem25 40349 fourierdlem37 40361 fourierdlem52 40375 fourierdlem64 40387 fourierdlem79 40402 etransclem48 40499 hoicvr 40762 |
Copyright terms: Public domain | W3C validator |