Description: A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 2-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pfxn0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lbfzo0 | |
|
2 | ne0i | |
|
3 | 1 2 | sylbir | |
4 | 3 | 3ad2ant2 | |
5 | simp1 | |
|
6 | nnnn0 | |
|
7 | 6 | 3ad2ant2 | |
8 | lencl | |
|
9 | 8 | 3ad2ant1 | |
10 | simp3 | |
|
11 | elfz2nn0 | |
|
12 | 7 9 10 11 | syl3anbrc | |
13 | pfxf | |
|
14 | 5 12 13 | syl2anc | |
15 | f0dom0 | |
|
16 | 15 | bicomd | |
17 | 14 16 | syl | |
18 | 17 | necon3bid | |
19 | 4 18 | mpbird | |