|   | 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 13559 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∈ wcel 2107 ‘cfv 6560 (class class class)co 7432 ℤ≥cuz 12879 ...cfz 13548 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-fv 6568 df-ov 7435 df-oprab 7436 df-mpo 7437 df-1st 8015 df-2nd 8016 df-neg 11496 df-z 12616 df-uz 12880 df-fz 13549 | 
| This theorem is referenced by: elfzel2 13563 elfzle2 13569 peano2fzr 13578 fzsplit2 13590 fzsplit 13591 fznn0sub 13597 fzopth 13602 fzss1 13604 fzss2 13605 fzp1elp1 13618 predfz 13694 fzosplit 13733 fzoend 13797 fzofzp1b 13805 uzindi 14024 seqcl2 14062 seqfveq2 14066 monoord 14074 sermono 14076 seqsplit 14077 seqf1olem2 14084 seqid2 14090 seqhomo 14091 seqz 14092 bcval5 14358 seqcoll 14504 seqcoll2 14505 swrdval2 14685 pfxres 14718 pfxf 14719 spllen 14793 splfv2a 14795 repswpfx 14824 fsum0diag2 15820 climcndslem2 15887 prodfn0 15931 lcmflefac 16686 pcbc 16939 vdwlem2 17021 vdwlem5 17024 vdwlem6 17025 vdwlem8 17027 prmgaplem1 17088 psgnunilem5 19513 efgsres 19757 efgredleme 19762 efgcpbllemb 19774 imasdsf1olem 24384 volsup 25592 dvn2bss 25967 dvtaylp 26413 wilth 27115 ftalem1 27117 ppisval2 27149 dvdsppwf1o 27230 logfaclbnd 27267 bposlem6 27334 wlkres 29689 fzsplit3 32796 wrdres 32920 pfxf1 32927 swrdrn2 32940 swrdrn3 32941 swrdf1 32942 swrdrndisj 32943 splfv3 32944 pfxchn 33000 cycpmco2f1 33145 cycpmco2rn 33146 cycpmco2lem7 33153 ballotlemsima 34519 ballotlemfrc 34530 ballotlemfrceq 34532 fzssfzo 34555 signstres 34591 fsum2dsub 34623 revpfxsfxrev 35122 swrdrevpfx 35123 pfxwlk 35130 erdszelem7 35203 erdszelem8 35204 poimirlem1 37629 poimirlem2 37630 poimirlem3 37631 poimirlem4 37632 poimirlem7 37635 poimirlem12 37640 poimirlem15 37643 poimirlem16 37644 poimirlem17 37645 poimirlem19 37647 poimirlem20 37648 poimirlem23 37651 poimirlem24 37652 poimirlem25 37653 poimirlem29 37657 poimirlem31 37659 mettrifi 37765 fzsplitnd 41984 aks6d1c2lem4 42129 bcc0 44364 iunincfi 45104 monoordxrv 45497 fmulcl 45601 fmul01lt1lem2 45605 dvnprodlem2 45967 stoweidlem11 46031 stoweidlem17 46037 fourierdlem15 46142 ssfz12 47331 smonoord 47363 | 
| Copyright terms: Public domain | W3C validator |