![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elfzuz | GIF version |
Description: A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzuz | ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuzb 10085 | . 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾))) | |
2 | 1 | simplbi 274 | 1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2164 ‘cfv 5254 (class class class)co 5918 ℤ≥cuz 9592 ...cfz 10074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2986 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-br 4030 df-opab 4091 df-mpt 4092 df-id 4324 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-fv 5262 df-ov 5921 df-oprab 5922 df-mpo 5923 df-neg 8193 df-z 9318 df-uz 9593 df-fz 10075 |
This theorem is referenced by: elfzel1 10090 elfzelz 10091 elfzle1 10093 eluzfz2b 10099 fzsplit2 10116 fzsplit 10117 fzopth 10127 fzss1 10129 fzss2 10130 fzssuz 10131 fzp1elp1 10141 uzsplit 10158 elfzmlbm 10197 fzosplit 10244 seq3feq2 10547 seq3feq 10551 ser3mono 10558 seq3caopr3 10562 iseqf1olemkle 10568 iseqf1olemklt 10569 iseqf1olemnab 10572 iseqf1olemqk 10578 iseqf1olemjpcl 10579 iseqf1olemqpcl 10580 iseqf1olemfvp 10581 seq3f1olemqsumkj 10582 seq3f1olemqsumk 10583 seq3f1olemqsum 10584 seq3f1olemstep 10585 seq3f1oleml 10587 seq3f1o 10588 seqf1oglem2 10591 seq3z 10599 ser0 10604 ser3le 10608 seq3coll 10913 climub 11487 sumrbdclem 11520 fsum3cvg 11521 fsum3ser 11540 fsump1i 11576 fsum0diaglem 11583 iserabs 11618 isumsplit 11634 isum1p 11635 geosergap 11649 mertenslemi1 11678 prodf1 11685 prodfap0 11688 prodfrecap 11689 prodfdivap 11690 prodrbdclem 11714 fproddccvg 11715 fprodntrivap 11727 fprodabs 11759 fprodeq0 11760 infssuzex 12086 nninfctlemfo 12177 prmind2 12258 prmdvdsfz 12277 isprm5lem 12279 eulerthlemrprm 12367 eulerthlema 12368 pcfac 12488 lgsdilem2 15152 cvgcmp2nlemabs 15522 |
Copyright terms: Public domain | W3C validator |