Step | Hyp | Ref
| Expression |
1 | | sseqval.2 |
. . . 4
Word |
2 | | wrdf 13310 |
. . . 4
Word ..^ |
3 | 1, 2 | syl 17 |
. . 3
..^ |
4 | | vex 3203 |
. . . . . . . . 9
|
5 | 4 | a1i 11 |
. . . . . . . 8
|
6 | | fvex 6201 |
. . . . . . . . 9
|
7 | | df-lsw 13300 |
. . . . . . . . 9
lastS |
8 | 6, 7 | dmmpti 6023 |
. . . . . . . 8
lastS |
9 | 5, 8 | syl6eleqr 2712 |
. . . . . . 7
lastS |
10 | | eldifsn 4317 |
. . . . . . . . 9
|
11 | | sseqval.3 |
. . . . . . . . . . . 12
Word |
12 | | inss1 3833 |
. . . . . . . . . . . 12
Word Word |
13 | 11, 12 | eqsstri 3635 |
. . . . . . . . . . 11
Word |
14 | 13 | sseli 3599 |
. . . . . . . . . 10
Word |
15 | | lswcl 13355 |
. . . . . . . . . 10
Word lastS |
16 | 14, 15 | sylan 488 |
. . . . . . . . 9
lastS |
17 | 10, 16 | sylbi 207 |
. . . . . . . 8
lastS |
18 | 17 | adantl 482 |
. . . . . . 7
lastS |
19 | 9, 18 | jca 554 |
. . . . . 6
lastS lastS |
20 | 19 | ralrimiva 2966 |
. . . . 5
lastS lastS |
21 | 6, 7 | fnmpti 6022 |
. . . . . 6
lastS |
22 | | fnfun 5988 |
. . . . . 6
lastS
lastS |
23 | | ffvresb 6394 |
. . . . . 6
lastS lastS lastS lastS |
24 | 21, 22, 23 | mp2b 10 |
. . . . 5
lastS
lastS lastS |
25 | 20, 24 | sylibr 224 |
. . . 4
lastS |
26 | | eqid 2622 |
. . . . 5
|
27 | | lencl 13324 |
. . . . . . 7
Word |
28 | 27 | nn0zd 11480 |
. . . . . 6
Word |
29 | 1, 28 | syl 17 |
. . . . 5
|
30 | | ovex 6678 |
. . . . . . 7
++
|
31 | | simpr 477 |
. . . . . . . . 9
|
32 | 1, 27 | syl 17 |
. . . . . . . . . . 11
|
33 | 32 | adantr 481 |
. . . . . . . . . 10
|
34 | | elnn0uz 11725 |
. . . . . . . . . 10
|
35 | 33, 34 | sylib 208 |
. . . . . . . . 9
|
36 | | uztrn 11704 |
. . . . . . . . 9
|
37 | 31, 35, 36 | syl2anc 693 |
. . . . . . . 8
|
38 | | nn0uz 11722 |
. . . . . . . 8
|
39 | 37, 38 | syl6eleqr 2712 |
. . . . . . 7
|
40 | | fvconst2g 6467 |
. . . . . . 7
++ ++ ++ |
41 | 30, 39, 40 | sylancr 695 |
. . . . . 6
++ ++ |
42 | | sseqval.4 |
. . . . . . . . . . . . 13
|
43 | | sseqval.1 |
. . . . . . . . . . . . . 14
|
44 | 43, 1, 11, 42 | sseqmw 30453 |
. . . . . . . . . . . . 13
|
45 | 42, 44 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
46 | 45 | s1cld 13383 |
. . . . . . . . . . 11
Word
|
47 | | ccatcl 13359 |
. . . . . . . . . . 11
Word Word ++ Word |
48 | 1, 46, 47 | syl2anc 693 |
. . . . . . . . . 10
++ Word |
49 | 30 | a1i 11 |
. . . . . . . . . . 11
++ |
50 | | ccatws1len 13398 |
. . . . . . . . . . . . 13
Word ++ |
51 | 1, 45, 50 | syl2anc 693 |
. . . . . . . . . . . 12
++ |
52 | | uzid 11702 |
. . . . . . . . . . . . 13
|
53 | | peano2uz 11741 |
. . . . . . . . . . . . 13
|
54 | 29, 52, 53 | 3syl 18 |
. . . . . . . . . . . 12
|
55 | 51, 54 | eqeltrd 2701 |
. . . . . . . . . . 11
++ |
56 | | hashf 13125 |
. . . . . . . . . . . 12
|
57 | | ffn 6045 |
. . . . . . . . . . . 12
|
58 | | elpreima 6337 |
. . . . . . . . . . . 12
++
++ ++ |
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . 11
++
++ ++ |
60 | 49, 55, 59 | sylanbrc 698 |
. . . . . . . . . 10
++ |
61 | 48, 60 | elind 3798 |
. . . . . . . . 9
++ Word
|
62 | 61, 11 | syl6eleqr 2712 |
. . . . . . . 8
++ |
63 | 62 | adantr 481 |
. . . . . . 7
++ |
64 | 1 | adantr 481 |
. . . . . . . 8
Word |
65 | 42 | adantr 481 |
. . . . . . . . 9
|
66 | 44 | adantr 481 |
. . . . . . . . 9
|
67 | 65, 66 | ffvelrnd 6360 |
. . . . . . . 8
|
68 | | ccatws1n0 13409 |
. . . . . . . 8
Word ++ |
69 | 64, 67, 68 | syl2anc 693 |
. . . . . . 7
++ |
70 | | eldifsn 4317 |
. . . . . . 7
++ ++
++
|
71 | 63, 69, 70 | sylanbrc 698 |
. . . . . 6
++ |
72 | 41, 71 | eqeltrd 2701 |
. . . . 5
++ |
73 | | eqidd 2623 |
. . . . . . 7
++ ++ |
74 | | simprl 794 |
. . . . . . . 8
|
75 | 74 | fveq2d 6195 |
. . . . . . . . 9
|
76 | 75 | s1eqd 13381 |
. . . . . . . 8
|
77 | 74, 76 | oveq12d 6668 |
. . . . . . 7
++ ++ |
78 | | vex 3203 |
. . . . . . . 8
|
79 | 78 | a1i 11 |
. . . . . . 7
|
80 | | vex 3203 |
. . . . . . . 8
|
81 | 80 | a1i 11 |
. . . . . . 7
|
82 | | ovex 6678 |
. . . . . . . 8
++
|
83 | 82 | a1i 11 |
. . . . . . 7
++ |
84 | 73, 77, 79, 81, 83 | ovmpt2d 6788 |
. . . . . 6
++ ++ |
85 | | eldifi 3732 |
. . . . . . . . . . . 12
|
86 | 85 | ad2antrl 764 |
. . . . . . . . . . 11
|
87 | 13, 86 | sseldi 3601 |
. . . . . . . . . 10
Word |
88 | 42 | adantr 481 |
. . . . . . . . . . . 12
|
89 | 88, 86 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
90 | 89 | s1cld 13383 |
. . . . . . . . . 10
Word
|
91 | | ccatcl 13359 |
. . . . . . . . . 10
Word Word ++ Word |
92 | 87, 90, 91 | syl2anc 693 |
. . . . . . . . 9
++ Word |
93 | | ccatws1len 13398 |
. . . . . . . . . . . 12
Word ++ |
94 | 87, 89, 93 | syl2anc 693 |
. . . . . . . . . . 11
++ |
95 | 86, 11 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
Word
|
96 | | elin 3796 |
. . . . . . . . . . . . . . . 16
Word
Word |
97 | 96 | simprbi 480 |
. . . . . . . . . . . . . . 15
Word |
98 | 95, 97 | syl 17 |
. . . . . . . . . . . . . 14
|
99 | | elpreima 6337 |
. . . . . . . . . . . . . . 15
|
100 | 56, 57, 99 | mp2b 10 |
. . . . . . . . . . . . . 14
|
101 | 98, 100 | sylib 208 |
. . . . . . . . . . . . 13
|
102 | 101 | simprd 479 |
. . . . . . . . . . . 12
|
103 | | peano2uz 11741 |
. . . . . . . . . . . 12
|
104 | 102, 103 | syl 17 |
. . . . . . . . . . 11
|
105 | 94, 104 | eqeltrd 2701 |
. . . . . . . . . 10
++ |
106 | | elpreima 6337 |
. . . . . . . . . . 11
++
++ ++ |
107 | 56, 57, 106 | mp2b 10 |
. . . . . . . . . 10
++
++ ++ |
108 | 83, 105, 107 | sylanbrc 698 |
. . . . . . . . 9
++ |
109 | 92, 108 | elind 3798 |
. . . . . . . 8
++ Word |
110 | 109, 11 | syl6eleqr 2712 |
. . . . . . 7
++ |
111 | | ccatws1n0 13409 |
. . . . . . . 8
Word ++ |
112 | 87, 89, 111 | syl2anc 693 |
. . . . . . 7
++ |
113 | | eldifsn 4317 |
. . . . . . 7
++ ++
++
|
114 | 110, 112,
113 | sylanbrc 698 |
. . . . . 6
++ |
115 | 84, 114 | eqeltrd 2701 |
. . . . 5
++ |
116 | 26, 29, 72, 115 | seqf 12822 |
. . . 4
++ ++ |
117 | | fco2 6059 |
. . . 4
lastS ++ ++ lastS
++ ++ |
118 | 25, 116, 117 | syl2anc 693 |
. . 3
lastS
++
++ |
119 | | fzouzdisj 12504 |
. . . 4
..^ |
120 | 119 | a1i 11 |
. . 3
..^
|
121 | | fun 6066 |
. . 3
..^ lastS ++ ++ ..^
lastS ++ ++ ..^ |
122 | 3, 118, 120, 121 | syl21anc 1325 |
. 2
lastS ++ ++ ..^ |
123 | 43, 1, 11, 42 | sseqval 30450 |
. . 3
seqstr lastS ++ ++ |
124 | | fzouzsplit 12503 |
. . . . . 6
..^ |
125 | 34, 124 | sylbi 207 |
. . . . 5
..^ |
126 | 1, 27, 125 | 3syl 18 |
. . . 4
..^ |
127 | 38, 126 | syl5eq 2668 |
. . 3
..^ |
128 | | unidm 3756 |
. . . . 5
|
129 | 128 | a1i 11 |
. . . 4
|
130 | 129 | eqcomd 2628 |
. . 3
|
131 | 123, 127,
130 | feq123d 6034 |
. 2
seqstr
lastS
++
++ ..^ |
132 | 122, 131 | mpbird 247 |
1
seqstr |