Step | Hyp | Ref
| Expression |
1 | | ccatcl 12393 |
. . . 4
  Word
Word   concat  Word   |
2 | | revcl 12520 |
. . . 4
  concat  Word reverse  concat   Word   |
3 | | wrdf 12359 |
. . . 4
 reverse  concat   Word reverse  concat      ..^   reverse  concat         |
4 | | ffn 5668 |
. . . 4
 reverse  concat      ..^   reverse  concat       reverse  concat    ..^   reverse  concat       |
5 | 1, 2, 3, 4 | 4syl 21 |
. . 3
  Word
Word  reverse  concat    ..^   reverse  concat       |
6 | | revlen 12521 |
. . . . . . 7
  concat  Word    reverse  concat        concat     |
7 | 1, 6 | syl 16 |
. . . . . 6
  Word
Word     reverse  concat        concat     |
8 | | ccatlen 12394 |
. . . . . . 7
  Word
Word      concat               |
9 | | lencl 12368 |
. . . . . . . . 9
 Word       |
10 | 9 | nn0cnd 10750 |
. . . . . . . 8
 Word       |
11 | | lencl 12368 |
. . . . . . . . 9
 Word       |
12 | 11 | nn0cnd 10750 |
. . . . . . . 8
 Word       |
13 | | addcom 9667 |
. . . . . . . 8
                                 |
14 | 10, 12, 13 | syl2an 477 |
. . . . . . 7
  Word
Word                        |
15 | 8, 14 | eqtrd 2495 |
. . . . . 6
  Word
Word      concat               |
16 | 7, 15 | eqtrd 2495 |
. . . . 5
  Word
Word     reverse  concat                |
17 | 16 | oveq2d 6217 |
. . . 4
  Word
Word   ..^   reverse  concat      ..^             |
18 | 17 | fneq2d 5611 |
. . 3
  Word
Word   reverse  concat    ..^   reverse  concat     reverse  concat    ..^              |
19 | 5, 18 | mpbid 210 |
. 2
  Word
Word  reverse  concat    ..^             |
20 | | revcl 12520 |
. . . . 5
 Word reverse  Word   |
21 | | revcl 12520 |
. . . . 5
 Word reverse  Word   |
22 | | ccatcl 12393 |
. . . . 5
  reverse  Word reverse  Word
  reverse  concat reverse   Word
  |
23 | 20, 21, 22 | syl2anr 478 |
. . . 4
  Word
Word   reverse  concat reverse   Word
  |
24 | | wrdf 12359 |
. . . 4
  reverse  concat reverse   Word  reverse  concat reverse      ..^    reverse  concat reverse         |
25 | | ffn 5668 |
. . . 4
  reverse  concat reverse      ..^    reverse  concat reverse        reverse  concat reverse    ..^    reverse  concat reverse       |
26 | 23, 24, 25 | 3syl 20 |
. . 3
  Word
Word   reverse  concat reverse    ..^    reverse  concat reverse       |
27 | | ccatlen 12394 |
. . . . . . 7
  reverse  Word reverse  Word
     reverse  concat reverse        reverse      reverse      |
28 | 20, 21, 27 | syl2anr 478 |
. . . . . 6
  Word
Word      reverse  concat reverse        reverse      reverse      |
29 | | revlen 12521 |
. . . . . . 7
 Word    reverse         |
30 | | revlen 12521 |
. . . . . . 7
 Word    reverse         |
31 | 29, 30 | oveqan12rd 6221 |
. . . . . 6
  Word
Word      reverse      reverse                |
32 | 28, 31 | eqtrd 2495 |
. . . . 5
  Word
Word      reverse  concat reverse                |
33 | 32 | oveq2d 6217 |
. . . 4
  Word
Word   ..^    reverse  concat reverse      ..^             |
34 | 33 | fneq2d 5611 |
. . 3
  Word
Word    reverse  concat reverse    ..^    reverse  concat reverse      reverse  concat reverse    ..^              |
35 | 26, 34 | mpbid 210 |
. 2
  Word
