Description: A prefix of a subword is a subword. (Contributed by AV, 2-Apr-2018) (Revised by AV, 8-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pfxswrd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovexd | |
|
2 | elfznn0 | |
|
3 | pfxval | |
|
4 | 1 2 3 | syl2an | |
5 | fznn0sub | |
|
6 | 5 | 3ad2ant3 | |
7 | 0elfz | |
|
8 | 6 7 | syl | |
9 | 8 | anim1i | |
10 | swrdswrd | |
|
11 | 10 | imp | |
12 | 9 11 | syldan | |
13 | elfznn0 | |
|
14 | nn0cn | |
|
15 | 14 | addid1d | |
16 | 13 15 | syl | |
17 | 16 | 3ad2ant3 | |
18 | 17 | adantr | |
19 | 18 | opeq1d | |
20 | 19 | oveq2d | |
21 | 4 12 20 | 3eqtrd | |
22 | 21 | ex | |