![]() |
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 13495 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
2 | 1 | simprbi 498 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ‘cfv 6544 (class class class)co 7409 ℤ≥cuz 12822 ...cfz 13484 |
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 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-ov 7412 df-oprab 7413 df-mpo 7414 df-1st 7975 df-2nd 7976 df-neg 11447 df-z 12559 df-uz 12823 df-fz 13485 |
This theorem is referenced by: elfzel2 13499 elfzle2 13505 peano2fzr 13514 fzsplit2 13526 fzsplit 13527 fznn0sub 13533 fzopth 13538 fzss1 13540 fzss2 13541 fzp1elp1 13554 predfz 13626 fzosplit 13665 fzoend 13723 fzofzp1b 13730 uzindi 13947 seqcl2 13986 seqfveq2 13990 monoord 13998 sermono 14000 seqsplit 14001 seqf1olem2 14008 seqid2 14014 seqhomo 14015 seqz 14016 bcval5 14278 seqcoll 14425 seqcoll2 14426 swrdval2 14596 pfxres 14629 pfxf 14630 spllen 14704 splfv2a 14706 repswpfx 14735 fsum0diag2 15729 climcndslem2 15796 prodfn0 15840 lcmflefac 16585 pcbc 16833 vdwlem2 16915 vdwlem5 16918 vdwlem6 16919 vdwlem8 16921 prmgaplem1 16982 psgnunilem5 19362 efgsres 19606 efgredleme 19611 efgcpbllemb 19623 imasdsf1olem 23879 volsup 25073 dvn2bss 25447 dvtaylp 25882 wilth 26575 ftalem1 26577 ppisval2 26609 dvdsppwf1o 26690 logfaclbnd 26725 bposlem6 26792 wlkres 28958 fzsplit3 32036 wrdres 32134 pfxf1 32139 swrdrn2 32149 swrdrn3 32150 swrdf1 32151 swrdrndisj 32152 splfv3 32153 cycpmco2f1 32314 cycpmco2rn 32315 cycpmco2lem7 32322 ballotlemsima 33545 ballotlemfrc 33556 ballotlemfrceq 33558 fzssfzo 33581 signstres 33617 fsum2dsub 33650 revpfxsfxrev 34137 swrdrevpfx 34138 pfxwlk 34145 erdszelem7 34219 erdszelem8 34220 poimirlem1 36537 poimirlem2 36538 poimirlem3 36539 poimirlem4 36540 poimirlem7 36543 poimirlem12 36548 poimirlem15 36551 poimirlem16 36552 poimirlem17 36553 poimirlem19 36555 poimirlem20 36556 poimirlem23 36559 poimirlem24 36560 poimirlem25 36561 poimirlem29 36565 poimirlem31 36567 mettrifi 36673 fzsplitnd 40896 bcc0 43147 iunincfi 43831 monoordxrv 44240 fmulcl 44345 fmul01lt1lem2 44349 dvnprodlem2 44711 stoweidlem11 44775 stoweidlem17 44781 fourierdlem15 44886 ssfz12 46070 smonoord 46087 |
Copyright terms: Public domain | W3C validator |