Word   reverse  concat reverse    ..^             |
36 | | id 22 |
. . . 4
  ..^            ..^             |
37 | 11 | nn0zd 10857 |
. . . . 5
 Word       |
38 | 37 | adantl 466 |
. . . 4
  Word
Word        |
39 | | fzospliti 11699 |
. . . 4
   ..^                  ..^          ..^              |
40 | 36, 38, 39 | syl2anr 478 |
. . 3
   Word
Word   ..^              ..^          ..^              |
41 | | simpll 753 |
. . . . . . 7
   Word
Word   ..^     
Word   |
42 | | simplr 754 |
. . . . . . 7
   Word
Word   ..^     
Word   |
43 | | fzoval 11672 |
. . . . . . . . . . . 12
    
 ..^                 |
44 | 38, 43 | syl 16 |
. . . . . . . . . . 11
  Word
Word   ..^                 |
45 | 44 | eleq2d 2524 |
. . . . . . . . . 10
  Word
Word    ..^    
             |
46 | 45 | biimpa 484 |
. . . . . . . . 9
   Word
Word   ..^     
            |
47 | | fznn0sub2 11606 |
. . . . . . . . 9
          
                    |
48 | 46, 47 | syl 16 |
. . . . . . . 8
   Word
Word   ..^                          |
49 | 44 | adantr 465 |
. . . . . . . 8
   Word
Word   ..^       ..^                 |
50 | 48, 49 | eleqtrrd 2545 |
. . . . . . 7
   Word
Word   ..^               ..^       |
51 | | ccatval3 12397 |
. . . . . . 7
  Word
Word          ..^        concat                                 |
52 | 41, 42, 50, 51 | syl3anc 1219 |
. . . . . 6
   Word
Word   ..^        concat                                 |
53 | 15 | oveq1d 6216 |
. . . . . . . . . . 11
  Word
Word       concat                  |
54 | 12 | adantl 466 |
. . . . . . . . . . . 12
  Word
Word        |
55 | 10 | adantr 465 |
. . . . . . . . . . . 12
  Word
Word        |
56 | | ax-1cn 9452 |
. . . . . . . . . . . . 13
 |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
  Word
Word    |
58 | 54, 55, 57 | addsubd 9852 |
. . . . . . . . . . 11
  Word
Word                            |
59 | 53, 58 | eqtrd 2495 |
. . . . . . . . . 10
  Word
Word       concat                  |
60 | 59 | oveq1d 6216 |
. . . . . . . . 9
  Word
Word        concat                     |
61 | 60 | adantr 465 |
. . . . . . . 8
   Word
Word   ..^            concat                     |
62 | | peano2zm 10800 |
. . . . . . . . . . . 12
    
        |
63 | 37, 62 | syl 16 |
. . . . . . . . . . 11
 Word         |
64 | 63 | zcnd 10860 |
. . . . . . . . . 10
 Word         |
65 | 64 | ad2antlr 726 |
. . . . . . . . 9
   Word
Word   ..^              |
66 | 10 | ad2antrr 725 |
. . . . . . . . 9
   Word
Word   ..^            |
67 | | elfzoelz 11671 |
. . . . . . . . . . 11
  ..^    
  |
68 | 67 | zcnd 10860 |
. . . . . . . . . 10
  ..^    
  |
69 | 68 | adantl 466 |
. . . . . . . . 9
   Word
Word   ..^     
  |
70 | 65, 66, 69 | addsubd 9852 |
. . . . . . . 8
   Word
Word   ..^                                    |
71 | 61, 70 | eqtrd 2495 |
. . . . . . 7
   Word
Word   ..^            concat                     |
72 | 71 | fveq2d 5804 |
. . . . . 6
   Word
Word   ..^        concat          concat        concat                     |
73 | | revfv 12522 |
. . . . . . 7
  Word
 ..^       reverse                   |
74 | 73 | adantll 713 |
. . . . . 6
   Word
Word   ..^       reverse                   |
75 | 52, 72, 74 | 3eqtr4d 2505 |
. . . . 5
   Word
