Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elfzel2 | Structured version Visualization version GIF version |
Description: Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzel2 | ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz3 12988 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | |
2 | eluzelz 12327 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 ‘cfv 6333 (class class class)co 7164 ℤcz 12055 ℤ≥cuz 12317 ...cfz 12974 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 ax-un 7473 ax-cnex 10664 ax-resscn 10665 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-iun 4880 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-fv 6341 df-ov 7167 df-oprab 7168 df-mpo 7169 df-1st 7707 df-2nd 7708 df-neg 10944 df-z 12056 df-uz 12318 df-fz 12975 |
This theorem is referenced by: elfz1eq 13002 fzdisj 13018 fzssp1 13034 fzp1disj 13050 fzrev2i 13056 fzrev3 13057 elfz1b 13060 fznuz 13073 fznn0sub2 13098 elfzmlbm 13101 difelfznle 13105 nn0disj 13107 fz1fzo0m1 13169 fzofzp1b 13219 bcm1k 13760 bcp1nk 13762 pfxccatin12lem2 14175 spllen 14198 fsum0diag2 15224 fallfacval3 15451 fallfacval4 15482 psgnunilem2 18734 pntpbnd1 26314 crctcshwlkn0 27751 fzm1ne1 30677 swrdrevpfx 32641 swrdwlk 32651 elfzfzo 42336 sumnnodd 42697 dvnmul 43010 dvnprodlem1 43013 dvnprodlem2 43014 stoweidlem34 43101 fourierdlem11 43185 fourierdlem12 43186 fourierdlem15 43189 fourierdlem41 43215 fourierdlem48 43221 fourierdlem49 43222 fourierdlem54 43227 fourierdlem79 43252 fourierdlem102 43275 fourierdlem114 43287 etransclem23 43324 etransclem35 43336 iundjiun 43524 2elfz2melfz 44328 elfzelfzlble 44331 iccpartiltu 44392 iccpartgt 44397 |
Copyright terms: Public domain | W3C validator |