![]() |
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 12086 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
2 | 1 | baibd 540 | 1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2079 class class class wbr 4956 ‘cfv 6217 ≤ cle 10511 ℤcz 11818 ℤ≥cuz 12082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pr 5214 ax-cnex 10428 ax-resscn 10429 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1079 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-sbc 3702 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-iota 6181 df-fun 6219 df-fv 6225 df-ov 7010 df-neg 10709 df-z 11819 df-uz 12083 |
This theorem is referenced by: uzneg 12101 uztric 12104 uzwo3 12181 fzn 12762 fzsplit2 12771 fznn 12814 uzsplit 12818 elfz2nn0 12837 fzouzsplit 12910 faclbnd 13488 bcval5 13516 fz1isolem 13655 seqcoll 13658 rexuzre 14534 caurcvg 14855 caucvg 14857 summolem2a 14893 fsum0diaglem 14952 climcnds 15027 mertenslem1 15061 ntrivcvgmullem 15078 prodmolem2a 15109 ruclem10 15413 eulerthlem2 15936 pcpremul 15997 pcdvdsb 16022 pcadd 16042 pcfac 16052 pcbc 16053 prmunb 16067 prmreclem5 16073 vdwnnlem3 16150 lt6abl 18724 ovolunlem1a 23768 mbflimsup 23938 plyco0 24453 plyeq0lem 24471 aannenlem1 24588 aaliou3lem2 24603 aaliou3lem8 24605 chtublem 25457 bcmax 25524 bpos1lem 25528 bposlem1 25530 axlowdimlem16 26414 fzsplit3 30175 ballotlem2 31319 ballotlemimin 31336 breprexplemc 31476 elfzm12 32471 poimirlem3 34372 poimirlem4 34373 poimirlem28 34397 mblfinlem2 34407 incsequz 34501 incsequz2 34502 nacsfix 38744 ellz1 38799 eluzrabdioph 38839 monotuz 38974 expdiophlem1 39054 nznngen 40138 fzisoeu 41061 fmul01 41357 climsuselem1 41384 climsuse 41385 iblspltprt 41753 itgspltprt 41759 wallispilem5 41850 stirlinglem8 41862 dirkertrigeqlem1 41879 fourierdlem12 41900 ssfz12 42984 |
Copyright terms: Public domain | W3C validator |