Word   ..^        concat          concat       reverse       |
76 | 1 | adantr 465 |
. . . . . 6
   Word
Word   ..^       concat
 Word   |
77 | | uzid 10987 |
. . . . . . . . . . 11
    
              |
78 | 38, 77 | syl 16 |
. . . . . . . . . 10
  Word
Word                |
79 | 9 | adantr 465 |
. . . . . . . . . 10
  Word
Word        |
80 | | uzaddcl 11023 |
. . . . . . . . . 10
                                       |
81 | 78, 79, 80 | syl2anc 661 |
. . . . . . . . 9
  Word
Word                      |
82 | 15, 81 | eqeltrd 2542 |
. . . . . . . 8
  Word
Word      concat             |
83 | | fzoss2 11695 |
. . . . . . . 8
     concat            ..^      ..^    concat      |
84 | 82, 83 | syl 16 |
. . . . . . 7
  Word
Word   ..^      ..^    concat      |
85 | 84 | sselda 3465 |
. . . . . 6
   Word
Word   ..^     
 ..^    concat      |
86 | | revfv 12522 |
. . . . . 6
   concat  Word  ..^    concat      reverse  concat        concat          concat        |
87 | 76, 85, 86 | syl2anc 661 |
. . . . 5
   Word
Word   ..^       reverse  concat        concat          concat        |
88 | 20 | ad2antlr 726 |
. . . . . 6
   Word
Word   ..^      reverse  Word   |
89 | 21 | ad2antrr 725 |
. . . . . 6
   Word
Word   ..^      reverse  Word   |
90 | 29 | adantl 466 |
. . . . . . . . 9
  Word
Word     reverse         |
91 | 90 | oveq2d 6217 |
. . . . . . . 8
  Word
Word   ..^   reverse     ..^       |
92 | 91 | eleq2d 2524 |
. . . . . . 7
  Word
Word    ..^   reverse     ..^        |
93 | 92 | biimpar 485 |
. . . . . 6
   Word
Word   ..^     
 ..^   reverse      |
94 | | ccatval1 12395 |
. . . . . 6
  reverse  Word reverse  Word
 ..^   reverse    
  reverse  concat reverse       reverse       |
95 | 88, 89, 93, 94 | syl3anc 1219 |
. . . . 5
   Word
Word   ..^        reverse  concat reverse       reverse       |
96 | 75, 87, 95 | 3eqtr4d 2505 |
. . . 4
   Word
Word   ..^       reverse  concat        reverse  concat reverse        |
97 | 8 | oveq1d 6216 |
. . . . . . . . . . . 12
  Word
Word       concat                  |
98 | 55, 54, 57 | addsubd 9852 |
. . . . . . . . . . . 12
  Word
Word                            |
99 | 97, 98 | eqtrd 2495 |
. . . . . . . . . . 11
  Word
Word       concat                  |
100 | 99 | oveq1d 6216 |
. . . . . . . . . 10
  Word
Word        concat                     |
101 | 100 | adantr 465 |
. . . . . . . . 9
   Word
Word       ..^                  concat                     |
102 | 9 | nn0zd 10857 |
. . . . . . . . . . . . 13
 Word       |
103 | | peano2zm 10800 |
. . . . . . . . . . . . 13
    
        |
104 | 102, 103 | syl 16 |
. . . . . . . . . . . 12
 Word         |
105 | 104 | zcnd 10860 |
. . . . . . . . . . 11
 Word         |
106 | 105 | ad2antrr 725 |
. . . . . . . . . 10
   Word
Word       ..^                    |
107 | | elfzoelz 11671 |
. . . . . . . . . . . 12
      ..^          
  |
108 | 107 | zcnd 10860 |
. . . . . . . . . . 11
      ..^          
  |
109 | 108 | adantl 466 |
. . . . . . . . . 10
   Word
Word       ..^           
  |
110 | 12 | ad2antlr 726 |
. . . . . . . . . 10
   Word
Word       ..^                  |
111 | 106, 109,
110 | subsub3d 9861 |
. . . . . . . . 9
   Word
