![]() |
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 12593 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | |
2 | eluzelz 11940 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝑁 ∈ ℤ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 ‘cfv 6101 (class class class)co 6878 ℤcz 11666 ℤ≥cuz 11930 ...cfz 12580 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-cnex 10280 ax-resscn 10281 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-fv 6109 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-1st 7401 df-2nd 7402 df-neg 10559 df-z 11667 df-uz 11931 df-fz 12581 |
This theorem is referenced by: elfz1eq 12606 fzdisj 12622 fzssp1 12638 fzp1disj 12653 fzrev2i 12659 fzrev3 12660 elfz1b 12663 fznuz 12676 fznn0sub2 12701 elfzmlbm 12704 difelfznle 12708 nn0disj 12710 fz1fzo0m1 12771 fzofzp1b 12821 bcm1k 13355 bcp1nk 13357 pfxccatin12lem2 13792 swrdccatin12lem2OLD 13793 spllen 13830 spllenOLD 13831 fsum0diag2 14853 fallfacval3 15079 fallfacval4 15110 psgnunilem2 18228 pntpbnd1 25627 crctcshwlkn0 27072 elfzfzo 40230 sumnnodd 40602 dvnmul 40898 dvnprodlem1 40901 dvnprodlem2 40902 stoweidlem34 40990 fourierdlem11 41074 fourierdlem12 41075 fourierdlem15 41078 fourierdlem41 41104 fourierdlem48 41110 fourierdlem49 41111 fourierdlem54 41116 fourierdlem79 41141 fourierdlem102 41164 fourierdlem114 41176 etransclem23 41213 etransclem35 41225 iundjiun 41416 2elfz2melfz 42164 elfzelfzlble 42167 iccpartiltu 42194 iccpartgt 42199 |
Copyright terms: Public domain | W3C validator |