![]() |
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 28927 fzsplit3 32005 wrdres 32103 pfxf1 32108 swrdrn2 32118 swrdrn3 32119 swrdf1 32120 swrdrndisj 32121 splfv3 32122 cycpmco2f1 32283 cycpmco2rn 32284 cycpmco2lem7 32291 ballotlemsima 33514 ballotlemfrc 33525 ballotlemfrceq 33527 fzssfzo 33550 signstres 33586 fsum2dsub 33619 revpfxsfxrev 34106 swrdrevpfx 34107 pfxwlk 34114 erdszelem7 34188 erdszelem8 34189 poimirlem1 36489 poimirlem2 36490 poimirlem3 36491 poimirlem4 36492 poimirlem7 36495 poimirlem12 36500 poimirlem15 36503 poimirlem16 36504 poimirlem17 36505 poimirlem19 36507 poimirlem20 36508 poimirlem23 36511 poimirlem24 36512 poimirlem25 36513 poimirlem29 36517 poimirlem31 36519 mettrifi 36625 fzsplitnd 40848 bcc0 43099 iunincfi 43783 monoordxrv 44192 fmulcl 44297 fmul01lt1lem2 44301 dvnprodlem2 44663 stoweidlem11 44727 stoweidlem17 44733 fourierdlem15 44838 ssfz12 46022 smonoord 46039 |
Copyright terms: Public domain | W3C validator |