Word       ..^                                          |
112 | 101, 111 | eqtr4d 2498 |
. . . . . . . 8
   Word
Word       ..^                  concat                     |
113 | 90 | oveq2d 6217 |
. . . . . . . . . 10
  Word
Word      reverse            |
114 | 113 | oveq2d 6217 |
. . . . . . . . 9
  Word
Word             reverse                     |
115 | 114 | adantr 465 |
. . . . . . . 8
   Word
Word       ..^                       reverse                     |
116 | 112, 115 | eqtr4d 2498 |
. . . . . . 7
   Word
Word       ..^                  concat                reverse       |
117 | 116 | fveq2d 5804 |
. . . . . 6
   Word
Word       ..^                     concat                    reverse        |
118 | | simpll 753 |
. . . . . . 7
   Word
Word       ..^           
Word   |
119 | | simplr 754 |
. . . . . . 7
   Word
Word       ..^           
Word   |
120 | | zaddcl 10797 |
. . . . . . . . . . . 12
                       |
121 | 37, 102, 120 | syl2anr 478 |
. . . . . . . . . . 11
  Word
Word              |
122 | | peano2zm 10800 |
. . . . . . . . . . 11
          
              |
123 | 121, 122 | syl 16 |
. . . . . . . . . 10
  Word
Word                |
124 | 123 | adantr 465 |
. . . . . . . . 9
   Word
Word       ..^                          |
125 | | fzoval 11672 |
. . . . . . . . . . . 12
          
     ..^                                 |
126 | 121, 125 | syl 16 |
. . . . . . . . . . 11
  Word
Word       ..^                                 |
127 | 126 | eleq2d 2524 |
. . . . . . . . . 10
  Word
Word        ..^          
                       |
128 | 127 | biimpa 484 |
. . . . . . . . 9
   Word
Word       ..^           
                      |
129 | | fzrev2i 11639 |
. . . . . . . . 9
                                                                                                   |
130 | 124, 128,
129 | syl2anc 661 |
. . . . . . . 8
   Word
Word       ..^                                                                            |
131 | 53 | oveq1d 6216 |
. . . . . . . . 9
  Word
Word        concat                     |
132 | 131 | adantr 465 |
. . . . . . . 8
   Word
Word       ..^                  concat                     |
133 | 102 | adantr 465 |
. . . . . . . . . . 11
  Word
Word        |
134 | | fzoval 11672 |
. . . . . . . . . . 11
    
 ..^                 |
135 | 133, 134 | syl 16 |
. . . . . . . . . 10
  Word
Word   ..^                 |
136 | 123 | zcnd 10860 |
. . . . . . . . . . . 12
  Word
Word                |
137 | 136 | subidd 9819 |
. . . . . . . . . . 11
  Word
Word                              |
138 | | addcl 9476 |
. . . . . . . . . . . . . 14
                       |
139 | 12, 10, 138 | syl2anr 478 |
. . . . . . . . . . . . 13
  Word
Word              |
140 | 139, 57, 54 | sub32d 9863 |
. . . . . . . . . . . 12
  Word
Word                                        |
141 | | pncan2 9729 |
. . . . . . . . . . . . . 14
                                 |
142 | 12, 10, 141 | syl2anr 478 |
. . . . . . . . . . . . 13
  Word
Word                        |
143 | 142 | oveq1d 6216 |
. . . . . . . . . . . 12
  Word
Word                            |
144 | 140, 143 | eqtrd 2495 |
. . . . . . . . . . 11
  Word
Word                            |
145 | 137, 144 | oveq12d 6219 |
. . . . . . . . . 10
  Word
Word                                                              |
146 | 135, 145 | eqtr4d 2498 |
. . . . . . . . 9
  Word
Word   ..^                                                       |
147 | 146 | adantr 465 |
. . . . . . . 8
   Word
Word       ..^             ..^                                                       |
148 | 130, 132,
147 | 3eltr4d 2557 |
. . . . . . 7
   Word
Word       ..^                  concat      ..^       |
149 | | ccatval1 12395 |
. . . . . . 7
  Word
