Metamath Proof Explorer

Theorem wrdt2ind

Description: Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023)

Ref Expression
Hypotheses wrdt2ind.1 
|- ( x = (/) -> ( ph <-> ps ) )
wrdt2ind.2 
|- ( x = y -> ( ph <-> ch ) )
wrdt2ind.3 
|- ( x = ( y ++ <" i j "> ) -> ( ph <-> th ) )
wrdt2ind.4 
|- ( x = A -> ( ph <-> ta ) )
wrdt2ind.5 
|- ps
wrdt2ind.6 
|- ( ( y e. Word B /\ i e. B /\ j e. B ) -> ( ch -> th ) )
Assertion wrdt2ind 
|- ( ( A e. Word B /\ 2 || ( # ` A ) ) -> ta )

Proof

Step Hyp Ref Expression
1 wrdt2ind.1 
 |-  ( x = (/) -> ( ph <-> ps ) )
2 wrdt2ind.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 wrdt2ind.3 
 |-  ( x = ( y ++ <" i j "> ) -> ( ph <-> th ) )
4 wrdt2ind.4 
 |-  ( x = A -> ( ph <-> ta ) )
5 wrdt2ind.5 
 |-  ps
6 wrdt2ind.6 
 |-  ( ( y e. Word B /\ i e. B /\ j e. B ) -> ( ch -> th ) )
7 oveq2 
 |-  ( n = 0 -> ( 2 x. n ) = ( 2 x. 0 ) )
8 7 eqeq1d 
 |-  ( n = 0 -> ( ( 2 x. n ) = ( # ` x ) <-> ( 2 x. 0 ) = ( # ` x ) ) )
9 8 imbi1d 
 |-  ( n = 0 -> ( ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> ( ( 2 x. 0 ) = ( # ` x ) -> ph ) ) )
10 9 ralbidv 
 |-  ( n = 0 -> ( A. x e. Word B ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> A. x e. Word B ( ( 2 x. 0 ) = ( # ` x ) -> ph ) ) )
11 oveq2 
 |-  ( n = k -> ( 2 x. n ) = ( 2 x. k ) )
12 11 eqeq1d 
 |-  ( n = k -> ( ( 2 x. n ) = ( # ` x ) <-> ( 2 x. k ) = ( # ` x ) ) )
13 12 imbi1d 
 |-  ( n = k -> ( ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> ( ( 2 x. k ) = ( # ` x ) -> ph ) ) )
14 13 ralbidv 
 |-  ( n = k -> ( A. x e. Word B ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> A. x e. Word B ( ( 2 x. k ) = ( # ` x ) -> ph ) ) )
15 oveq2 
 |-  ( n = ( k + 1 ) -> ( 2 x. n ) = ( 2 x. ( k + 1 ) ) )
16 15 eqeq1d 
 |-  ( n = ( k + 1 ) -> ( ( 2 x. n ) = ( # ` x ) <-> ( 2 x. ( k + 1 ) ) = ( # ` x ) ) )
17 16 imbi1d 
 |-  ( n = ( k + 1 ) -> ( ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) ) )
18 17 ralbidv 
 |-  ( n = ( k + 1 ) -> ( A. x e. Word B ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> A. x e. Word B ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) ) )
19 oveq2 
 |-  ( n = m -> ( 2 x. n ) = ( 2 x. m ) )
20 19 eqeq1d 
 |-  ( n = m -> ( ( 2 x. n ) = ( # ` x ) <-> ( 2 x. m ) = ( # ` x ) ) )
21 20 imbi1d 
 |-  ( n = m -> ( ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> ( ( 2 x. m ) = ( # ` x ) -> ph ) ) )
22 21 ralbidv 
 |-  ( n = m -> ( A. x e. Word B ( ( 2 x. n ) = ( # ` x ) -> ph ) <-> A. x e. Word B ( ( 2 x. m ) = ( # ` x ) -> ph ) ) )
23 2t0e0 
 |-  ( 2 x. 0 ) = 0
24 23 eqeq1i 
 |-  ( ( 2 x. 0 ) = ( # ` x ) <-> 0 = ( # ` x ) )
25 eqcom 
 |-  ( 0 = ( # ` x ) <-> ( # ` x ) = 0 )
26 24 25 bitri 
 |-  ( ( 2 x. 0 ) = ( # ` x ) <-> ( # ` x ) = 0 )
27 hasheq0 
 |-  ( x e. Word B -> ( ( # ` x ) = 0 <-> x = (/) ) )
28 26 27 syl5bb 
 |-  ( x e. Word B -> ( ( 2 x. 0 ) = ( # ` x ) <-> x = (/) ) )
29 5 1 mpbiri 
 |-  ( x = (/) -> ph )
30 28 29 syl6bi 
 |-  ( x e. Word B -> ( ( 2 x. 0 ) = ( # ` x ) -> ph ) )
31 30 rgen 
 |-  A. x e. Word B ( ( 2 x. 0 ) = ( # ` x ) -> ph )
32 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
33 32 eqeq2d 
 |-  ( x = y -> ( ( 2 x. k ) = ( # ` x ) <-> ( 2 x. k ) = ( # ` y ) ) )
34 33 2 imbi12d 
 |-  ( x = y -> ( ( ( 2 x. k ) = ( # ` x ) -> ph ) <-> ( ( 2 x. k ) = ( # ` y ) -> ch ) ) )
35 34 cbvralvw 
 |-  ( A. x e. Word B ( ( 2 x. k ) = ( # ` x ) -> ph ) <-> A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) )
36 simprl 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> x e. Word B )
37 0zd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 e. ZZ )
38 lencl 
 |-  ( x e. Word B -> ( # ` x ) e. NN0 )
39 36 38 syl 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) e. NN0 )
40 39 nn0zd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) e. ZZ )
41 2z 
 |-  2 e. ZZ
42 41 a1i 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 e. ZZ )
43 40 42 zsubcld 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. ZZ )
44 2re 
 |-  2 e. RR
45 44 a1i 
 |-  ( k e. NN0 -> 2 e. RR )
46 nn0re 
 |-  ( k e. NN0 -> k e. RR )
47 0le2 
 |-  0 <_ 2
48 47 a1i 
 |-  ( k e. NN0 -> 0 <_ 2 )
49 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
50 45 46 48 49 mulge0d 
 |-  ( k e. NN0 -> 0 <_ ( 2 x. k ) )
51 50 adantr 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 <_ ( 2 x. k ) )
52 2cnd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 e. CC )
53 simpl 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> k e. NN0 )
54 53 nn0cnd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> k e. CC )
55 1cnd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 1 e. CC )
56 52 54 55 adddid 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. ( k + 1 ) ) = ( ( 2 x. k ) + ( 2 x. 1 ) ) )
57 simprr 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. ( k + 1 ) ) = ( # ` x ) )
58 2t1e2 
 |-  ( 2 x. 1 ) = 2
59 58 a1i 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. 1 ) = 2 )
60 59 oveq2d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( 2 x. k ) + ( 2 x. 1 ) ) = ( ( 2 x. k ) + 2 ) )
61 56 57 60 3eqtr3d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) = ( ( 2 x. k ) + 2 ) )
62 61 oveq1d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) = ( ( ( 2 x. k ) + 2 ) - 2 ) )
63 52 54 mulcld 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. k ) e. CC )
64 63 52 pncand 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( ( 2 x. k ) + 2 ) - 2 ) = ( 2 x. k ) )
65 62 64 eqtrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) = ( 2 x. k ) )
66 51 65 breqtrrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 <_ ( ( # ` x ) - 2 ) )
67 43 zred 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. RR )
68 39 nn0red 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) e. RR )
69 2pos 
 |-  0 < 2
70 44 a1i 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 e. RR )
71 70 68 ltsubposd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 0 < 2 <-> ( ( # ` x ) - 2 ) < ( # ` x ) ) )
72 69 71 mpbii 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) < ( # ` x ) )
73 67 68 72 ltled 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) <_ ( # ` x ) )
74 elfz2 
 |-  ( ( ( # ` x ) - 2 ) e. ( 0 ... ( # ` x ) ) <-> ( ( 0 e. ZZ /\ ( # ` x ) e. ZZ /\ ( ( # ` x ) - 2 ) e. ZZ ) /\ ( 0 <_ ( ( # ` x ) - 2 ) /\ ( ( # ` x ) - 2 ) <_ ( # ` x ) ) ) )
75 74 biimpri 
 |-  ( ( ( 0 e. ZZ /\ ( # ` x ) e. ZZ /\ ( ( # ` x ) - 2 ) e. ZZ ) /\ ( 0 <_ ( ( # ` x ) - 2 ) /\ ( ( # ` x ) - 2 ) <_ ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. ( 0 ... ( # ` x ) ) )
76 37 40 43 66 73 75 syl32anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. ( 0 ... ( # ` x ) ) )
77 pfxlen 
 |-  ( ( x e. Word B /\ ( ( # ` x ) - 2 ) e. ( 0 ... ( # ` x ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) = ( ( # ` x ) - 2 ) )
78 36 76 77 syl2anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) = ( ( # ` x ) - 2 ) )
79 78 65 eqtr2d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. k ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) )
80 79 adantlr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. k ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) )
81 fveq2 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( # ` y ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) )
82 81 eqeq2d 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( ( 2 x. k ) = ( # ` y ) <-> ( 2 x. k ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) ) )
83 vex 
 |-  y e. _V
84 83 2 sbcie 
 |-  ( [. y / x ]. ph <-> ch )
85 dfsbcq 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( [. y / x ]. ph <-> [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph ) )
86 84 85 bitr3id 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( ch <-> [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph ) )
87 82 86 imbi12d 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( ( ( 2 x. k ) = ( # ` y ) -> ch ) <-> ( ( 2 x. k ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) -> [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph ) ) )
88 simplr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) )
89 pfxcl 
 |-  ( x e. Word B -> ( x prefix ( ( # ` x ) - 2 ) ) e. Word B )
90 89 ad2antrl 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( x prefix ( ( # ` x ) - 2 ) ) e. Word B )
91 87 88 90 rspcdva 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( 2 x. k ) = ( # ` ( x prefix ( ( # ` x ) - 2 ) ) ) -> [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph ) )
92 80 91 mpd 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph )
93 2nn0 
 |-  2 e. NN0
94 93 a1i 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 e. NN0 )
95 52 addid2d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 0 + 2 ) = 2 )
96 0red 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 e. RR )
97 65 67 eqeltrrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. k ) e. RR )
98 96 97 70 51 leadd1dd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 0 + 2 ) <_ ( ( 2 x. k ) + 2 ) )
99 95 98 eqbrtrrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 <_ ( ( 2 x. k ) + 2 ) )
100 99 61 breqtrrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 <_ ( # ` x ) )
101 nn0sub 
 |-  ( ( 2 e. NN0 /\ ( # ` x ) e. NN0 ) -> ( 2 <_ ( # ` x ) <-> ( ( # ` x ) - 2 ) e. NN0 ) )
102 101 biimpa 
 |-  ( ( ( 2 e. NN0 /\ ( # ` x ) e. NN0 ) /\ 2 <_ ( # ` x ) ) -> ( ( # ` x ) - 2 ) e. NN0 )
103 94 39 100 102 syl21anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. NN0 )
104 68 recnd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) e. CC )
105 104 52 55 subsubd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - ( 2 - 1 ) ) = ( ( ( # ` x ) - 2 ) + 1 ) )
106 2m1e1 
 |-  ( 2 - 1 ) = 1
107 106 a1i 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 - 1 ) = 1 )
108 107 oveq2d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - ( 2 - 1 ) ) = ( ( # ` x ) - 1 ) )
109 105 108 eqtr3d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( ( # ` x ) - 2 ) + 1 ) = ( ( # ` x ) - 1 ) )
110 68 lem1d 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 1 ) <_ ( # ` x ) )
111 109 110 eqbrtrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( ( # ` x ) - 2 ) + 1 ) <_ ( # ` x ) )
112 nn0p1elfzo 
 |-  ( ( ( ( # ` x ) - 2 ) e. NN0 /\ ( # ` x ) e. NN0 /\ ( ( ( # ` x ) - 2 ) + 1 ) <_ ( # ` x ) ) -> ( ( # ` x ) - 2 ) e. ( 0 ..^ ( # ` x ) ) )
113 103 39 111 112 syl3anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 2 ) e. ( 0 ..^ ( # ` x ) ) )
114 wrdsymbcl 
 |-  ( ( x e. Word B /\ ( ( # ` x ) - 2 ) e. ( 0 ..^ ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 2 ) ) e. B )
115 36 113 114 syl2anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 2 ) ) e. B )
116 115 adantlr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 2 ) ) e. B )
117 nn0ge2m1nn0 
 |-  ( ( ( # ` x ) e. NN0 /\ 2 <_ ( # ` x ) ) -> ( ( # ` x ) - 1 ) e. NN0 )
118 39 100 117 syl2anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 1 ) e. NN0 )
119 104 55 npcand 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( ( # ` x ) - 1 ) + 1 ) = ( # ` x ) )
120 68 leidd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( # ` x ) <_ ( # ` x ) )
121 119 120 eqbrtrd 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( ( # ` x ) - 1 ) + 1 ) <_ ( # ` x ) )
122 nn0p1elfzo 
 |-  ( ( ( ( # ` x ) - 1 ) e. NN0 /\ ( # ` x ) e. NN0 /\ ( ( ( # ` x ) - 1 ) + 1 ) <_ ( # ` x ) ) -> ( ( # ` x ) - 1 ) e. ( 0 ..^ ( # ` x ) ) )
123 118 39 121 122 syl3anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ( # ` x ) - 1 ) e. ( 0 ..^ ( # ` x ) ) )
124 wrdsymbcl 
 |-  ( ( x e. Word B /\ ( ( # ` x ) - 1 ) e. ( 0 ..^ ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 1 ) ) e. B )
125 36 123 124 syl2anc 
 |-  ( ( k e. NN0 /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 1 ) ) e. B )
126 125 adantlr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( x ` ( ( # ` x ) - 1 ) ) e. B )
127 oveq1 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( y ++ <" i j "> ) = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) )
128 127 sbceq1d 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( [. ( y ++ <" i j "> ) / x ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) / x ]. ph ) )
129 85 128 imbi12d 
 |-  ( y = ( x prefix ( ( # ` x ) - 2 ) ) -> ( ( [. y / x ]. ph -> [. ( y ++ <" i j "> ) / x ]. ph ) <-> ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) / x ]. ph ) ) )
130 id 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> i = ( x ` ( ( # ` x ) - 2 ) ) )
131 eqidd 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> j = j )
132 130 131 s2eqd 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> <" i j "> = <" ( x ` ( ( # ` x ) - 2 ) ) j "> )
133 132 oveq2d 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) )
134 133 sbceq1d 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> ( [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) / x ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) / x ]. ph ) )
135 134 imbi2d 
 |-  ( i = ( x ` ( ( # ` x ) - 2 ) ) -> ( ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" i j "> ) / x ]. ph ) <-> ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) / x ]. ph ) ) )
136 eqidd 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> ( x ` ( ( # ` x ) - 2 ) ) = ( x ` ( ( # ` x ) - 2 ) ) )
137 id 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> j = ( x ` ( ( # ` x ) - 1 ) ) )
138 136 137 s2eqd 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> <" ( x ` ( ( # ` x ) - 2 ) ) j "> = <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> )
139 138 oveq2d 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) )
140 139 sbceq1d 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> ( [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) / x ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) )
141 140 imbi2d 
 |-  ( j = ( x ` ( ( # ` x ) - 1 ) ) -> ( ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) j "> ) / x ]. ph ) <-> ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) ) )
142 ovex 
 |-  ( y ++ <" i j "> ) e. _V
143 142 3 sbcie 
 |-  ( [. ( y ++ <" i j "> ) / x ]. ph <-> th )
144 6 84 143 3imtr4g 
 |-  ( ( y e. Word B /\ i e. B /\ j e. B ) -> ( [. y / x ]. ph -> [. ( y ++ <" i j "> ) / x ]. ph ) )
145 129 135 141 144 vtocl3ga 
 |-  ( ( ( x prefix ( ( # ` x ) - 2 ) ) e. Word B /\ ( x ` ( ( # ` x ) - 2 ) ) e. B /\ ( x ` ( ( # ` x ) - 1 ) ) e. B ) -> ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) )
146 90 116 126 145 syl3anc 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( [. ( x prefix ( ( # ` x ) - 2 ) ) / x ]. ph -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) )
147 92 146 mpd 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph )
148 simprl 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> x e. Word B )
149 1red 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 1 e. RR )
150 simpll 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> k e. NN0 )
151 150 nn0red 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> k e. RR )
152 151 149 readdcld 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( k + 1 ) e. RR )
153 44 a1i 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 e. RR )
154 47 a1i 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 <_ 2 )
155 0p1e1 
 |-  ( 0 + 1 ) = 1
156 0red 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 e. RR )
157 150 nn0ge0d 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 0 <_ k )
158 149 leidd 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 1 <_ 1 )
159 156 149 151 149 157 158 le2addd 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 0 + 1 ) <_ ( k + 1 ) )
160 155 159 eqbrtrrid 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 1 <_ ( k + 1 ) )
161 149 152 153 154 160 lemul2ad 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. 1 ) <_ ( 2 x. ( k + 1 ) ) )
162 58 161 eqbrtrrid 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 <_ ( 2 x. ( k + 1 ) ) )
163 simprr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( 2 x. ( k + 1 ) ) = ( # ` x ) )
164 162 163 breqtrd 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> 2 <_ ( # ` x ) )
165 eqid 
 |-  ( # ` x ) = ( # ` x )
166 165 pfxlsw2ccat 
 |-  ( ( x e. Word B /\ 2 <_ ( # ` x ) ) -> x = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) )
167 166 eqcomd 
 |-  ( ( x e. Word B /\ 2 <_ ( # ` x ) ) -> ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) = x )
168 167 eqcomd 
 |-  ( ( x e. Word B /\ 2 <_ ( # ` x ) ) -> x = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) )
169 148 164 168 syl2anc 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> x = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) )
170 sbceq1a 
 |-  ( x = ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) -> ( ph <-> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) )
171 169 170 syl 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ( ph <-> [. ( ( x prefix ( ( # ` x ) - 2 ) ) ++ <" ( x ` ( ( # ` x ) - 2 ) ) ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. ph ) )
172 147 171 mpbird 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ ( x e. Word B /\ ( 2 x. ( k + 1 ) ) = ( # ` x ) ) ) -> ph )
173 172 expr 
 |-  ( ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) /\ x e. Word B ) -> ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) )
174 173 ralrimiva 
 |-  ( ( k e. NN0 /\ A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) ) -> A. x e. Word B ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) )
175 174 ex 
 |-  ( k e. NN0 -> ( A. y e. Word B ( ( 2 x. k ) = ( # ` y ) -> ch ) -> A. x e. Word B ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) ) )
176 35 175 syl5bi 
 |-  ( k e. NN0 -> ( A. x e. Word B ( ( 2 x. k ) = ( # ` x ) -> ph ) -> A. x e. Word B ( ( 2 x. ( k + 1 ) ) = ( # ` x ) -> ph ) ) )
177 10 14 18 22 31 176 nn0ind 
 |-  ( m e. NN0 -> A. x e. Word B ( ( 2 x. m ) = ( # ` x ) -> ph ) )
178 177 adantl 
 |-  ( ( A e. Word B /\ m e. NN0 ) -> A. x e. Word B ( ( 2 x. m ) = ( # ` x ) -> ph ) )
179 simpl 
 |-  ( ( A e. Word B /\ m e. NN0 ) -> A e. Word B )
180 fveq2 
 |-  ( x = A -> ( # ` x ) = ( # ` A ) )
181 180 eqeq2d 
 |-  ( x = A -> ( ( 2 x. m ) = ( # ` x ) <-> ( 2 x. m ) = ( # ` A ) ) )
182 181 4 imbi12d 
 |-  ( x = A -> ( ( ( 2 x. m ) = ( # ` x ) -> ph ) <-> ( ( 2 x. m ) = ( # ` A ) -> ta ) ) )
183 182 adantl 
 |-  ( ( ( A e. Word B /\ m e. NN0 ) /\ x = A ) -> ( ( ( 2 x. m ) = ( # ` x ) -> ph ) <-> ( ( 2 x. m ) = ( # ` A ) -> ta ) ) )
184 179 183 rspcdv 
 |-  ( ( A e. Word B /\ m e. NN0 ) -> ( A. x e. Word B ( ( 2 x. m ) = ( # ` x ) -> ph ) -> ( ( 2 x. m ) = ( # ` A ) -> ta ) ) )
185 178 184 mpd 
 |-  ( ( A e. Word B /\ m e. NN0 ) -> ( ( 2 x. m ) = ( # ` A ) -> ta ) )
186 185 imp 
 |-  ( ( ( A e. Word B /\ m e. NN0 ) /\ ( 2 x. m ) = ( # ` A ) ) -> ta )
187 186 adantllr 
 |-  ( ( ( ( A e. Word B /\ 2 || ( # ` A ) ) /\ m e. NN0 ) /\ ( 2 x. m ) = ( # ` A ) ) -> ta )
188 lencl 
 |-  ( A e. Word B -> ( # ` A ) e. NN0 )
189 evennn02n 
 |-  ( ( # ` A ) e. NN0 -> ( 2 || ( # ` A ) <-> E. m e. NN0 ( 2 x. m ) = ( # ` A ) ) )
190 189 biimpa 
 |-  ( ( ( # ` A ) e. NN0 /\ 2 || ( # ` A ) ) -> E. m e. NN0 ( 2 x. m ) = ( # ` A ) )
191 188 190 sylan 
 |-  ( ( A e. Word B /\ 2 || ( # ` A ) ) -> E. m e. NN0 ( 2 x. m ) = ( # ` A ) )
192 187 191 r19.29a 
 |-  ( ( A e. Word B /\ 2 || ( # ` A ) ) -> ta )