![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elfzuz3 | Structured version Visualization 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 11794 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 466 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-1st 6793 df-2nd 6794 df-neg 9863 df-z 10938 df-uz 11160 df-fz 11785 |
This theorem is referenced by: elfzel2 11798 elfzle2 11803 peano2fzr 11812 fzsplit2 11824 fzsplit 11825 fznn0sub 11831 fzopth 11835 fzss1 11837 fzss2 11838 fzp1elp1 11849 predfz 11914 fzosplit 11951 fzoend 12002 fzofzp1b 12009 uzindi 12194 seqcl2 12231 seqfveq2 12235 monoord 12243 sermono 12245 seqsplit 12246 seqf1olem2 12253 seqid2 12259 seqhomo 12260 seqz 12261 bcval5 12503 seqcoll 12627 seqcoll2 12628 swrdval2 12776 swrd0val 12777 swrd0len 12778 spllen 12861 splfv2a 12863 fsum0diag2 13844 climcndslem2 13908 prodfn0 13950 lcmslefacOLD 14586 lcmflefac 14621 pcbc 14845 vdwlem2 14932 vdwlem5 14935 vdwlem6 14936 vdwlem8 14938 prmgaplem1 15007 psgnunilem5 17135 efgsres 17388 efgredleme 17393 efgcpbllemb 17405 imasdsf1olem 21388 volsup 22509 dvn2bss 22884 dvtaylp 23325 wilth 23996 ftalem1 23997 ppisval2 24031 dvdsppwf1o 24115 logfaclbnd 24150 bposlem6 24217 eupares 25703 fzsplit3 28370 ballotlemsima 29348 ballotlemfrc 29359 ballotlemfrceq 29361 ballotlemsimaOLD 29386 ballotlemfrcOLD 29397 ballotlemfrceqOLD 29399 fzssfzo 29422 wrdres 29426 signstres 29464 erdszelem7 29920 erdszelem8 29921 poimirlem1 31941 poimirlem2 31942 poimirlem3 31943 poimirlem4 31944 poimirlem7 31947 poimirlem12 31952 poimirlem15 31955 poimirlem16 31956 poimirlem17 31957 poimirlem19 31959 poimirlem20 31960 poimirlem23 31963 poimirlem24 31964 poimirlem25 31965 poimirlem29 31969 poimirlem31 31971 mettrifi 32086 bcc0 36689 fmulcl 37659 fmul01lt1lem2 37663 dvnprodlem2 37822 stoweidlem11 37871 stoweidlem17 37877 fourierdlem15 37984 smonoord 38718 pfxres 38929 pfxf 38930 repswpfx 38977 ssfz12 39054 |
Copyright terms: Public domain | W3C validator |