| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > eluzle | 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 9654 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
| 2 | 1 | simp3bi 1017 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2176 class class class wbr 4044 ‘cfv 5271 ≤ cle 8108 ℤcz 9372 ℤ≥cuz 9648 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 ax-cnex 8016 ax-resscn 8017 |
| This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-rab 2493 df-v 2774 df-sbc 2999 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-br 4045 df-opab 4106 df-mpt 4107 df-id 4340 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-fv 5279 df-ov 5947 df-neg 8246 df-z 9373 df-uz 9649 |
| This theorem is referenced by: uztrn 9665 uzneg 9667 uzss 9669 uz11 9671 eluzp1l 9673 uzm1 9679 uzin 9681 uzind4 9709 elfz5 10139 elfzle1 10149 elfzle2 10150 elfzle3 10152 uzsplit 10214 uzdisj 10215 uznfz 10225 elfz2nn0 10234 uzsubfz0 10251 nn0disj 10260 fzouzdisj 10304 elfzonelfzo 10359 infssuzex 10376 suprzubdc 10379 fldiv4lem1div2uz2 10449 mulp1mod1 10510 m1modge3gt1 10516 uzennn 10581 seq3split 10633 seq3f1olemqsumk 10657 seq3f1o 10662 seq3coll 10987 swrdlen2 11115 swrdfv2 11116 seq3shft 11149 cvg1nlemcau 11295 resqrexlemcvg 11330 resqrexlemga 11334 summodclem2a 11692 fsum3 11698 fsum3cvg3 11707 fsumadd 11717 sumsnf 11720 fsummulc2 11759 isumshft 11801 divcnv 11808 geolim2 11823 cvgratnnlemseq 11837 cvgratnnlemsumlt 11839 cvgratz 11843 mertenslemi1 11846 prodmodclem3 11886 prodmodclem2a 11887 fprodntrivap 11895 prodsnf 11903 fprodeq0 11928 efcllemp 11969 dvdsbnd 12277 uzwodc 12358 ncoprmgcdne1b 12411 isprm5 12464 hashdvds 12543 pcmpt2 12667 pcfaclem 12672 pcfac 12673 nninfdclemp1 12821 strext 12937 gsumfzval 13223 znidom 14419 lgslem1 15477 lgsdirprm 15511 lgseisen 15551 cvgcmp2nlemabs 15971 |
| Copyright terms: Public domain | W3C validator |