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 9300 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
2 | 1 | simp2bi 982 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1465 class class class wbr 3899 ‘cfv 5093 ≤ cle 7769 ℤcz 9022 ℤ≥cuz 9294 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-14 1477 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-pow 4068 ax-pr 4101 ax-cnex 7679 ax-resscn 7680 |
This theorem depends on definitions: df-bi 116 df-3or 948 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-eu 1980 df-mo 1981 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-rex 2399 df-rab 2402 df-v 2662 df-sbc 2883 df-un 3045 df-in 3047 df-ss 3054 df-pw 3482 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-opab 3960 df-mpt 3961 df-id 4185 df-xp 4515 df-rel 4516 df-cnv 4517 df-co 4518 df-dm 4519 df-rn 4520 df-res 4521 df-ima 4522 df-iota 5058 df-fun 5095 df-fn 5096 df-f 5097 df-fv 5101 df-ov 5745 df-neg 7904 df-z 9023 df-uz 9295 |
This theorem is referenced by: eluzelre 9304 uztrn 9310 uzneg 9312 uzssz 9313 uzss 9314 eluzp1l 9318 eluzaddi 9320 eluzsubi 9321 eluzadd 9322 eluzsub 9323 uzm1 9324 uzin 9326 uzind4 9351 uz2mulcl 9370 elfz5 9766 elfzel2 9772 elfzelz 9774 eluzfz2 9780 peano2fzr 9785 fzsplit2 9798 fzopth 9809 fzsuc 9817 elfzp1 9820 fzdifsuc 9829 uzsplit 9840 uzdisj 9841 fzm1 9848 fzneuz 9849 uznfz 9851 nn0disj 9883 elfzo3 9908 fzoss2 9917 fzouzsplit 9924 eluzgtdifelfzo 9942 fzosplitsnm1 9954 fzofzp1b 9973 elfzonelfzo 9975 fzosplitsn 9978 fzisfzounsn 9981 mulp1mod1 10106 m1modge3gt1 10112 frec2uzltd 10144 frecfzen2 10168 uzennn 10177 uzsinds 10183 seq3fveq2 10210 seq3feq2 10211 seq3shft2 10214 monoord 10217 monoord2 10218 ser3mono 10219 seq3split 10220 iseqf1olemjpcl 10236 iseqf1olemqpcl 10237 seq3f1olemqsumk 10240 seq3f1olemp 10243 seq3f1oleml 10244 seq3f1o 10245 seq3id 10249 seq3z 10252 fser0const 10257 leexp2a 10314 expnlbnd2 10385 hashfz 10535 hashfzo 10536 hashfzp1 10538 seq3coll 10553 seq3shft 10578 rexuz3 10730 r19.2uz 10733 cau4 10856 caubnd2 10857 clim 11018 climshft2 11043 climaddc1 11066 climmulc2 11068 climsubc1 11069 climsubc2 11070 clim2ser 11074 clim2ser2 11075 iserex 11076 climlec2 11078 climub 11081 climcau 11084 climcaucn 11088 serf0 11089 sumrbdclem 11113 fsum3cvg 11114 summodclem2a 11118 zsumdc 11121 fsum3 11124 fisumss 11129 fsum3cvg2 11131 fsum3ser 11134 fsumcl2lem 11135 fsumadd 11143 fsumm1 11153 fzosump1 11154 fsum1p 11155 fsump1 11157 fsummulc2 11185 telfsumo 11203 fsumparts 11207 iserabs 11212 binomlem 11220 isumshft 11227 isumsplit 11228 isumrpcl 11231 divcnv 11234 trireciplem 11237 geosergap 11243 geolim2 11249 cvgratnnlemseq 11263 cvgratnnlemabsle 11264 cvgratnnlemsumlt 11265 cvgratnnlemrate 11267 cvgratz 11269 cvgratgt0 11270 mertenslemi1 11272 efgt1p2 11328 zsupcllemstep 11565 infssuzex 11569 dvdsbnd 11572 ncoprmgcdne1b 11697 isprm3 11726 prmind2 11728 nprm 11731 dvdsprm 11744 exprmfct 11745 phibndlem 11819 phibnd 11820 dfphi2 11823 hashdvds 11824 supfz 13164 |
Copyright terms: Public domain | W3C validator |