Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elfzle2 | GIF version |
Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzle2 | ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz3 9982 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾)) | |
2 | eluzle 9503 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑁) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2142 class class class wbr 3990 ‘cfv 5200 (class class class)co 5857 ≤ cle 7959 ℤ≥cuz 9491 ...cfz 9969 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-14 2145 ax-ext 2153 ax-sep 4108 ax-pow 4161 ax-pr 4195 ax-setind 4522 ax-cnex 7869 ax-resscn 7870 |
This theorem depends on definitions: df-bi 116 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-ral 2454 df-rex 2455 df-rab 2458 df-v 2733 df-sbc 2957 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-br 3991 df-opab 4052 df-mpt 4053 df-id 4279 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-fv 5208 df-ov 5860 df-oprab 5861 df-mpo 5862 df-neg 8097 df-z 9217 df-uz 9492 df-fz 9970 |
This theorem is referenced by: elfz1eq 9995 fzdisj 10012 fznatpl1 10036 fzp1disj 10040 uzdisj 10053 fzneuz 10061 fznuz 10062 elfzmlbm 10091 difelfznle 10095 nn0disj 10098 iseqf1olemqcl 10446 iseqf1olemnab 10448 iseqf1olemab 10449 iseqf1olemqk 10454 iseqf1olemfvp 10457 seq3f1olemqsumkj 10458 seq3f1olemqsumk 10459 seq3f1olemqsum 10460 seq3f1oleml 10463 seq3f1o 10464 bcval4 10690 bcp1nk 10700 zfz1isolemiso 10778 seq3coll 10781 summodclem3 11347 summodclem2a 11348 fsum3 11354 fsumcl2lem 11365 fsum0diaglem 11407 mertenslemi1 11502 prodmodclem3 11542 prodmodclem2a 11543 fprodseq 11550 fzm1ndvds 11820 prmind2 12078 prmdvdsfz 12097 isprm5lem 12099 hashdvds 12179 eulerthlemrprm 12187 eulerthlema 12188 prmdiveq 12194 ennnfonelemim 12383 ctinfomlemom 12386 lgsval2lem 13790 supfz 14185 |
Copyright terms: Public domain | W3C validator |