![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluz | GIF version |
Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
Ref | Expression |
---|---|
eluz | ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz1 9422 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
2 | 1 | baibd 909 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∈ wcel 2125 class class class wbr 3961 ‘cfv 5163 ≤ cle 7892 ℤcz 9146 ℤ≥cuz 9418 |
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-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-14 2128 ax-ext 2136 ax-sep 4078 ax-pow 4130 ax-pr 4164 ax-cnex 7802 ax-resscn 7803 |
This theorem depends on definitions: df-bi 116 df-3or 964 df-3an 965 df-tru 1335 df-nf 1438 df-sb 1740 df-eu 2006 df-mo 2007 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-ral 2437 df-rex 2438 df-rab 2441 df-v 2711 df-sbc 2934 df-un 3102 df-in 3104 df-ss 3111 df-pw 3541 df-sn 3562 df-pr 3563 df-op 3565 df-uni 3769 df-br 3962 df-opab 4022 df-mpt 4023 df-id 4248 df-xp 4585 df-rel 4586 df-cnv 4587 df-co 4588 df-dm 4589 df-iota 5128 df-fun 5165 df-fv 5171 df-ov 5817 df-neg 8028 df-z 9147 df-uz 9419 |
This theorem is referenced by: uzneg 9436 uztric 9439 uzm1 9448 eluzdc 9499 fzn 9922 fzsplit2 9930 fznn 9969 uzsplit 9972 elfz2nn0 9992 fzouzsplit 10056 exfzdc 10117 fzfig 10307 faclbnd 10592 seq3coll 10690 cvg1nlemcau 10861 cvg1nlemres 10862 summodclem2a 11255 fsum0diaglem 11314 mertenslemi1 11409 prodmodclem2a 11450 zsupcllemstep 11805 zsupcl 11807 infssuzex 11809 uzdcinzz 13310 |
Copyright terms: Public domain | W3C validator |