![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluzle | Unicode 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 9088 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simp3bi 961 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 3965 ax-pow 4017 ax-pr 4047 ax-cnex 7499 ax-resscn 7500 |
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 2624 df-sbc 2844 df-un 3006 df-in 3008 df-ss 3015 df-pw 3437 df-sn 3458 df-pr 3459 df-op 3461 df-uni 3662 df-br 3854 df-opab 3908 df-mpt 3909 df-id 4131 df-xp 4460 df-rel 4461 df-cnv 4462 df-co 4463 df-dm 4464 df-rn 4465 df-res 4466 df-ima 4467 df-iota 4995 df-fun 5032 df-fn 5033 df-f 5034 df-fv 5038 df-ov 5671 df-neg 7719 df-z 8814 df-uz 9083 |
This theorem is referenced by: uztrn 9098 uzneg 9100 uzss 9102 uz11 9104 eluzp1l 9106 uzm1 9112 uzin 9114 uzind4 9139 elfz5 9495 elfzle1 9504 elfzle2 9505 elfzle3 9507 uzsplit 9569 uzdisj 9570 uznfz 9580 elfz2nn0 9589 uzsubfz0 9603 nn0disj 9612 fzouzdisj 9654 elfzonelfzo 9704 mulp1mod1 9835 m1modge3gt1 9841 seq3split 9970 seq3f1olemqsumk 9991 seq3f1o 9996 iseqcoll 10310 seq3shft 10335 cvg1nlemcau 10480 resqrexlemcvg 10515 resqrexlemga 10519 isummolem2a 10834 fisum 10841 fsum3 10842 fsum3cvg3 10852 fsumadd 10863 sumsnf 10866 fsummulc2 10905 isumshft 10947 divcnv 10954 geolim2 10969 cvgratnnlemseq 10983 cvgratnnlemsumlt 10985 cvgratz 10989 mertenslemi1 10992 efcllemp 11011 infssuzex 11286 dvdsbnd 11289 ncoprmgcdne1b 11412 hashdvds 11538 |
Copyright terms: Public domain | W3C validator |