![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzssuz | Structured version Visualization version GIF version |
Description: A finite set of sequential integers is a subset of an upper set of integers. (Contributed by NM, 28-Oct-2005.) |
Ref | Expression |
---|---|
fzssuz | ⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz 12529 | . 2 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) | |
2 | 1 | ssriv 3746 | 1 ⊢ (𝑀...𝑁) ⊆ (ℤ≥‘𝑀) |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3713 ‘cfv 6047 (class class class)co 6811 ℤ≥cuz 11877 ...cfz 12517 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-8 2139 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-sep 4931 ax-nul 4939 ax-pow 4990 ax-pr 5053 ax-un 7112 ax-cnex 10182 ax-resscn 10183 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-eu 2609 df-mo 2610 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-ral 3053 df-rex 3054 df-rab 3057 df-v 3340 df-sbc 3575 df-csb 3673 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-pw 4302 df-sn 4320 df-pr 4322 df-op 4326 df-uni 4587 df-iun 4672 df-br 4803 df-opab 4863 df-mpt 4880 df-id 5172 df-xp 5270 df-rel 5271 df-cnv 5272 df-co 5273 df-dm 5274 df-rn 5275 df-res 5276 df-ima 5277 df-iota 6010 df-fun 6049 df-fn 6050 df-f 6051 df-fv 6055 df-ov 6814 df-oprab 6815 df-mpt2 6816 df-1st 7331 df-2nd 7332 df-neg 10459 df-z 11568 df-uz 11878 df-fz 12518 |
This theorem is referenced by: fzssnn 12576 fzof 12659 ltwefz 12954 seqcoll2 13439 caubnd 14295 climsup 14597 summolem2a 14643 fsumss 14653 fsumsers 14656 isumclim3 14687 binomlem 14758 prodmolem2a 14861 fprodntriv 14869 fprodss 14875 iprodclim3 14928 fprodefsum 15022 isprm3 15596 2prm 15605 prmreclem5 15824 4sqlem11 15859 vdwnnlem1 15899 gsumval3 18506 telgsums 18588 fz2ssnn0 29854 esumpcvgval 30447 esumcvg 30455 eulerpartlemsv3 30730 ballotlemfc0 30861 ballotlemfcc 30862 ballotlemiex 30870 ballotlemsdom 30880 ballotlemsima 30884 ballotlemrv2 30890 fsum2dsub 30992 erdszelem4 31481 erdszelem8 31485 volsupnfl 33765 sdclem2 33849 geomcau 33866 diophin 37836 irrapxlem1 37886 fzssnn0 40029 iuneqfzuzlem 40046 fzossuz 40094 uzublem 40153 climinf 40339 sge0uzfsumgt 41162 iundjiun 41178 caratheodorylem1 41244 |
Copyright terms: Public domain | W3C validator |