Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eluz1 | Structured version Visualization version GIF version |
Description: Membership in the upper set of integers starting at 𝑀. (Contributed by NM, 5-Sep-2005.) |
Ref | Expression |
---|---|
eluz1 | ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzval 12234 | . . 3 ⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) = {𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘}) | |
2 | 1 | eleq2d 2898 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑁 ∈ {𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘})) |
3 | breq2 5062 | . . 3 ⊢ (𝑘 = 𝑁 → (𝑀 ≤ 𝑘 ↔ 𝑀 ≤ 𝑁)) | |
4 | 3 | elrab 3679 | . 2 ⊢ (𝑁 ∈ {𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘} ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
5 | 2, 4 | syl6bb 288 | 1 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 {crab 3142 class class class wbr 5058 ‘cfv 6349 ≤ cle 10665 ℤcz 11970 ℤ≥cuz 12232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 ax-cnex 10582 ax-resscn 10583 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fv 6357 df-ov 7148 df-neg 10862 df-z 11971 df-uz 12233 |
This theorem is referenced by: eluz2 12238 eluz1i 12240 eluz 12246 uzid 12247 uzss 12254 eluzp1m1 12257 raluz 12285 rexuz 12287 preduz 13019 fi1uzind 13845 algcvga 15913 uzssico 30434 nndiffz1 30436 fzspl 30440 cycpmco2lem6 30701 cycpmconjslem2 30725 breprexplemc 31803 lzunuz 39245 |
Copyright terms: Public domain | W3C validator |