Proof of Theorem splval2
Step | Hyp | Ref
| Expression |
1 | | splval2.s |
. . . 4
++ ++ |
2 | | splval2.a |
. . . . . 6
Word |
3 | | splval2.b |
. . . . . 6
Word |
4 | | ccatcl 13359 |
. . . . . 6
Word
Word ++ Word |
5 | 2, 3, 4 | syl2anc 693 |
. . . . 5
++ Word |
6 | | splval2.c |
. . . . 5
Word |
7 | | ccatcl 13359 |
. . . . 5
++ Word Word ++ ++ Word |
8 | 5, 6, 7 | syl2anc 693 |
. . . 4
++ ++ Word |
9 | 1, 8 | eqeltrd 2701 |
. . 3
Word |
10 | | splval2.f |
. . . 4
|
11 | | lencl 13324 |
. . . . 5
Word |
12 | 2, 11 | syl 17 |
. . . 4
|
13 | 10, 12 | eqeltrd 2701 |
. . 3
|
14 | | splval2.t |
. . . 4
|
15 | | lencl 13324 |
. . . . . 6
Word |
16 | 3, 15 | syl 17 |
. . . . 5
|
17 | 13, 16 | nn0addcld 11355 |
. . . 4
|
18 | 14, 17 | eqeltrd 2701 |
. . 3
|
19 | | splval2.r |
. . 3
Word |
20 | | splval 13502 |
. . 3
Word
Word
splice
substr ++ ++ substr |
21 | 9, 13, 18, 19, 20 | syl13anc 1328 |
. 2
splice
substr ++ ++ substr |
22 | | nn0uz 11722 |
. . . . . . . . . 10
|
23 | 13, 22 | syl6eleq 2711 |
. . . . . . . . 9
|
24 | | eluzfz1 12348 |
. . . . . . . . 9
|
25 | 23, 24 | syl 17 |
. . . . . . . 8
|
26 | 13 | nn0zd 11480 |
. . . . . . . . . . . 12
|
27 | | uzid 11702 |
. . . . . . . . . . . 12
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
|
29 | | uzaddcl 11744 |
. . . . . . . . . . 11
|
30 | 28, 16, 29 | syl2anc 693 |
. . . . . . . . . 10
|
31 | 14, 30 | eqeltrd 2701 |
. . . . . . . . 9
|
32 | | elfzuzb 12336 |
. . . . . . . . 9
|
33 | 23, 31, 32 | sylanbrc 698 |
. . . . . . . 8
|
34 | 18, 22 | syl6eleq 2711 |
. . . . . . . . 9
|
35 | | ccatlen 13360 |
. . . . . . . . . . . 12
++ Word Word ++ ++ ++ |
36 | 5, 6, 35 | syl2anc 693 |
. . . . . . . . . . 11
++ ++ ++ |
37 | 1 | fveq2d 6195 |
. . . . . . . . . . 11
++ ++ |
38 | 10 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
39 | | ccatlen 13360 |
. . . . . . . . . . . . . 14
Word
Word ++ |
40 | 2, 3, 39 | syl2anc 693 |
. . . . . . . . . . . . 13
++ |
41 | 38, 14, 40 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
++ |
42 | 41 | oveq1d 6665 |
. . . . . . . . . . 11
++ |
43 | 36, 37, 42 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
44 | 18 | nn0zd 11480 |
. . . . . . . . . . . 12
|
45 | | uzid 11702 |
. . . . . . . . . . . 12
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
|
47 | | lencl 13324 |
. . . . . . . . . . . 12
Word |
48 | 6, 47 | syl 17 |
. . . . . . . . . . 11
|
49 | | uzaddcl 11744 |
. . . . . . . . . . 11
|
50 | 46, 48, 49 | syl2anc 693 |
. . . . . . . . . 10
|
51 | 43, 50 | eqeltrd 2701 |
. . . . . . . . 9
|
52 | | elfzuzb 12336 |
. . . . . . . . 9
|
53 | 34, 51, 52 | sylanbrc 698 |
. . . . . . . 8
|
54 | | ccatswrd 13456 |
. . . . . . . 8
Word
substr ++ substr substr |
55 | 9, 25, 33, 53, 54 | syl13anc 1328 |
. . . . . . 7
substr ++ substr substr |
56 | | eluzfz1 12348 |
. . . . . . . . . . . 12
|
57 | 34, 56 | syl 17 |
. . . . . . . . . . 11
|
58 | | lencl 13324 |
. . . . . . . . . . . . . 14
Word |
59 | 9, 58 | syl 17 |
. . . . . . . . . . . . 13
|
60 | 59, 22 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
61 | | eluzfz2 12349 |
. . . . . . . . . . . 12
|
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
|
63 | | ccatswrd 13456 |
. . . . . . . . . . 11
Word substr ++ substr substr |
64 | 9, 57, 53, 62, 63 | syl13anc 1328 |
. . . . . . . . . 10
substr ++ substr substr |
65 | | swrdid 13428 |
. . . . . . . . . . 11
Word substr |
66 | 9, 65 | syl 17 |
. . . . . . . . . 10
substr |
67 | 64, 66, 1 | 3eqtrd 2660 |
. . . . . . . . 9
substr ++ substr ++ ++ |
68 | | swrdcl 13419 |
. . . . . . . . . . 11
Word substr Word |
69 | 9, 68 | syl 17 |
. . . . . . . . . 10
substr Word |
70 | | swrdcl 13419 |
. . . . . . . . . . 11
Word substr Word |
71 | 9, 70 | syl 17 |
. . . . . . . . . 10
substr
Word |
72 | | swrd0len 13422 |
. . . . . . . . . . . 12
Word
substr |
73 | 9, 53, 72 | syl2anc 693 |
. . . . . . . . . . 11
substr |
74 | 73, 41 | eqtrd 2656 |
. . . . . . . . . 10
substr ++ |
75 | | ccatopth 13470 |
. . . . . . . . . 10
substr Word substr
Word ++ Word
Word substr ++ substr ++ substr ++ ++
substr ++ substr |
76 | 69, 71, 5, 6, 74, 75 | syl221anc 1337 |
. . . . . . . . 9
substr ++ substr ++ ++
substr ++ substr |
77 | 67, 76 | mpbid 222 |
. . . . . . . 8
substr ++
substr
|
78 | 77 | simpld 475 |
. . . . . . 7
substr ++ |
79 | 55, 78 | eqtrd 2656 |
. . . . . 6
substr ++ substr ++ |
80 | | swrdcl 13419 |
. . . . . . . 8
Word substr Word |
81 | 9, 80 | syl 17 |
. . . . . . 7
substr Word |
82 | | swrdcl 13419 |
. . . . . . . 8
Word substr Word |
83 | 9, 82 | syl 17 |
. . . . . . 7
substr Word |
84 | | uztrn 11704 |
. . . . . . . . . . 11
|
85 | 51, 31, 84 | syl2anc 693 |
. . . . . . . . . 10
|
86 | | elfzuzb 12336 |
. . . . . . . . . 10
|
87 | 23, 85, 86 | sylanbrc 698 |
. . . . . . . . 9
|
88 | | swrd0len 13422 |
. . . . . . . . 9
Word
substr |
89 | 9, 87, 88 | syl2anc 693 |
. . . . . . . 8
substr |
90 | 89, 10 | eqtrd 2656 |
. . . . . . 7
substr |
91 | | ccatopth 13470 |
. . . . . . 7
substr Word substr Word
Word Word substr substr ++ substr ++
substr
substr |
92 | 81, 83, 2, 3, 90, 91 | syl221anc 1337 |
. . . . . 6
substr ++ substr ++ substr substr |
93 | 79, 92 | mpbid 222 |
. . . . 5
substr substr |
94 | 93 | simpld 475 |
. . . 4
substr |
95 | 94 | oveq1d 6665 |
. . 3
substr ++ ++ |
96 | 77 | simprd 479 |
. . 3
substr
|
97 | 95, 96 | oveq12d 6668 |
. 2
substr ++ ++ substr ++ ++ |
98 | 21, 97 | eqtrd 2656 |
1
splice
++ ++ |