![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluzelz | GIF version |
Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
Ref | Expression |
---|---|
eluzelz | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2 9569 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
2 | 1 | simp2bi 1015 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 class class class wbr 4021 ‘cfv 5238 ≤ cle 8028 ℤcz 9288 ℤ≥cuz 9563 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4139 ax-pow 4195 ax-pr 4230 ax-cnex 7937 ax-resscn 7938 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-sbc 2978 df-un 3148 df-in 3150 df-ss 3157 df-pw 3595 df-sn 3616 df-pr 3617 df-op 3619 df-uni 3828 df-br 4022 df-opab 4083 df-mpt 4084 df-id 4314 df-xp 4653 df-rel 4654 df-cnv 4655 df-co 4656 df-dm 4657 df-rn 4658 df-res 4659 df-ima 4660 df-iota 5199 df-fun 5240 df-fn 5241 df-f 5242 df-fv 5246 df-ov 5903 df-neg 8166 df-z 9289 df-uz 9564 |
This theorem is referenced by: eluzelre 9573 uztrn 9580 uzneg 9582 uzssz 9583 uzss 9584 eluzp1l 9588 eluzaddi 9590 eluzsubi 9591 eluzadd 9592 eluzsub 9593 uzm1 9594 uzin 9596 uzind4 9624 uz2mulcl 9644 elfz5 10053 elfzel2 10059 elfzelz 10061 eluzfz2 10068 peano2fzr 10073 fzsplit2 10086 fzopth 10097 fzsuc 10105 elfzp1 10108 fzdifsuc 10117 uzsplit 10128 uzdisj 10129 fzm1 10136 fzneuz 10137 uznfz 10139 nn0disj 10174 elfzo3 10199 fzoss2 10208 fzouzsplit 10215 eluzgtdifelfzo 10233 fzosplitsnm1 10245 fzofzp1b 10264 elfzonelfzo 10266 fzosplitsn 10269 fzisfzounsn 10272 mulp1mod1 10402 m1modge3gt1 10408 frec2uzltd 10440 frecfzen2 10464 uzennn 10473 uzsinds 10481 seq3fveq2 10508 seq3feq2 10509 seq3shft2 10512 monoord 10515 monoord2 10516 ser3mono 10517 seq3split 10518 iseqf1olemjpcl 10534 iseqf1olemqpcl 10535 seq3f1olemqsumk 10538 seq3f1olemp 10541 seq3f1oleml 10542 seq3f1o 10543 seq3id 10547 seq3z 10550 fser0const 10556 leexp2a 10613 expnlbnd2 10686 hashfz 10842 hashfzo 10843 hashfzp1 10845 seq3coll 10863 seq3shft 10888 rexuz3 11040 r19.2uz 11043 cau4 11166 caubnd2 11167 clim 11330 climshft2 11355 climaddc1 11378 climmulc2 11380 climsubc1 11381 climsubc2 11382 clim2ser 11386 clim2ser2 11387 iserex 11388 climlec2 11390 climub 11393 climcau 11396 climcaucn 11400 serf0 11401 sumrbdclem 11426 fsum3cvg 11427 summodclem2a 11430 zsumdc 11433 fsum3 11436 fisumss 11441 fsum3cvg2 11443 fsum3ser 11446 fsumcl2lem 11447 fsumadd 11455 fsumm1 11465 fzosump1 11466 fsum1p 11467 fsump1 11469 fsummulc2 11497 telfsumo 11515 fsumparts 11519 iserabs 11524 binomlem 11532 isumshft 11539 isumsplit 11540 isumrpcl 11543 divcnv 11546 trireciplem 11549 geosergap 11555 geolim2 11561 cvgratnnlemseq 11575 cvgratnnlemabsle 11576 cvgratnnlemsumlt 11577 cvgratnnlemrate 11579 cvgratz 11581 cvgratgt0 11582 mertenslemi1 11584 clim2divap 11589 prodrbdclem 11620 fproddccvg 11621 prodmodclem3 11624 prodmodclem2a 11625 zproddc 11628 fprodntrivap 11633 fprodssdc 11639 fprodm1 11647 fprod1p 11648 fprodp1 11649 fprodabs 11665 fprodeq0 11666 efgt1p2 11744 modm1div 11848 zsupcllemstep 11987 infssuzex 11991 suprzubdc 11994 dvdsbnd 11998 uzwodc 12079 ncoprmgcdne1b 12132 isprm3 12161 prmind2 12163 nprm 12166 dvdsprm 12180 exprmfct 12181 isprm5lem 12184 isprm5 12185 phibndlem 12259 phibnd 12260 dfphi2 12263 hashdvds 12264 pclemdc 12331 pcaddlem 12382 pcmptdvds 12388 pcfac 12393 expnprm 12396 fngsum 12875 igsumvalx 12876 gsumval2 12883 gsumsplit1r 12884 relogbval 14854 relogbzcl 14855 nnlogbexp 14862 logblt 14865 logbgcd1irr 14870 lgsne0 14925 2sqlem6 14953 2sqlem8a 14955 2sqlem8 14956 supfz 15307 |
Copyright terms: Public domain | W3C validator |