Step | Hyp | Ref
| Expression |
1 | | swrdcl 13419 |
. . . . . 6
Word substr Word |
2 | 1 | adantr 481 |
. . . . 5
Word
substr Word |
3 | | swrdcl 13419 |
. . . . . 6
Word substr Word |
4 | 3 | adantr 481 |
. . . . 5
Word
substr Word |
5 | | ccatcl 13359 |
. . . . 5
substr Word substr Word
substr ++ substr Word |
6 | 2, 4, 5 | syl2anc 693 |
. . . 4
Word
substr ++ substr Word |
7 | | wrdf 13310 |
. . . 4
substr ++ substr Word substr ++ substr ..^ substr
++ substr |
8 | | ffn 6045 |
. . . 4
substr ++ substr ..^ substr
++ substr substr ++ substr ..^ substr ++ substr |
9 | 6, 7, 8 | 3syl 18 |
. . 3
Word
substr ++ substr ..^ substr ++ substr |
10 | | ccatlen 13360 |
. . . . . . 7
substr Word substr Word
substr
++ substr substr substr
|
11 | 2, 4, 10 | syl2anc 693 |
. . . . . 6
Word
substr
++ substr substr substr
|
12 | | simpl 473 |
. . . . . . . . 9
Word
Word |
13 | | simpr1 1067 |
. . . . . . . . 9
Word
|
14 | | simpr2 1068 |
. . . . . . . . . 10
Word
|
15 | | simpr3 1069 |
. . . . . . . . . 10
Word
|
16 | | fzass4 12379 |
. . . . . . . . . . . 12
|
17 | 16 | biimpri 218 |
. . . . . . . . . . 11
|
18 | 17 | simpld 475 |
. . . . . . . . . 10
|
19 | 14, 15, 18 | syl2anc 693 |
. . . . . . . . 9
Word
|
20 | | swrdlen 13423 |
. . . . . . . . 9
Word
substr |
21 | 12, 13, 19, 20 | syl3anc 1326 |
. . . . . . . 8
Word
substr |
22 | | swrdlen 13423 |
. . . . . . . . 9
Word
substr |
23 | 12, 14, 15, 22 | syl3anc 1326 |
. . . . . . . 8
Word
substr |
24 | 21, 23 | oveq12d 6668 |
. . . . . . 7
Word
substr substr |
25 | | elfzelz 12342 |
. . . . . . . . . 10
|
26 | 14, 25 | syl 17 |
. . . . . . . . 9
Word
|
27 | 26 | zcnd 11483 |
. . . . . . . 8
Word
|
28 | | elfzelz 12342 |
. . . . . . . . . 10
|
29 | 13, 28 | syl 17 |
. . . . . . . . 9
Word
|
30 | 29 | zcnd 11483 |
. . . . . . . 8
Word
|
31 | | elfzelz 12342 |
. . . . . . . . . 10
|
32 | 15, 31 | syl 17 |
. . . . . . . . 9
Word
|
33 | 32 | zcnd 11483 |
. . . . . . . 8
Word
|
34 | 27, 30, 33 | npncan3d 10428 |
. . . . . . 7
Word
|
35 | 24, 34 | eqtrd 2656 |
. . . . . 6
Word
substr substr |
36 | 11, 35 | eqtrd 2656 |
. . . . 5
Word
substr
++ substr |
37 | 36 | oveq2d 6666 |
. . . 4
Word
..^ substr ++ substr ..^ |
38 | 37 | fneq2d 5982 |
. . 3
Word
substr ++ substr ..^ substr ++ substr
substr ++ substr ..^ |
39 | 9, 38 | mpbid 222 |
. 2
Word
substr ++ substr ..^ |
40 | | swrdcl 13419 |
. . . . 5
Word substr Word |
41 | 40 | adantr 481 |
. . . 4
Word
substr Word |
42 | | wrdf 13310 |
. . . 4
substr Word substr
..^ substr |
43 | | ffn 6045 |
. . . 4
substr ..^ substr substr ..^ substr |
44 | 41, 42, 43 | 3syl 18 |
. . 3
Word
substr ..^ substr |
45 | | fzass4 12379 |
. . . . . . . . 9
|
46 | 45 | biimpri 218 |
. . . . . . . 8
|
47 | 46 | simpld 475 |
. . . . . . 7
|
48 | 13, 14, 47 | syl2anc 693 |
. . . . . 6
Word
|
49 | | swrdlen 13423 |
. . . . . 6
Word
substr |
50 | 12, 48, 15, 49 | syl3anc 1326 |
. . . . 5
Word
substr |
51 | 50 | oveq2d 6666 |
. . . 4
Word
..^ substr
..^ |
52 | 51 | fneq2d 5982 |
. . 3
Word
substr ..^ substr
substr
..^ |
53 | 44, 52 | mpbid 222 |
. 2
Word
substr ..^ |
54 | | simpr 477 |
. . . . 5
Word ..^
..^ |
55 | 26, 29 | zsubcld 11487 |
. . . . . 6
Word
|
56 | 55 | adantr 481 |
. . . . 5
Word ..^
|
57 | | fzospliti 12500 |
. . . . 5
..^
..^ ..^ |
58 | 54, 56, 57 | syl2anc 693 |
. . . 4
Word ..^
..^ ..^ |
59 | 2 | adantr 481 |
. . . . . . 7
Word ..^
substr
Word |
60 | 4 | adantr 481 |
. . . . . . 7
Word ..^
substr
Word |
61 | 21 | oveq2d 6666 |
. . . . . . . . 9
Word
..^ substr
..^ |
62 | 61 | eleq2d 2687 |
. . . . . . . 8
Word
..^ substr ..^ |
63 | 62 | biimpar 502 |
. . . . . . 7
Word ..^
..^ substr |
64 | | ccatval1 13361 |
. . . . . . 7
substr Word substr Word
..^ substr substr ++ substr substr |
65 | 59, 60, 63, 64 | syl3anc 1326 |
. . . . . 6
Word ..^
substr
++ substr substr |
66 | | simpll 790 |
. . . . . . 7
Word ..^
Word |
67 | | simplr1 1103 |
. . . . . . 7
Word ..^
|
68 | 19 | adantr 481 |
. . . . . . 7
Word ..^
|
69 | | simpr 477 |
. . . . . . 7
Word ..^
..^ |
70 | | swrdfv 13424 |
. . . . . . 7
Word
..^ substr |
71 | 66, 67, 68, 69, 70 | syl31anc 1329 |
. . . . . 6
Word ..^
substr
|
72 | 65, 71 | eqtrd 2656 |
. . . . 5
Word ..^
substr
++ substr
|
73 | 2 | adantr 481 |
. . . . . . 7
Word ..^ substr Word |
74 | 4 | adantr 481 |
. . . . . . 7
Word ..^ substr Word |
75 | 21, 35 | oveq12d 6668 |
. . . . . . . . 9
Word
substr ..^ substr substr
..^ |
76 | 75 | eleq2d 2687 |
. . . . . . . 8
Word
substr ..^ substr
substr
..^ |
77 | 76 | biimpar 502 |
. . . . . . 7
Word ..^ substr ..^ substr
substr |
78 | | ccatval2 13362 |
. . . . . . 7
substr Word substr Word
substr ..^ substr substr
substr
++ substr substr substr |
79 | 73, 74, 77, 78 | syl3anc 1326 |
. . . . . 6
Word ..^ substr ++ substr substr substr |
80 | | simpll 790 |
. . . . . . 7
Word ..^ Word |
81 | | simplr2 1104 |
. . . . . . 7
Word ..^ |
82 | | simplr3 1105 |
. . . . . . 7
Word ..^ |
83 | 21 | oveq2d 6666 |
. . . . . . . . 9
Word
substr |
84 | 83 | adantr 481 |
. . . . . . . 8
Word ..^ substr |
85 | 34 | oveq2d 6666 |
. . . . . . . . . . 11
Word
..^ ..^ |
86 | 85 | eleq2d 2687 |
. . . . . . . . . 10
Word
..^
..^ |
87 | 86 | biimpar 502 |
. . . . . . . . 9
Word ..^ ..^ |
88 | 32, 26 | zsubcld 11487 |
. . . . . . . . . 10
Word
|
89 | 88 | adantr 481 |
. . . . . . . . 9
Word ..^ |
90 | | fzosubel3 12528 |
. . . . . . . . 9
..^
..^ |
91 | 87, 89, 90 | syl2anc 693 |
. . . . . . . 8
Word ..^
..^ |
92 | 84, 91 | eqeltrd 2701 |
. . . . . . 7
Word ..^ substr ..^ |
93 | | swrdfv 13424 |
. . . . . . 7
Word
substr ..^ substr
substr substr |
94 | 80, 81, 82, 92, 93 | syl31anc 1329 |
. . . . . 6
Word ..^ substr substr substr |
95 | 83 | oveq1d 6665 |
. . . . . . . . 9
Word
substr
|
96 | 95 | adantr 481 |
. . . . . . . 8
Word ..^ substr
|
97 | | elfzoelz 12470 |
. . . . . . . . . . 11
..^
|
98 | 97 | zcnd 11483 |
. . . . . . . . . 10
..^
|
99 | 98 | adantl 482 |
. . . . . . . . 9
Word ..^ |
100 | 27, 30 | subcld 10392 |
. . . . . . . . . 10
Word
|
101 | 100 | adantr 481 |
. . . . . . . . 9
Word ..^ |
102 | 27 | adantr 481 |
. . . . . . . . 9
Word ..^ |
103 | 99, 101, 102 | subadd23d 10414 |
. . . . . . . 8
Word ..^ |
104 | 27, 30 | nncand 10397 |
. . . . . . . . . 10
Word
|
105 | 104 | oveq2d 6666 |
. . . . . . . . 9
Word
|
106 | 105 | adantr 481 |
. . . . . . . 8
Word ..^
|
107 | 96, 103, 106 | 3eqtrd 2660 |
. . . . . . 7
Word ..^ substr |
108 | 107 | fveq2d 6195 |
. . . . . 6
Word ..^ substr |
109 | 79, 94, 108 | 3eqtrd 2660 |
. . . . 5
Word ..^ substr ++ substr |
110 | 72, 109 | jaodan 826 |
. . . 4
Word ..^ ..^
substr
++ substr
|
111 | 58, 110 | syldan 487 |
. . 3
Word ..^
substr
++ substr
|
112 | | simpll 790 |
. . . 4
Word ..^
Word |
113 | 48 | adantr 481 |
. . . 4
Word ..^
|
114 | | simplr3 1105 |
. . . 4
Word ..^
|
115 | | swrdfv 13424 |
. . . 4
Word
..^ substr |
116 | 112, 113,
114, 54, 115 | syl31anc 1329 |
. . 3
Word ..^
substr
|
117 | 111, 116 | eqtr4d 2659 |
. 2
Word ..^
substr
++ substr substr |
118 | 39, 53, 117 | eqfnfvd 6314 |
1
Word
substr ++ substr substr |