![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > elfzuz3 | Structured version Unicode version |
Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
elfzuz3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuzb 11563 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 464 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-ral 2803 df-rex 2804 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-op 3991 df-uni 4199 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-id 4743 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-fv 5533 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-1st 6686 df-2nd 6687 df-neg 9708 df-z 10757 df-uz 10972 df-fz 11554 |
This theorem is referenced by: elfzel2 11567 elfzle2 11571 peano2fzr 11579 fzsplit2 11590 fzsplit 11591 fznn0sub 11603 fzopth 11611 fzss1 11613 fzss2 11614 fzp1elp1 11625 fzosplit 11698 fzoend 11734 fzofzp1b 11741 uzindi 11919 seqcl2 11940 seqfveq2 11944 monoord 11952 sermono 11954 seqsplit 11955 seqf1olem2 11962 seqid2 11968 seqhomo 11969 seqz 11970 bcval5 12210 seqcoll 12333 seqcoll2 12334 swrdval2 12433 swrd0val 12434 swrd0len 12435 spllen 12513 splfv2a 12515 fsum0diag2 13367 climcndslem2 13430 pcbc 14079 vdwlem2 14160 vdwlem5 14163 vdwlem6 14164 vdwlem8 14166 psgnunilem5 16118 efgsres 16355 efgredleme 16360 efgcpbllemb 16372 imasdsf1olem 20079 volsup 21169 dvn2bss 21536 dvtaylp 21967 wilth 22541 ftalem1 22542 ppisval2 22574 dvdsppwf1o 22658 logfaclbnd 22693 bposlem6 22760 eupares 23747 fzsplit3 26222 ballotlemsima 27041 ballotlemfrc 27052 ballotlemfrceq 27054 fzssfzo 27077 wrdres 27081 signstres 27119 erdszelem7 27228 erdszelem8 27229 prodfn0 27552 predfz 27807 mettrifi 28800 fmulcl 29909 fmul01lt1lem2 29913 stoweidlem11 29953 stoweidlem17 29959 ssfz12 30344 |
Copyright terms: Public domain | W3C validator |