![]() |
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 13442 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
2 | 1 | simprbi 498 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ‘cfv 6501 (class class class)co 7362 ℤ≥cuz 12770 ...cfz 13431 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 ax-un 7677 ax-cnex 11114 ax-resscn 11115 |
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-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-sbc 3745 df-csb 3861 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-fv 6509 df-ov 7365 df-oprab 7366 df-mpo 7367 df-1st 7926 df-2nd 7927 df-neg 11395 df-z 12507 df-uz 12771 df-fz 13432 |
This theorem is referenced by: elfzel2 13446 elfzle2 13452 peano2fzr 13461 fzsplit2 13473 fzsplit 13474 fznn0sub 13480 fzopth 13485 fzss1 13487 fzss2 13488 fzp1elp1 13501 predfz 13573 fzosplit 13612 fzoend 13670 fzofzp1b 13677 uzindi 13894 seqcl2 13933 seqfveq2 13937 monoord 13945 sermono 13947 seqsplit 13948 seqf1olem2 13955 seqid2 13961 seqhomo 13962 seqz 13963 bcval5 14225 seqcoll 14370 seqcoll2 14371 swrdval2 14541 pfxres 14574 pfxf 14575 spllen 14649 splfv2a 14651 repswpfx 14680 fsum0diag2 15675 climcndslem2 15742 prodfn0 15786 lcmflefac 16531 pcbc 16779 vdwlem2 16861 vdwlem5 16864 vdwlem6 16865 vdwlem8 16867 prmgaplem1 16928 psgnunilem5 19283 efgsres 19527 efgredleme 19532 efgcpbllemb 19544 imasdsf1olem 23742 volsup 24936 dvn2bss 25310 dvtaylp 25745 wilth 26436 ftalem1 26438 ppisval2 26470 dvdsppwf1o 26551 logfaclbnd 26586 bposlem6 26653 wlkres 28660 fzsplit3 31739 wrdres 31835 pfxf1 31840 swrdrn2 31850 swrdrn3 31851 swrdf1 31852 swrdrndisj 31853 splfv3 31854 cycpmco2f1 32015 cycpmco2rn 32016 cycpmco2lem7 32023 ballotlemsima 33155 ballotlemfrc 33166 ballotlemfrceq 33168 fzssfzo 33191 signstres 33227 fsum2dsub 33260 revpfxsfxrev 33749 swrdrevpfx 33750 pfxwlk 33757 erdszelem7 33831 erdszelem8 33832 poimirlem1 36108 poimirlem2 36109 poimirlem3 36110 poimirlem4 36111 poimirlem7 36114 poimirlem12 36119 poimirlem15 36122 poimirlem16 36123 poimirlem17 36124 poimirlem19 36126 poimirlem20 36127 poimirlem23 36130 poimirlem24 36131 poimirlem25 36132 poimirlem29 36136 poimirlem31 36138 mettrifi 36245 fzsplitnd 40469 bcc0 42694 iunincfi 43378 monoordxrv 43791 fmulcl 43896 fmul01lt1lem2 43900 dvnprodlem2 44262 stoweidlem11 44326 stoweidlem17 44332 fourierdlem15 44437 ssfz12 45620 smonoord 45637 |
Copyright terms: Public domain | W3C validator |