Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eluzle | Structured version Visualization version GIF version |
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
Ref | Expression |
---|---|
eluzle | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2 11569 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
2 | 1 | simp3bi 1071 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 class class class wbr 4583 ‘cfv 5804 ≤ cle 9954 ℤcz 11254 ℤ≥cuz 11563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-cnex 9871 ax-resscn 9872 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-ov 6552 df-neg 10148 df-z 11255 df-uz 11564 |
This theorem is referenced by: uztrn 11580 uzneg 11582 uzss 11584 uz11 11586 eluzp1l 11588 uzm1 11594 uzin 11596 uzind4 11622 uzwo 11627 uzsupss 11656 zgt1rpn0n1 11747 elfz5 12205 elfzle1 12215 elfzle2 12216 elfzle3 12218 ssfzunsn 12257 uzsplit 12281 uzdisj 12282 uznfz 12292 elfz2nn0 12300 uzsubfz0 12316 nn0disj 12324 fzouzdisj 12373 fldiv4lem1div2uz2 12499 m1modge3gt1 12579 expmulnbnd 12858 seqcoll 13105 swrdlen2 13297 swrdfv2 13298 rexuzre 13940 rlimclim1 14124 isercoll 14246 iseralt 14263 o1fsum 14386 mertenslem1 14455 fprodeq0 14544 efcllem 14647 rpnnen2lem9 14790 smuval2 15042 smupvallem 15043 isprm7 15258 hashdvds 15318 pcmpt2 15435 pcfaclem 15440 pcfac 15441 vdwlem6 15528 ramtlecl 15542 prmlem1 15652 prmlem2 15665 znfld 19728 lmnn 22869 mbflimsup 23239 mbfi1fseqlem6 23293 dvfsumge 23589 plyco0 23752 coeeulem 23784 radcnvlem2 23972 log2tlbnd 24472 lgamgulmlem4 24558 lgamcvg2 24581 chtub 24737 chpval2 24743 chpchtsum 24744 bcmax 24803 bpos1lem 24807 bpos1 24808 bposlem3 24811 bposlem4 24812 bposlem5 24813 bposlem6 24814 lgslem1 24822 lgsdirprm 24856 lgseisen 24904 m1lgs 24913 dchrisumlema 24977 dchrisumlem2 24979 dchrisum0lem1 25005 axlowdimlem3 25624 axlowdimlem6 25627 axlowdimlem7 25628 axlowdimlem16 25637 axlowdimlem17 25638 constr3trllem3 26180 minvecolem3 27116 minvecolem4 27120 subfacval3 30425 climuzcnv 30819 knoppndvlem6 31678 poimirlem29 32608 fdc 32711 jm2.24nn 36544 jm2.23 36581 expdiophlem1 36606 hashnzfz2 37542 bccbc 37566 binomcxplemnn0 37570 ssinc 38292 ssdec 38293 fzdifsuc2 38466 uzfissfz 38483 iuneqfzuzlem 38491 ssuzfz 38506 fmul01lt1lem1 38651 climsuselem1 38674 climsuse 38675 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 iblspltprt 38865 itgspltprt 38871 stoweidlem11 38904 stirlinglem11 38977 fourierdlem79 39078 fourierdlem103 39102 fourierdlem104 39103 vonioolem1 39571 fmtnoprmfac1 40015 fmtnoprmfac2lem1 40016 lighneallem2 40061 lighneallem4a 40063 gboage9 40186 bgoldbnnsum3prm 40220 nnolog2flm1 42182 |
Copyright terms: Public domain | W3C validator |