![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eluz | Structured version Visualization version 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 12859 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
2 | 1 | baibd 538 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 class class class wbr 5149 ‘cfv 6549 ≤ cle 11281 ℤcz 12591 ℤ≥cuz 12855 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 ax-cnex 11196 ax-resscn 11197 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-iota 6501 df-fun 6551 df-fv 6557 df-ov 7422 df-neg 11479 df-z 12592 df-uz 12856 |
This theorem is referenced by: uzneg 12875 uztric 12879 uzwo3 12960 fzn 13552 fzsplit2 13561 fznn 13604 uzsplit 13608 elfz2nn0 13627 fzouzsplit 13702 faclbnd 14285 bcval5 14313 fz1isolem 14458 seqcoll 14461 rexuzre 15335 caurcvg 15659 caucvg 15661 summolem2a 15697 fsum0diaglem 15758 climcnds 15833 mertenslem1 15866 ntrivcvgmullem 15883 prodmolem2a 15914 ruclem10 16219 eulerthlem2 16754 pcpremul 16815 pcdvdsb 16841 pcadd 16861 pcfac 16871 pcbc 16872 prmunb 16886 prmreclem5 16892 vdwnnlem3 16969 lt6abl 19862 ovolunlem1a 25469 mbflimsup 25639 plyco0 26171 plyeq0lem 26189 aannenlem1 26308 aaliou3lem2 26323 aaliou3lem8 26325 chtublem 27189 bcmax 27256 bpos1lem 27260 bposlem1 27262 axlowdimlem16 28840 fzsplit3 32644 cycpmco2lem7 32945 ballotlem2 34239 ballotlemimin 34256 breprexplemc 34395 elfzm12 35410 poimirlem3 37227 poimirlem4 37228 poimirlem28 37252 mblfinlem2 37262 incsequz 37352 incsequz2 37353 aks4d1p1 41679 primrootspoweq0 41709 aks6d1c2 41733 sticksstones12a 41760 sticksstones12 41761 aks6d1c6lem3 41775 nacsfix 42274 ellz1 42329 eluzrabdioph 42368 monotuz 42504 expdiophlem1 42584 nznngen 43895 fzisoeu 44820 fmul01 45106 climsuselem1 45133 climsuse 45134 iblspltprt 45499 itgspltprt 45505 wallispilem5 45595 stirlinglem8 45607 dirkertrigeqlem1 45624 fourierdlem12 45645 ssfz12 46832 |
Copyright terms: Public domain | W3C validator |