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 11693 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
2 | 1 | simp3bi 1078 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1990 class class class wbr 4653 ‘cfv 5888 ≤ cle 10075 ℤcz 11377 ℤ≥cuz 11687 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-cnex 9992 ax-resscn 9993 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fv 5896 df-ov 6653 df-neg 10269 df-z 11378 df-uz 11688 |
This theorem is referenced by: uztrn 11704 uzneg 11706 uzss 11708 uz11 11710 eluzp1l 11712 uzm1 11718 uzin 11720 uzind4 11746 uzwo 11751 uzsupss 11780 zgt1rpn0n1 11871 elfz5 12334 elfzle1 12344 elfzle2 12345 elfzle3 12347 elfz1uz 12410 uzsplit 12412 uzdisj 12413 uznfz 12423 elfz2nn0 12431 uzsubfz0 12447 nn0disj 12455 fzouzdisj 12504 fldiv4lem1div2uz2 12637 m1modge3gt1 12717 expmulnbnd 12996 seqcoll 13248 swrdlen2 13445 swrdfv2 13446 rexuzre 14092 rlimclim1 14276 isercoll 14398 iseralt 14415 o1fsum 14545 mertenslem1 14616 fprodeq0 14705 efcllem 14808 rpnnen2lem9 14951 smuval2 15204 smupvallem 15205 isprm7 15420 hashdvds 15480 pcmpt2 15597 pcfaclem 15602 pcfac 15603 vdwlem6 15690 ramtlecl 15704 prmlem1 15814 prmlem2 15827 znfld 19909 lmnn 23061 mbflimsup 23433 mbfi1fseqlem6 23487 dvfsumge 23785 plyco0 23948 coeeulem 23980 radcnvlem2 24168 log2tlbnd 24672 lgamgulmlem4 24758 lgamcvg2 24781 chtub 24937 chpval2 24943 chpchtsum 24944 bcmax 25003 bpos1lem 25007 bpos1 25008 bposlem3 25011 bposlem4 25012 bposlem5 25013 bposlem6 25014 lgslem1 25022 lgsdirprm 25056 lgseisen 25104 m1lgs 25113 dchrisumlema 25177 dchrisumlem2 25179 dchrisum0lem1 25205 axlowdimlem3 25824 axlowdimlem6 25827 axlowdimlem7 25828 axlowdimlem16 25837 axlowdimlem17 25838 minvecolem3 27732 minvecolem4 27736 breprexplemc 30710 subfacval3 31171 climuzcnv 31565 knoppndvlem6 32508 poimirlem29 33438 fdc 33541 jm2.24nn 37526 jm2.23 37563 expdiophlem1 37588 hashnzfz2 38520 bccbc 38544 binomcxplemnn0 38548 ssinc 39264 ssdec 39265 fzdifsuc2 39525 uzfissfz 39542 iuneqfzuzlem 39550 ssuzfz 39565 uzublem 39657 uzinico 39787 fmul01lt1lem1 39816 climsuselem1 39839 climsuse 39840 limsupubuzlem 39944 limsupequzlem 39954 limsupmnfuzlem 39958 limsupre3uzlem 39967 ioodvbdlimc1lem2 40147 ioodvbdlimc2lem 40149 iblspltprt 40189 itgspltprt 40195 stoweidlem11 40228 stirlinglem11 40301 fourierdlem79 40402 fourierdlem103 40426 fourierdlem104 40427 vonioolem1 40894 fmtnoprmfac1 41477 fmtnoprmfac2lem1 41478 lighneallem2 41523 lighneallem4a 41525 gboge9 41652 bgoldbnnsum3prm 41692 nnolog2flm1 42384 |
Copyright terms: Public domain | W3C validator |