Metamath Proof Explorer


Theorem iswrdi

Description: A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion iswrdi W : 0 ..^ L S W Word S

Proof

Step Hyp Ref Expression
1 oveq2 l = L 0 ..^ l = 0 ..^ L
2 1 feq2d l = L W : 0 ..^ l S W : 0 ..^ L S
3 2 rspcev L 0 W : 0 ..^ L S l 0 W : 0 ..^ l S
4 0nn0 0 0
5 fzo0n0 0 ..^ L L
6 nnnn0 L L 0
7 5 6 sylbi 0 ..^ L L 0
8 7 necon1bi ¬ L 0 0 ..^ L =
9 fzo0 0 ..^ 0 =
10 8 9 eqtr4di ¬ L 0 0 ..^ L = 0 ..^ 0
11 10 feq2d ¬ L 0 W : 0 ..^ L S W : 0 ..^ 0 S
12 11 biimpa ¬ L 0 W : 0 ..^ L S W : 0 ..^ 0 S
13 oveq2 l = 0 0 ..^ l = 0 ..^ 0
14 13 feq2d l = 0 W : 0 ..^ l S W : 0 ..^ 0 S
15 14 rspcev 0 0 W : 0 ..^ 0 S l 0 W : 0 ..^ l S
16 4 12 15 sylancr ¬ L 0 W : 0 ..^ L S l 0 W : 0 ..^ l S
17 3 16 pm2.61ian W : 0 ..^ L S l 0 W : 0 ..^ l S
18 iswrd W Word S l 0 W : 0 ..^ l S
19 17 18 sylibr W : 0 ..^ L S W Word S