![]() |
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 9086 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) | |
2 | 1 | simp2bi 960 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 class class class wbr 3851 ‘cfv 5028 ≤ cle 7584 ℤcz 8811 ℤ≥cuz 9080 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-14 1451 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-pow 4015 ax-pr 4045 ax-cnex 7497 ax-resscn 7498 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-eu 1952 df-mo 1953 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-rex 2366 df-rab 2369 df-v 2622 df-sbc 2842 df-un 3004 df-in 3006 df-ss 3013 df-pw 3435 df-sn 3456 df-pr 3457 df-op 3459 df-uni 3660 df-br 3852 df-opab 3906 df-mpt 3907 df-id 4129 df-xp 4458 df-rel 4459 df-cnv 4460 df-co 4461 df-dm 4462 df-rn 4463 df-res 4464 df-ima 4465 df-iota 4993 df-fun 5030 df-fn 5031 df-f 5032 df-fv 5036 df-ov 5669 df-neg 7717 df-z 8812 df-uz 9081 |
This theorem is referenced by: eluzelre 9090 uztrn 9096 uzneg 9098 uzssz 9099 uzss 9100 eluzp1l 9104 eluzaddi 9106 eluzsubi 9107 eluzadd 9108 eluzsub 9109 uzm1 9110 uzin 9112 uzind4 9137 uz2mulcl 9156 elfz5 9493 elfzel2 9499 elfzelz 9501 eluzfz2 9507 peano2fzr 9512 fzsplit2 9525 fzopth 9536 fzsuc 9544 elfzp1 9547 fzdifsuc 9556 uzsplit 9567 uzdisj 9568 fzm1 9575 fzneuz 9576 uznfz 9578 nn0disj 9610 elfzo3 9635 fzoss2 9644 fzouzsplit 9651 eluzgtdifelfzo 9669 fzosplitsnm1 9681 fzofzp1b 9700 elfzonelfzo 9702 fzosplitsn 9705 fzisfzounsn 9708 mulp1mod1 9833 m1modge3gt1 9839 frec2uzltd 9871 frecfzen2 9895 uzsinds 9909 iseqfveq2 9951 iseqfeq2 9952 seq3fveq2 9953 seq3feq2 9954 iseqshft2 9959 monoord 9965 monoord2 9966 isermono 9967 seq3split 9968 iseqsplit 9969 iseqf1olemjpcl 9985 iseqf1olemqpcl 9986 seq3f1olemqsumk 9989 seq3f1olemp 9992 seq3f1oleml 9993 seq3f1o 9994 iseqid 10000 iseqz 10004 fser0const 10012 leexp2a 10069 expnlbnd2 10140 hashfz 10290 hashfzo 10291 hashfzp1 10293 iseqcoll 10308 seq3shft 10333 rexuz3 10484 r19.2uz 10487 cau4 10610 caubnd2 10611 clim 10730 climshft2 10756 climaddc1 10778 climmulc2 10780 climsubc1 10781 climsubc2 10782 clim2ser 10786 clim2ser2 10787 iserex 10788 climlec2 10791 climub 10794 climcau 10797 climcaucn 10801 serf0 10802 isumrblem 10826 fisumcvg 10827 fsum3cvg 10828 isummolem2a 10832 zisum 10835 fisum 10839 fsum3 10840 fisumss 10845 fisumcvg2 10847 fsum3cvg2 10848 fisumser 10851 fsumcl2lem 10853 fsumadd 10861 fsumm1 10871 fzosump1 10872 fsum1p 10873 fsump1 10875 fsummulc2 10903 telfsumo 10921 fsumparts 10925 iserabs 10930 binomlem 10938 isumshft 10945 isumsplit 10946 isumrpcl 10949 divcnv 10952 trireciplem 10955 geosergap 10961 geolim2 10967 cvgratnnlemseq 10981 cvgratnnlemabsle 10982 cvgratnnlemsumlt 10983 cvgratnnlemrate 10985 cvgratz 10987 cvgratgt0 10988 mertenslemi1 10990 efgt1p2 11046 zsupcllemstep 11280 infssuzex 11284 dvdsbnd 11287 ncoprmgcdne1b 11410 isprm3 11439 prmind2 11441 nprm 11444 dvdsprm 11457 exprmfct 11458 phibndlem 11531 phibnd 11532 dfphi2 11535 hashdvds 11536 supfz 12188 |
Copyright terms: Public domain | W3C validator |