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 12439 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
2 | 1 | baibd 543 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2110 class class class wbr 5050 ‘cfv 6377 ≤ cle 10865 ℤcz 12173 ℤ≥cuz 12435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 ax-cnex 10782 ax-resscn 10783 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3063 df-rex 3064 df-rab 3067 df-v 3407 df-dif 3866 df-un 3868 df-in 3870 df-ss 3880 df-nul 4235 df-if 4437 df-sn 4539 df-pr 4541 df-op 4545 df-uni 4817 df-br 5051 df-opab 5113 df-mpt 5133 df-id 5452 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-iota 6335 df-fun 6379 df-fv 6385 df-ov 7213 df-neg 11062 df-z 12174 df-uz 12436 |
This theorem is referenced by: uzneg 12455 uztric 12459 uzwo3 12536 fzn 13125 fzsplit2 13134 fznn 13177 uzsplit 13181 elfz2nn0 13200 fzouzsplit 13274 faclbnd 13853 bcval5 13881 fz1isolem 14024 seqcoll 14027 rexuzre 14913 caurcvg 15237 caucvg 15239 summolem2a 15276 fsum0diaglem 15337 climcnds 15412 mertenslem1 15445 ntrivcvgmullem 15462 prodmolem2a 15493 ruclem10 15797 eulerthlem2 16332 pcpremul 16393 pcdvdsb 16419 pcadd 16439 pcfac 16449 pcbc 16450 prmunb 16464 prmreclem5 16470 vdwnnlem3 16547 lt6abl 19277 ovolunlem1a 24390 mbflimsup 24560 plyco0 25083 plyeq0lem 25101 aannenlem1 25218 aaliou3lem2 25233 aaliou3lem8 25235 chtublem 26089 bcmax 26156 bpos1lem 26160 bposlem1 26162 axlowdimlem16 27045 fzsplit3 30832 cycpmco2lem7 31115 ballotlem2 32164 ballotlemimin 32181 breprexplemc 32321 elfzm12 33343 poimirlem3 35515 poimirlem4 35516 poimirlem28 35540 mblfinlem2 35550 incsequz 35641 incsequz2 35642 aks4d1p1 39815 sticksstones12a 39833 sticksstones12 39834 nacsfix 40235 ellz1 40290 eluzrabdioph 40329 monotuz 40464 expdiophlem1 40544 nznngen 41605 fzisoeu 42510 fmul01 42794 climsuselem1 42821 climsuse 42822 iblspltprt 43187 itgspltprt 43193 wallispilem5 43283 stirlinglem8 43295 dirkertrigeqlem1 43312 fourierdlem12 43333 ssfz12 44477 |
Copyright terms: Public domain | W3C validator |