![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elfzel2 | Unicode version |
Description: Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzel2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuz3 9500 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eluzelz 9091 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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-in1 580 ax-in2 581 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-setind 4368 ax-cnex 7499 ax-resscn 7500 |
This theorem depends on definitions: df-bi 116 df-3or 926 df-3an 927 df-tru 1293 df-fal 1296 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-ne 2257 df-ral 2365 df-rex 2366 df-rab 2369 df-v 2624 df-sbc 2844 df-dif 3004 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-oprab 5672 df-mpt2 5673 df-neg 7719 df-z 8814 df-uz 9083 df-fz 9488 |
This theorem is referenced by: elfz1eq 9512 fzdisj 9529 fzssp1 9544 fzp1disj 9557 fzrev2i 9563 fzrev3 9564 fznuz 9579 fznn0sub2 9602 elfzmlbm 9605 difelfznle 9609 nn0disj 9612 fzofzp1b 9702 iseqf1olemqcl 9978 iseqf1olemab 9981 iseqf1olemqf1o 9985 iseqf1olemqk 9986 iseqf1olemjpcl 9987 iseqf1olemqpcl 9988 iseqf1olemfvp 9989 seq3f1olemqsumkj 9990 seq3f1olemqsumk 9991 seq3f1olemqsum 9992 seq3f1olemstep 9993 bcm1k 10231 bcp1nk 10233 |
Copyright terms: Public domain | W3C validator |