Step | Hyp | Ref
| Expression |
1 | | sseqval.1 |
. . 3
|
2 | | sseqval.2 |
. . 3
Word |
3 | | sseqval.3 |
. . 3
Word |
4 | | sseqval.4 |
. . 3
|
5 | | sseqfv2.4 |
. . 3
|
6 | 1, 2, 3, 4, 5 | sseqfv2 30456 |
. 2
seqstr lastS ++ ++ |
7 | | fveq2 6191 |
. . . . . . 7
++ ++ ++ ++ |
8 | | oveq2 6658 |
. . . . . . . . 9
..^ ..^ |
9 | 8 | reseq2d 5396 |
. . . . . . . 8
seqstr ..^ seqstr
..^ |
10 | 9 | fveq2d 6195 |
. . . . . . . . 9
seqstr ..^ seqstr ..^ |
11 | 10 | s1eqd 13381 |
. . . . . . . 8
seqstr ..^ seqstr ..^ |
12 | 9, 11 | oveq12d 6668 |
. . . . . . 7
seqstr ..^ ++ seqstr ..^
seqstr ..^ ++ seqstr ..^ |
13 | 7, 12 | eqeq12d 2637 |
. . . . . 6
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr
..^ ++ seqstr ..^ |
14 | 13 | imbi2d 330 |
. . . . 5
++
++ seqstr ..^ ++ seqstr ..^
++ ++ seqstr
..^ ++ seqstr ..^ |
15 | | fveq2 6191 |
. . . . . . 7
++ ++
++
++ |
16 | | oveq2 6658 |
. . . . . . . . 9
..^ ..^ |
17 | 16 | reseq2d 5396 |
. . . . . . . 8
seqstr ..^ seqstr
..^ |
18 | 17 | fveq2d 6195 |
. . . . . . . . 9
seqstr ..^ seqstr
..^ |
19 | 18 | s1eqd 13381 |
. . . . . . . 8
seqstr ..^ seqstr ..^ |
20 | 17, 19 | oveq12d 6668 |
. . . . . . 7
seqstr ..^ ++ seqstr
..^ seqstr
..^ ++ seqstr ..^ |
21 | 15, 20 | eqeq12d 2637 |
. . . . . 6
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ ++ seqstr ..^ |
22 | 21 | imbi2d 330 |
. . . . 5
++ ++ seqstr ..^ ++ seqstr ..^
++ ++ seqstr ..^ ++ seqstr ..^ |
23 | | fveq2 6191 |
. . . . . . 7
++ ++
++
++ |
24 | | oveq2 6658 |
. . . . . . . . 9
..^ ..^ |
25 | 24 | reseq2d 5396 |
. . . . . . . 8
seqstr ..^ seqstr
..^ |
26 | 25 | fveq2d 6195 |
. . . . . . . . 9
seqstr ..^ seqstr
..^ |
27 | 26 | s1eqd 13381 |
. . . . . . . 8
seqstr ..^ seqstr ..^ |
28 | 25, 27 | oveq12d 6668 |
. . . . . . 7
seqstr ..^ ++ seqstr
..^ seqstr
..^ ++ seqstr ..^ |
29 | 23, 28 | eqeq12d 2637 |
. . . . . 6
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ ++ seqstr ..^ |
30 | 29 | imbi2d 330 |
. . . . 5
++ ++ seqstr ..^ ++ seqstr ..^
++ ++ seqstr ..^ ++ seqstr ..^ |
31 | | fveq2 6191 |
. . . . . . 7
++ ++
++
++ |
32 | | oveq2 6658 |
. . . . . . . . 9
..^ ..^ |
33 | 32 | reseq2d 5396 |
. . . . . . . 8
seqstr ..^ seqstr
..^ |
34 | 33 | fveq2d 6195 |
. . . . . . . . 9
seqstr ..^ seqstr
..^ |
35 | 34 | s1eqd 13381 |
. . . . . . . 8
seqstr ..^ seqstr ..^ |
36 | 33, 35 | oveq12d 6668 |
. . . . . . 7
seqstr ..^ ++ seqstr
..^ seqstr
..^ ++ seqstr ..^ |
37 | 31, 36 | eqeq12d 2637 |
. . . . . 6
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ ++ seqstr ..^ |
38 | 37 | imbi2d 330 |
. . . . 5
++ ++ seqstr ..^ ++ seqstr ..^
++ ++ seqstr ..^ ++ seqstr ..^ |
39 | | ovex 6678 |
. . . . . . . 8
++
|
40 | | lencl 13324 |
. . . . . . . . 9
Word |
41 | 2, 40 | syl 17 |
. . . . . . . 8
|
42 | | fvconst2g 6467 |
. . . . . . . 8
++ ++ ++ |
43 | 39, 41, 42 | sylancr 695 |
. . . . . . 7
++ ++ |
44 | 40 | nn0zd 11480 |
. . . . . . . 8
Word |
45 | | seq1 12814 |
. . . . . . . 8
++ ++ ++ |
46 | 2, 44, 45 | 3syl 18 |
. . . . . . 7
++ ++ ++ |
47 | 1, 2, 3, 4 | sseqfres 30455 |
. . . . . . . 8
seqstr ..^ |
48 | 47 | fveq2d 6195 |
. . . . . . . . 9
seqstr ..^ |
49 | 48 | s1eqd 13381 |
. . . . . . . 8
seqstr
..^ |
50 | 47, 49 | oveq12d 6668 |
. . . . . . 7
seqstr
..^ ++ seqstr ..^ ++ |
51 | 43, 46, 50 | 3eqtr4d 2666 |
. . . . . 6
++ ++ seqstr
..^ ++ seqstr ..^ |
52 | 51 | a1i 11 |
. . . . 5
++ ++ seqstr
..^ ++ seqstr ..^ |
53 | | seqp1 12816 |
. . . . . . . . . . . 12
++
++ ++ ++
++
++ |
54 | 53 | adantl 482 |
. . . . . . . . . . 11
++ ++ ++ ++
++
++ |
55 | | id 22 |
. . . . . . . . . . . . . . 15
|
56 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | s1eqd 13381 |
. . . . . . . . . . . . . . 15
|
58 | 55, 57 | oveq12d 6668 |
. . . . . . . . . . . . . 14
++ ++ |
59 | | eqidd 2623 |
. . . . . . . . . . . . . 14
++ ++ |
60 | 58, 59 | cbvmpt2v 6735 |
. . . . . . . . . . . . 13
++ ++ |
61 | 60 | a1i 11 |
. . . . . . . . . . . 12
++
++
|
62 | | simprl 794 |
. . . . . . . . . . . . 13
++ ++ ++
++ ++ |
63 | 62 | fveq2d 6195 |
. . . . . . . . . . . . . 14
++ ++ ++
++ ++ |
64 | 63 | s1eqd 13381 |
. . . . . . . . . . . . 13
++ ++ ++
++ ++ |
65 | 62, 64 | oveq12d 6668 |
. . . . . . . . . . . 12
++ ++ ++
++
++ ++ ++ ++ ++ |
66 | | fvexd 6203 |
. . . . . . . . . . . 12
++ ++ |
67 | | fvexd 6203 |
. . . . . . . . . . . 12
++ |
68 | | ovex 6678 |
. . . . . . . . . . . . 13
++ ++ ++ ++ ++ |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
++
++ ++ ++ ++ |
70 | 61, 65, 66, 67, 69 | ovmpt2d 6788 |
. . . . . . . . . . 11
++
++
++
++ ++ ++ ++ ++ ++ |
71 | 54, 70 | eqtrd 2656 |
. . . . . . . . . 10
++ ++ ++ ++ ++ ++ ++ |
72 | 71 | adantr 481 |
. . . . . . . . 9
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ ++ ++ ++ ++ ++ |
73 | 1 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
74 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word |
75 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
76 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
77 | 73, 74, 3, 75, 76 | sseqfv2 30456 |
. . . . . . . . . . . . . . 15
seqstr lastS ++ ++ |
78 | 77 | adantr 481 |
. . . . . . . . . . . . . 14
++ ++ seqstr ..^ ++ seqstr ..^ seqstr lastS ++ ++ |
79 | | simpr 477 |
. . . . . . . . . . . . . . 15
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ ++ seqstr ..^ |
80 | 79 | fveq2d 6195 |
. . . . . . . . . . . . . 14
++ ++ seqstr ..^ ++ seqstr ..^ lastS ++ ++ lastS seqstr ..^ ++ seqstr
..^ |
81 | 1, 2, 3, 4 | sseqf 30454 |
. . . . . . . . . . . . . . . . . . 19
seqstr |
82 | | fzo0ssnn0 12548 |
. . . . . . . . . . . . . . . . . . 19
..^ |
83 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . 19
seqstr ..^
seqstr ..^..^ |
84 | 81, 82, 83 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
seqstr ..^..^ |
85 | | iswrdi 13309 |
. . . . . . . . . . . . . . . . . 18
seqstr ..^..^ seqstr ..^ Word |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . 17
seqstr ..^ Word |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . 16
seqstr ..^ Word |
88 | | elex 3212 |
. . . . . . . . . . . . . . . . . . . . 21
seqstr ..^ Word seqstr ..^ |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
seqstr ..^ |
90 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
seqstr |
91 | | eluznn0 11757 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
92 | 41, 91 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . 22
|
93 | 73, 90, 92 | subiwrdlen 30448 |
. . . . . . . . . . . . . . . . . . . . 21
seqstr ..^ |
94 | 93, 76 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . 20
seqstr ..^ |
95 | | hashf 13125 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . 21
seqstr ..^
seqstr ..^ seqstr
..^ |
98 | 95, 96, 97 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
seqstr ..^
seqstr ..^ seqstr
..^ |
99 | 89, 94, 98 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . 19
seqstr ..^ |
100 | 87, 99 | elind 3798 |
. . . . . . . . . . . . . . . . . 18
seqstr ..^ Word |
101 | 100, 3 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
seqstr ..^ |
102 | 75, 101 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
seqstr ..^ |
103 | | lswccats1 13411 |
. . . . . . . . . . . . . . . 16
seqstr ..^ Word seqstr ..^ lastS
seqstr ..^ ++ seqstr ..^ seqstr ..^ |
104 | 87, 102, 103 | syl2anc 693 |
. . . . . . . . . . . . . . 15
lastS seqstr ..^ ++ seqstr ..^ seqstr ..^ |
105 | 104 | adantr 481 |
. . . . . . . . . . . . . 14
++ ++ seqstr ..^ ++ seqstr ..^ lastS seqstr
..^ ++ seqstr ..^ seqstr
..^ |
106 | 78, 80, 105 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
++ ++ seqstr ..^ ++ seqstr ..^ seqstr ..^ seqstr |
107 | 106 | s1eqd 13381 |
. . . . . . . . . . . 12
++ ++ seqstr ..^ ++ seqstr ..^ seqstr ..^ seqstr |
108 | 107 | oveq2d 6666 |
. . . . . . . . . . 11
++ ++ seqstr ..^ ++ seqstr ..^ seqstr ..^ ++ seqstr
..^ seqstr
..^ ++ seqstr |
109 | 73, 90, 92 | iwrdsplit 30449 |
. . . . . . . . . . . 12
seqstr ..^ seqstr ..^ ++ seqstr |
110 | 109 | adantr 481 |
. . . . . . . . . . 11
++ ++ seqstr ..^ ++ seqstr ..^ seqstr ..^ seqstr ..^ ++ seqstr |
111 | 108, 79, 110 | 3eqtr4d 2666 |
. . . . . . . . . 10
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr
..^ |
112 | 111 | fveq2d 6195 |
. . . . . . . . . . 11
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ |
113 | 112 | s1eqd 13381 |
. . . . . . . . . 10
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ |
114 | 111, 113 | oveq12d 6668 |
. . . . . . . . 9
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ ++ ++ ++ seqstr ..^ ++ seqstr ..^ |
115 | 72, 114 | eqtrd 2656 |
. . . . . . . 8
++ ++ seqstr ..^ ++ seqstr ..^ ++ ++ seqstr ..^ ++ seqstr ..^ |
116 | 115 | ex 450 |
. . . . . . 7
++
++ seqstr ..^ ++ seqstr ..^
++
++ seqstr ..^ ++ seqstr ..^ |
117 | 116 | expcom 451 |
. . . . . 6
++ ++ seqstr ..^ ++ seqstr ..^
++
++ seqstr ..^ ++ seqstr ..^ |
118 | 117 | a2d 29 |
. . . . 5
++ ++ seqstr ..^ ++ seqstr ..^
++
++ seqstr ..^ ++ seqstr ..^ |
119 | 14, 22, 30, 38, 52, 118 | uzind4 11746 |
. . . 4
++ ++ seqstr ..^ ++ seqstr ..^ |
120 | 5, 119 | mpcom 38 |
. . 3
++ ++ seqstr ..^ ++ seqstr ..^ |
121 | 120 | fveq2d 6195 |
. 2
lastS ++ ++ lastS seqstr ..^ ++ seqstr ..^ |
122 | | fzo0ssnn0 12548 |
. . . . 5
..^ |
123 | | fssres 6070 |
. . . . 5
seqstr ..^
seqstr ..^..^ |
124 | 81, 122, 123 | sylancl 694 |
. . . 4
seqstr ..^..^ |
125 | | iswrdi 13309 |
. . . 4
seqstr ..^..^ seqstr ..^ Word |
126 | 124, 125 | syl 17 |
. . 3
seqstr ..^ Word |
127 | | elex 3212 |
. . . . . . . 8
seqstr ..^ Word seqstr ..^ |
128 | 126, 127 | syl 17 |
. . . . . . 7
seqstr ..^ |
129 | | eluznn0 11757 |
. . . . . . . . . 10
|
130 | 41, 5, 129 | syl2anc 693 |
. . . . . . . . 9
|
131 | 1, 81, 130 | subiwrdlen 30448 |
. . . . . . . 8
seqstr ..^ |
132 | 131, 5 | eqeltrd 2701 |
. . . . . . 7
seqstr ..^ |
133 | | elpreima 6337 |
. . . . . . . 8
seqstr ..^
seqstr ..^ seqstr
..^ |
134 | 95, 96, 133 | mp2b 10 |
. . . . . . 7
seqstr ..^
seqstr ..^ seqstr
..^ |
135 | 128, 132,
134 | sylanbrc 698 |
. . . . . 6
seqstr ..^ |
136 | 126, 135 | elind 3798 |
. . . . 5
seqstr ..^ Word |
137 | 136, 3 | syl6eleqr 2712 |
. . . 4
seqstr ..^ |
138 | 4, 137 | ffvelrnd 6360 |
. . 3
seqstr ..^ |
139 | | lswccats1 13411 |
. . 3
seqstr ..^ Word seqstr ..^ lastS
seqstr ..^ ++ seqstr ..^ seqstr ..^ |
140 | 126, 138,
139 | syl2anc 693 |
. 2
lastS seqstr ..^ ++ seqstr ..^ seqstr ..^ |
141 | 6, 121, 140 | 3eqtrd 2660 |
1
seqstr seqstr ..^ |