Word       concat      ..^        concat          concat               concat        |
150 | 118, 119,
148, 149 | syl3anc 1219 |
. . . . . 6
   Word
Word       ..^              concat          concat               concat        |
151 | 29 | ad2antlr 726 |
. . . . . . . . 9
   Word
Word       ..^               reverse         |
152 | 151 | oveq2d 6217 |
. . . . . . . 8
   Word
Word       ..^                reverse            |
153 | | id 22 |
. . . . . . . . 9
      ..^          
     ..^             |
154 | | fzosubel3 11719 |
. . . . . . . . 9
       ..^                       ..^       |
155 | 153, 133,
154 | syl2anr 478 |
. . . . . . . 8
   Word
Word       ..^                   ..^       |
156 | 152, 155 | eqeltrd 2542 |
. . . . . . 7
   Word
Word       ..^                reverse     ..^       |
157 | | revfv 12522 |
. . . . . . 7
  Word 
   reverse     ..^       reverse        reverse               
   reverse        |
158 | 118, 156,
157 | syl2anc 661 |
. . . . . 6
   Word
Word       ..^             reverse        reverse               
   reverse        |
159 | 117, 150,
158 | 3eqtr4d 2505 |
. . . . 5
   Word
Word       ..^              concat          concat       reverse        reverse       |
160 | 1 | adantr 465 |
. . . . . 6
   Word
Word       ..^             concat
 Word   |
161 | 11 | adantl 466 |
. . . . . . . . 9
  Word
Word        |
162 | | fzoss1 11694 |
. . . . . . . . . 10
              ..^            ..^             |
163 | | nn0uz 11007 |
. . . . . . . . . 10
     |
164 | 162, 163 | eleq2s 2562 |
. . . . . . . . 9
    
     ..^            ..^             |
165 | 161, 164 | syl 16 |
. . . . . . . 8
  Word
Word       ..^            ..^             |
166 | 15 | oveq2d 6217 |
. . . . . . . 8
  Word
Word   ..^    concat     ..^             |
167 | 165, 166 | sseqtr4d 3502 |
. . . . . . 7
  Word
Word       ..^            ..^    concat      |
168 | 167 | sselda 3465 |
. . . . . 6
   Word
Word       ..^           
 ..^    concat      |
169 | 160, 168,
86 | syl2anc 661 |
. . . . 5
   Word
Word       ..^             reverse  concat        concat          concat        |
170 | 20 | ad2antlr 726 |
. . . . . 6
   Word
Word       ..^            reverse  Word   |
171 | 21 | ad2antrr 725 |
. . . . . 6
   Word
Word       ..^            reverse  Word   |
172 | 90, 31 | oveq12d 6219 |
. . . . . . . 8
  Word
Word      reverse   ..^    reverse      reverse          ..^             |
173 | 172 | eleq2d 2524 |
. . . . . . 7
  Word
Word       reverse   ..^    reverse      reverse    
     ..^              |
174 | 173 | biimpar 485 |
. . . . . 6
   Word
Word       ..^           
    reverse   ..^    reverse      reverse       |
175 | | ccatval2 12396 |
. . . . . 6
  reverse  Word reverse  Word
    reverse   ..^    reverse      reverse     
  reverse  concat reverse       reverse        reverse       |
176 | 170, 171,
174, 175 | syl3anc 1219 |
. . . . 5
   Word
Word       ..^              reverse  concat reverse       reverse        reverse       |
177 | 159, 169,
176 | 3eqtr4d 2505 |
. . . 4
   Word
Word       ..^             reverse  concat        reverse  concat reverse        |
178 | 96, 177 | jaodan 783 |
. . 3
   Word
Word    ..^          ..^              reverse  concat        reverse  concat reverse        |
179 | 40, 178 | syldan 470 |
. 2
   Word
Word   ..^             reverse  concat        reverse  concat reverse        |
180 | 19, 35, 179 | eqfnfvd 5910 |
1
  Word
Word  reverse  concat    reverse  concat reverse     |