Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elfzuz3 | Structured version Visualization version GIF version |
Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzuz3 | ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuzb 12892 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
2 | 1 | simprbi 497 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ‘cfv 6349 (class class class)co 7145 ℤ≥cuz 12232 ...cfz 12882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 ax-cnex 10582 ax-resscn 10583 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-iun 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-fv 6357 df-ov 7148 df-oprab 7149 df-mpo 7150 df-1st 7680 df-2nd 7681 df-neg 10862 df-z 11971 df-uz 12233 df-fz 12883 |
This theorem is referenced by: elfzel2 12896 elfzle2 12901 peano2fzr 12910 fzsplit2 12922 fzsplit 12923 fznn0sub 12929 fzopth 12934 fzss1 12936 fzss2 12937 fzp1elp1 12950 predfz 13022 fzosplit 13060 fzoend 13118 fzofzp1b 13125 uzindi 13340 seqcl2 13378 seqfveq2 13382 monoord 13390 sermono 13392 seqsplit 13393 seqf1olem2 13400 seqid2 13406 seqhomo 13407 seqz 13408 bcval5 13668 seqcoll 13812 seqcoll2 13813 swrdval2 13998 pfxres 14031 pfxf 14032 spllen 14106 splfv2a 14108 repswpfx 14137 fsum0diag2 15128 climcndslem2 15195 prodfn0 15240 lcmflefac 15982 pcbc 16226 vdwlem2 16308 vdwlem5 16311 vdwlem6 16312 vdwlem8 16314 prmgaplem1 16375 psgnunilem5 18553 efgsres 18795 efgredleme 18800 efgcpbllemb 18812 imasdsf1olem 22912 volsup 24086 dvn2bss 24456 dvtaylp 24887 wilth 25576 ftalem1 25578 ppisval2 25610 dvdsppwf1o 25691 logfaclbnd 25726 bposlem6 25793 wlkres 27380 fzsplit3 30444 wrdres 30541 pfxf1 30546 swrdrn2 30556 swrdrn3 30557 swrdf1 30558 swrdrndisj 30559 splfv3 30560 cycpmco2f1 30694 cycpmco2rn 30695 cycpmco2lem7 30702 ballotlemsima 31673 ballotlemfrc 31684 ballotlemfrceq 31686 fzssfzo 31709 signstres 31745 fsum2dsub 31778 revpfxsfxrev 32260 swrdrevpfx 32261 pfxwlk 32268 erdszelem7 32342 erdszelem8 32343 poimirlem1 34775 poimirlem2 34776 poimirlem3 34777 poimirlem4 34778 poimirlem7 34781 poimirlem12 34786 poimirlem15 34789 poimirlem16 34790 poimirlem17 34791 poimirlem19 34793 poimirlem20 34794 poimirlem23 34797 poimirlem24 34798 poimirlem25 34799 poimirlem29 34803 poimirlem31 34805 mettrifi 34915 bcc0 40552 iunincfi 41240 monoordxrv 41638 fmulcl 41742 fmul01lt1lem2 41746 dvnprodlem2 42112 stoweidlem11 42177 stoweidlem17 42183 fourierdlem15 42288 ssfz12 43395 smonoord 43412 |
Copyright terms: Public domain | W3C validator |