![]() |
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 12521 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
2 | 1 | simprbi 483 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2131 ‘cfv 6041 (class class class)co 6805 ℤ≥cuz 11871 ...cfz 12511 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-cnex 10176 ax-resscn 10177 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-fv 6049 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-1st 7325 df-2nd 7326 df-neg 10453 df-z 11562 df-uz 11872 df-fz 12512 |
This theorem is referenced by: elfzel2 12525 elfzle2 12530 peano2fzr 12539 fzsplit2 12551 fzsplit 12552 fznn0sub 12558 fzopth 12563 fzss1 12565 fzss2 12566 fzp1elp1 12579 predfz 12650 fzosplit 12687 fzoend 12745 fzofzp1b 12752 uzindi 12967 seqcl2 13005 seqfveq2 13009 monoord 13017 sermono 13019 seqsplit 13020 seqf1olem2 13027 seqid2 13033 seqhomo 13034 seqz 13035 bcval5 13291 seqcoll 13432 seqcoll2 13433 swrdval2 13611 swrd0val 13612 swrd0len 13613 spllen 13697 splfv2a 13699 fsum0diag2 14706 climcndslem2 14773 prodfn0 14817 lcmflefac 15555 pcbc 15798 vdwlem2 15880 vdwlem5 15883 vdwlem6 15884 vdwlem8 15886 prmgaplem1 15947 psgnunilem5 18106 efgsres 18343 efgredleme 18348 efgcpbllemb 18360 imasdsf1olem 22371 volsup 23516 dvn2bss 23884 dvtaylp 24315 wilth 24988 ftalem1 24990 ppisval2 25022 dvdsppwf1o 25103 logfaclbnd 25138 bposlem6 25205 wlkres 26769 fzsplit3 29854 ballotlemsima 30878 ballotlemfrc 30889 ballotlemfrceq 30891 fzssfzo 30914 wrdres 30918 signstres 30953 fsum2dsub 30986 erdszelem7 31478 erdszelem8 31479 poimirlem1 33715 poimirlem2 33716 poimirlem3 33717 poimirlem4 33718 poimirlem7 33721 poimirlem12 33726 poimirlem15 33729 poimirlem16 33730 poimirlem17 33731 poimirlem19 33733 poimirlem20 33734 poimirlem23 33737 poimirlem24 33738 poimirlem25 33739 poimirlem29 33743 poimirlem31 33745 mettrifi 33858 bcc0 39033 iunincfi 39763 monoordxrv 40202 fmulcl 40308 fmul01lt1lem2 40312 dvnprodlem2 40657 stoweidlem11 40723 stoweidlem17 40729 fourierdlem15 40834 ssfz12 41826 smonoord 41843 pfxres 41890 pfxf 41891 repswpfx 41938 |
Copyright terms: Public domain | W3C validator |