MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  extwwlkfablem2 Structured version   Unicode version

Theorem extwwlkfablem2 25205
Description: Lemma 2 for extwwlkfab 25217. (Contributed by Alexander van der Vekens, 15-Sep-2018.)
Hypothesis
Ref Expression
numclwwlk.c  |-  C  =  ( n  e.  NN0  |->  ( ( V ClWWalksN  E ) `
 n ) )
Assertion
Ref Expression
extwwlkfablem2  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N ) )  /\  ( ( w ` 
0 )  =  X  /\  ( w `  ( N  -  2
) )  =  ( w `  0 ) ) )  ->  (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  ( C `  ( N  -  2 ) ) )
Distinct variable groups:    n, E    n, N    n, V
Allowed substitution hints:    C( w, n)    E( w)    N( w)    V( w)    X( w, n)

Proof of Theorem extwwlkfablem2
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 usgrav 24465 . . . . . . . . . . 11  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
2 uzuzle23 11146 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
3 eluzge2nn0 11145 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  2
)  ->  N  e.  NN0 )
42, 3syl 16 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  NN0 )
51, 4anim12i 566 . . . . . . . . . 10  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  N  e.  NN0 ) )
6 df-3an 975 . . . . . . . . . 10  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  N  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  N  e.  NN0 ) )
75, 6sylibr 212 . . . . . . . . 9  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( V  e.  _V  /\  E  e. 
_V  /\  N  e.  NN0 ) )
8 isclwwlkn 24896 . . . . . . . . 9  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  N  e.  NN0 )  ->  (
w  e.  ( ( V ClWWalksN  E ) `  N
)  <->  ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N ) ) )
97, 8syl 16 . . . . . . . 8  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  <->  ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N ) ) )
1093adant2 1015 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  <->  ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N ) ) )
11 isclwwlk 24895 . . . . . . . . . 10  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( w  e.  ( V ClWWalks  E )  <->  ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E ) ) )
1211anbi1d 704 . . . . . . . . 9  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N )  <-> 
( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) ) )
131, 12syl 16 . . . . . . . 8  |-  ( V USGrph  E  ->  ( ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N )  <-> 
( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) ) )
14133ad2ant1 1017 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
w  e.  ( V ClWWalks  E )  /\  ( # `
 w )  =  N )  <->  ( (
w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) ) )
1510, 14bitrd 253 . . . . . 6  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  <->  ( (
w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) ) )
16 swrdcl 12655 . . . . . . . . . . . 12  |-  ( w  e. Word  V  ->  (
w substr  <. 0 ,  ( N  -  2 )
>. )  e. Word  V )
17163ad2ant1 1017 . . . . . . . . . . 11  |-  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  ->  ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V )
1817adantr 465 . . . . . . . . . 10  |-  ( ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V )
1918ad2antlr 726 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V )
20 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( (
# `  w )  -  1 )  =  ( N  -  1 ) )
2120adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  =  ( N  - 
1 ) )
22 1le3 10773 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  <_  3
23 1red 9628 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  RR )
24 3re 10630 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  3  e.  RR
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  RR )
26 eluzelre 11116 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  RR )
2723, 25, 26lesub2d 10181 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  <_  3  <->  ( N  -  3 )  <_ 
( N  -  1 ) ) )
2822, 27mpbii 211 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  1 ) )
29 eluzelz 11115 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
30 eluzel2 11111 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  ZZ )
3129, 30zsubcld 10995 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  e.  ZZ )
32 peano2zm 10928 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
3329, 32syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
34 eluz 11119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  1
)  e.  ZZ )  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  1 ) ) )
3531, 33, 34syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  1 ) ) )
3628, 35mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
3736adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  1 )  e.  ( ZZ>= `  ( N  -  3
) ) )
3821, 37eqeltrd 2545 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
39 fzoss2 11852 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( ( # `  w )  -  1 ) ) )
40 ssralv 3560 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0..^ ( N  - 
3 ) )  C_  ( 0..^ ( ( # `  w )  -  1 ) )  ->  ( A. i  e.  (
0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( N  -  3 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
) )
4138, 39, 403syl 20 . . . . . . . . . . . . . . . . 17  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( w `  i
) ,  ( w `
 ( i  +  1 ) ) }  e.  ran  E ) )
4241adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( w `  i
) ,  ( w `
 ( i  +  1 ) ) }  e.  ran  E ) )
43 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  w  e. Word  V
)
44 1eluzge0 11149 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  ( ZZ>= `  0 )
45 fzss1 11748 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
4644, 45mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
47 ige3m2fz 11734 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... N
) )
4846, 47sseldd 3500 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 0 ... N
) )
4948adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... N ) )
50 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  w )  =  N  ->  ( 0 ... ( # `  w
) )  =  ( 0 ... N ) )
5150eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 0 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5251adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  e.  ( 0 ... ( # `  w ) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5349, 52mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... ( # `  w
) ) )
5453ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( N  - 
2 )  e.  ( 0 ... ( # `  w ) ) )
55 2re 10626 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  RR
56 2lt3 10724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  <  3
5755, 24, 56ltleii 9724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  <_  3
5855a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  RR )
5958, 25, 26lesub2d 10181 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  <_  3  <->  ( N  -  3 )  <_ 
( N  -  2 ) ) )
6057, 59mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  2 ) )
61 2z 10917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  2  e.  ZZ
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  ZZ )
6329, 62zsubcld 10995 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ZZ )
64 eluz 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  2
)  e.  ZZ )  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  2 ) ) )
6531, 63, 64syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  2 ) ) )
6660, 65mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
67 fzoss2 11852 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
6866, 67syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
6968sseld 3498 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7069ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7170imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) )
72 swrd0fv 12675 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 0 ... ( # `  w
) )  /\  i  e.  ( 0..^ ( N  -  2 ) ) )  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. ) `  i )  =  ( w `  i ) )
7343, 54, 71, 72syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i )  =  ( w `  i ) )
7473eqcomd 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( w `  i )  =  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) )
75 elfzonn0 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  NN0 )
7675adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  i  e.  NN0 )
77 peano2nn0 10857 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
7876, 77syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e. 
NN0 )
79 uz3m2nn 11148 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  NN )
8079adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( N  -  2 )  e.  NN )
81 elfzo0 11862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  <->  ( i  e. 
NN0  /\  ( N  -  3 )  e.  NN  /\  i  < 
( N  -  3 ) ) )
82 nn0cn 10826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( i  e.  NN0  ->  i  e.  CC )
83 ax-1cn 9567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  1  e.  CC
8482, 83jctir 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( i  e.  NN0  ->  ( i  e.  CC  /\  1  e.  CC ) )
8584adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  e.  CC  /\  1  e.  CC ) )
86 pncan 9845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  CC  /\  1  e.  CC )  ->  ( ( i  +  1 )  -  1 )  =  i )
8785, 86syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  =  i )
8887eqcomd 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
i  =  ( ( i  +  1 )  -  1 ) )
89 eluzelcn 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  CC )
9089adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  CC )
91 2cnd 10629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
2  e.  CC )
92 1cnd 9629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  CC )
9390, 91, 92subsub4d 9981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  -  1 )  =  ( N  -  ( 2  +  1 ) ) )
94 df-3 10616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  3  =  ( 2  +  1 )
9594oveq2i 6307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  -  3 )  =  ( N  -  (
2  +  1 ) )
9693, 95syl6reqr 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  3 )  =  ( ( N  -  2 )  -  1 ) )
9788, 96breq12d 4469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  <-> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
9897biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  ->  ( ( i  +  1 )  - 
1 )  <  (
( N  -  2 )  -  1 ) ) )
9998impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
100993adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
101100imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) )
102 nn0re 10825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  NN0  ->  i  e.  RR )
103 peano2re 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  RR  ->  (
i  +  1 )  e.  RR )
104102, 103syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  NN0  ->  ( i  +  1 )  e.  RR )
1051043ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( i  +  1 )  e.  RR )
106105adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  e.  RR )
10726, 58resubcld 10008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  RR )
108107adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  RR )
109 1red 9628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  RR )
110106, 108, 109ltsub1d 10182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  <  ( N  -  2 )  <-> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
111101, 110mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  <  ( N  -  2 ) )
112111ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( i  +  1 )  <  ( N  -  2 ) ) )
11381, 112sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( i  +  1 )  <  ( N  -  2 ) ) )
114113impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  < 
( N  -  2 ) )
115 elfzo0 11862 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) )  <->  ( ( i  +  1 )  e. 
NN0  /\  ( N  -  2 )  e.  NN  /\  ( i  +  1 )  < 
( N  -  2 ) ) )
11678, 80, 114, 115syl3anbrc 1180 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) ) )
117116ex 434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
118117ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
119118imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) )
120 swrd0fv 12675 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 0 ... ( # `  w
) )  /\  (
i  +  1 )  e.  ( 0..^ ( N  -  2 ) ) )  ->  (
( w substr  <. 0 ,  ( N  -  2 ) >. ) `  (
i  +  1 ) )  =  ( w `
 ( i  +  1 ) ) )
12143, 54, 119, 120syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) )  =  ( w `  ( i  +  1 ) ) )
122121eqcomd 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( w `  ( i  +  1 ) )  =  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) )
12374, 122preq12d 4119 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  =  {
( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) } )
124123eleq1d 2526 . . . . . . . . . . . . . . . . 17  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E
) )
125124ralbidva 2893 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( A. i  e.  ( 0..^ ( N  -  3 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( N  -  3 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E ) )
12642, 125sylibd 214 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E ) )
127126impancom 440 . . . . . . . . . . . . . 14  |-  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E )  ->  ( (
( # `  w )  =  N  /\  N  e.  ( ZZ>= `  3 )
)  ->  A. i  e.  ( 0..^ ( N  -  3 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E
) )
1281273adant3 1016 . . . . . . . . . . . . 13  |-  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  ->  ( ( (
# `  w )  =  N  /\  N  e.  ( ZZ>= `  3 )
)  ->  A. i  e.  ( 0..^ ( N  -  3 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E
) )
129128expdimp 437 . . . . . . . . . . . 12  |-  ( ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( N  e.  ( ZZ>= `  3 )  ->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E ) )
130129impcom 430 . . . . . . . . . . 11  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  A. i  e.  ( 0..^ ( N  -  3 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E
)
131130adantr 465 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E )
132 simprl1 1041 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  w  e. Word  V )
133 simprr 757 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  ( # `  w
)  =  N )
1342adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  N  e.  ( ZZ>= `  2 )
)
135132, 133, 1343jca 1176 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  ( w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  (
ZZ>= `  2 ) ) )
136135adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) )
137 extwwlkfablem2lem 25202 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  ( ZZ>= `  2 )
)  ->  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) )
138136, 137syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) )
139138oveq1d 6311 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 )  =  ( ( N  -  2 )  - 
1 ) )
140139oveq2d 6312 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) )  =  ( 0..^ ( ( N  -  2 )  - 
1 ) ) )
141 2cnd 10629 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  CC )
142 1cnd 9629 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  CC )
14389, 141, 142subsub4d 9981 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  (
2  +  1 ) ) )
144 2p1e3 10680 . . . . . . . . . . . . . . . . 17  |-  ( 2  +  1 )  =  3
145144a1i 11 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  +  1 )  =  3 )
146145oveq2d 6312 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  =  ( N  -  3 ) )
147143, 146eqtrd 2498 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
148147ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( ( N  -  2 )  - 
1 )  =  ( N  -  3 ) )
149148oveq2d 6312 . . . . . . . . . . . 12  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( 0..^ ( ( N  -  2 )  -  1 ) )  =  ( 0..^ ( N  -  3 ) ) )
150140, 149eqtrd 2498 . . . . . . . . . . 11  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) )  =  ( 0..^ ( N  - 
3 ) ) )
151150raleqdv 3060 . . . . . . . . . 10  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( A. i  e.  ( 0..^ ( (
# `  ( w substr  <.
0 ,  ( N  -  2 ) >.
) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  ( 0..^ ( N  - 
3 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E ) )
152131, 151mpbird 232 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  A. i  e.  ( 0..^ ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E
)
15320oveq2d 6312 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( 0..^ ( ( # `  w
)  -  1 ) )  =  ( 0..^ ( N  -  1 ) ) )
154153raleqdv 3060 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  w )  =  N  ->  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  <->  A. i  e.  (
0..^ ( N  - 
1 ) ) { ( w `  i
) ,  ( w `
 ( i  +  1 ) ) }  e.  ran  E ) )
155 simplr 755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  w  e. Word  V )
156 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  w )  =  N  ->  ( 1 ... ( # `  w
) )  =  ( 1 ... N ) )
157156eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 1 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 1 ... N
) ) )
15847, 157syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
159158ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( # `  w
)  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E )  /\  w  e. Word  V )  ->  ( N  e.  ( ZZ>= ` 
3 )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) ) )
160159com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
( ( # `  w
)  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E )  /\  w  e. Word  V )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) ) )
161160adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  -> 
( ( ( (
# `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
162161impcom 430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) )
163 swrd0fvlsw 12679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( w `
 ( ( N  -  2 )  - 
1 ) ) )
164155, 162, 163syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( w `
 ( ( N  -  2 )  - 
1 ) ) )
16547adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... N ) )
166156adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( 1 ... ( # `
 w ) )  =  ( 1 ... N ) )
167165, 166eleqtrrd 2548 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... ( # `  w
) ) )
168167ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
169168ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( # `  w
)  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E )  /\  w  e. Word  V )  ->  ( N  e.  ( ZZ>= ` 
3 )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) ) )
170169com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
( ( # `  w
)  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E )  /\  w  e. Word  V )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) ) )
171170adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  -> 
( ( ( (
# `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
172171impcom 430 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  ( N  -  2 )  e.  ( 1 ... ( # `  w
) ) )
173 swrd0fv0 12676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 )  =  ( w `  0
) )
174155, 172, 173syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  (
( w substr  <. 0 ,  ( N  -  2 ) >. ) `  0
)  =  ( w `
 0 ) )
175164, 174preq12d 4119 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  =  { ( w `  ( ( N  -  2 )  -  1 ) ) ,  ( w ` 
0 ) } )
176 cnm2m1cnm3 10811 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  CC  ->  (
( N  -  2 )  -  1 )  =  ( N  - 
3 ) )
17789, 176syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
178177fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
2 )  -  1 ) )  =  ( w `  ( N  -  3 ) ) )
179178ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  (
w `  ( ( N  -  2 )  -  1 ) )  =  ( w `  ( N  -  3
) ) )
180 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( w `  0 )  =  ( w `  ( N  -  2
) )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
181180eqcoms 2469 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( w `  ( N  -  2 ) )  =  ( w ` 
0 )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
182181ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
183179, 182preq12d 4119 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  { ( w `  ( ( N  -  2 )  -  1 ) ) ,  ( w ` 
0 ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) } )
184 eluzfz2b 11720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  <->  N  e.  (
3 ... N ) )
185 fzval3 11888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ZZ  ->  (
3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
18629, 185syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
187186eleq2d 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  <->  N  e.  (
3..^ ( N  + 
1 ) ) ) )
188 peano2z 10926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
189 zadd2cl 10997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  2 )  e.  ZZ )
190 1le2 10770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  1  <_  2
191 1red 9628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  1  e.  RR )
19255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  2  e.  RR )
193 zre 10889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  N  e.  RR )
194191, 192, 193leadd2d 10168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( N  e.  ZZ  ->  (
1  <_  2  <->  ( N  +  1 )  <_ 
( N  +  2 ) ) )
195190, 194mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  <_  ( N  + 
2 ) )
196188, 189, 1953jca 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ZZ  ->  (
( N  +  1 )  e.  ZZ  /\  ( N  +  2
)  e.  ZZ  /\  ( N  +  1
)  <_  ( N  +  2 ) ) )
19729, 196syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_  ( N  + 
2 ) ) )
198 eluz2 11112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  <->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_ 
( N  +  2 ) ) )
199197, 198sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) ) )
200 fzoss2 11852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
201199, 200syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
202201sseld 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( N  +  1 ) )  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
203187, 202sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
204184, 203syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( ZZ>= `  3 )  ->  N  e.  ( 3..^ ( N  +  2 ) ) ) )
205204pm2.43i 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) )
206 3cn 10631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  3  e.  CC
207206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  CC )
208207, 89, 142addsub12d 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  ( 3  -  1 ) ) )
209 3m1e2 10673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 3  -  1 )  =  2
210209oveq2i 6307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  +  ( 3  -  1 ) )  =  ( N  +  2 )
211208, 210syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  2 ) )
212211oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( 3  +  ( N  -  1 ) ) )  =  ( 3..^ ( N  + 
2 ) ) )
213205, 212eleqtrrd 2548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) ) )
214213, 33jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( 3  +  ( N  - 
1 ) ) )  /\  ( N  - 
1 )  e.  ZZ ) )
215 fzosubel3 11880 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) )  /\  ( N  -  1 )  e.  ZZ )  -> 
( N  -  3 )  e.  ( 0..^ ( N  -  1 ) ) )
216 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  i )  =  ( w `  ( N  -  3
) ) )
217 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  ( N  - 
3 )  ->  (
i  +  1 )  =  ( ( N  -  3 )  +  1 ) )
218217fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  ( i  +  1 ) )  =  ( w `  ( ( N  - 
3 )  +  1 ) ) )
219216, 218preq12d 4119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  ( N  - 
3 )  ->  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( ( N  -  3 )  +  1 ) ) } )
220219eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  =  ( N  - 
3 )  ->  ( { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( w `  ( N  -  3 ) ) ,  ( w `
 ( ( N  -  3 )  +  1 ) ) }  e.  ran  E ) )
221220rspcv 3206 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  -  3 )  e.  ( 0..^ ( N  -  1 ) )  ->  ( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( ( N  - 
3 )  +  1 ) ) }  e.  ran  E ) )
222214, 215, 2213syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( ( N  - 
3 )  +  1 ) ) }  e.  ran  E ) )
22389, 207, 142subsubd 9978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( ( N  - 
3 )  +  1 ) )
224209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  -  1 )  =  2 )
225224oveq2d 6312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( N  -  2 ) )
226223, 225eqtr3d 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  3 )  +  1 )  =  ( N  -  2 ) )
227226fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
3 )  +  1 ) )  =  ( w `  ( N  -  2 ) ) )
228227preq2d 4118 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( ( N  - 
3 )  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) } )
229228eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( {
( w `  ( N  -  3 ) ) ,  ( w `
 ( ( N  -  3 )  +  1 ) ) }  e.  ran  E  <->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( N  -  2
) ) }  e.  ran  E ) )
230222, 229sylibd 214 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( N  -  2
) ) }  e.  ran  E ) )
231230adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  -> 
( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) }  e.  ran  E
) )
232231com12 31 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  ->  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) }  e.  ran  E
) )
233232ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( # `  w
)  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E )  /\  w  e. Word  V )  ->  (
( N  e.  (
ZZ>= `  3 )  /\  ( w `  ( N  -  2 ) )  =  ( w `
 0 ) )  ->  { ( w `
 ( N  - 
3 ) ) ,  ( w `  ( N  -  2 ) ) }  e.  ran  E ) )
234233imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  { ( w `  ( N  -  3 ) ) ,  ( w `  ( N  -  2
) ) }  e.  ran  E )
235183, 234eqeltrd 2545 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  { ( w `  ( ( N  -  2 )  -  1 ) ) ,  ( w ` 
0 ) }  e.  ran  E )
236175, 235eqeltrd 2545 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( # `  w )  =  N  /\  A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E
)  /\  w  e. Word  V )  /\  ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
)
237236exp41 610 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  w )  =  N  ->  ( A. i  e.  ( 0..^ ( N  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  ( w  e. Word  V  ->  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  -  2 ) >.
) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) ) ) )
238154, 237sylbid 215 . . . . . . . . . . . . . . . . . 18  |-  ( (
# `  w )  =  N  ->  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  ->  ( w  e. Word  V  ->  ( ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) ) )
239238com13 80 . . . . . . . . . . . . . . . . 17  |-  ( w  e. Word  V  ->  ( A. i  e.  (
0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  ->  ( ( # `
 w )  =  N  ->  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  -  2 ) >.
) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) ) ) )
240239imp 429 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E )  ->  ( ( # `
 w )  =  N  ->  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  -  2 ) >.
) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) ) )
2412403adant3 1016 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  ->  ( ( # `  w )  =  N  ->  ( ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) )
242241imp 429 . . . . . . . . . . . . . 14  |-  ( ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( ( N  e.  ( ZZ>= `  3
)  /\  ( w `  ( N  -  2 ) )  =  ( w `  0 ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) )
243242expd 436 . . . . . . . . . . . . 13  |-  ( ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( ( w `  ( N  -  2
) )  =  ( w `  0 )  ->  { ( lastS  `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) ) )
244243impcom 430 . . . . . . . . . . . 12  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N ) )  ->  ( (
w `  ( N  -  2 ) )  =  ( w ` 
0 )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) )
245244com12 31 . . . . . . . . . . 11  |-  ( ( w `  ( N  -  2 ) )  =  ( w ` 
0 )  ->  (
( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) )
246245adantl 466 . . . . . . . . . 10  |-  ( ( ( w `  0
)  =  X  /\  ( w `  ( N  -  2 ) )  =  ( w `
 0 ) )  ->  ( ( N  e.  ( ZZ>= `  3
)  /\  ( (
w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  ->  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) )
247246impcom 430 . . . . . . . . 9  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  { ( lastS  `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E )
24819, 152, 2473jca 1176 . . . . . . . 8  |-  ( ( ( N  e.  (
ZZ>= `  3 )  /\  ( ( w  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  E )  /\  ( # `  w
)  =  N ) )  /\  ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) ) )  ->  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
)  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) )
249248exp31 604 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  ( w substr  <.
0 ,  ( N  -  2 ) >.
) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) ) )
2502493ad2ant3 1019 . . . . . 6  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( w  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  E
)  /\  ( # `  w
)  =  N )  ->  ( ( ( w `  0 )  =  X  /\  (
w `  ( N  -  2 ) )  =  ( w ` 
0 ) )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  ( w substr  <.
0 ,  ( N  -  2 ) >.
) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) ) )
25115, 250sylbid 215 . . . . 5  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  -> 
( ( ( w `
 0 )  =  X  /\  ( w `
 ( N  - 
2 ) )  =  ( w `  0
) )  ->  (
( w substr  <. 0 ,  ( N  -  2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) ) ) )
252251imp31 432 . . . 4  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N ) )  /\  ( ( w ` 
0 )  =  X  /\  ( w `  ( N  -  2
) )  =  ( w `  0 ) ) )  ->  (
( w substr  <. 0 ,  ( N  -  2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E ) )
253 clwwlknprop 24899 . . . . . . . . . 10  |-  ( w  e.  ( ( V ClWWalksN  E ) `  N
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) ) )
254 simpl2 1000 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  w  e. Word  V )
255 simpl3r 1052 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( # `  w )  =  N )
2562adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  ( ZZ>= ` 
2 ) )
257254, 255, 2563jca 1176 . . . . . . . . . . 11  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) )
258257ex 434 . . . . . . . . . 10  |-  ( ( ( V  e.  _V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `  w
)  =  N ) )  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
259253, 258syl 16 . . . . . . . . 9  |-  ( w  e.  ( ( V ClWWalksN  E ) `  N
)  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
260259com12 31 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  -> 
( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
2612603ad2ant3 1019 . . . . . . 7  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  -> 
( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
262261imp 429 . . . . . 6  |-  ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= ` 
3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N
) )  ->  (
w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  ( ZZ>= `  2 )
) )
263262adantr 465 . . . . 5  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N ) )  /\  ( ( w ` 
0 )  =  X  /\  ( w `  ( N  -  2
) )  =  ( w `  0 ) ) )  ->  (
w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  ( ZZ>= `  2 )
) )
264263, 137syl 16 . . . 4  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N ) )  /\  ( ( w ` 
0 )  =  X  /\  ( w `  ( N  -  2
) )  =  ( w `  0 ) ) )  ->  ( # `
 ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( N  -  2 ) )
265252, 264jca 532 . . 3  |-  ( ( ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>=
`  3 ) )  /\  w  e.  ( ( V ClWWalksN  E ) `  N ) )  /\  ( ( w ` 
0 )  =  X  /\  ( w `  ( N  -  2
) )  =  ( w `  0 ) ) )  ->  (
( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  ( w substr  <.
0 ,  ( N  -  2 ) >.
) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
)  /\  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) ) )
266 uznn0sub 11137 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  2 )  e. 
NN0 )
2672, 266syl 16 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e. 
NN0 )
2681, 267anim12i 566 . . . . . . . 8  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
269 df-3an 975 . . . . . . . 8  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  -  2 )  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
270268, 269sylibr 212 . . . . . . 7  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( V  e.  _V  /\  E  e. 
_V  /\  ( N  -  2 )  e. 
NN0 ) )
271 isclwwlkn 24896 . . . . . . 7  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  -  2 )  e.  NN0 )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e.  ( ( V ClWWalksN  E ) `
 ( N  - 
2 ) )  <->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( N  -  2 ) ) ) )
272270, 271syl 16 . . . . . 6  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  (
( V ClWWalksN  E ) `  ( N  -  2
) )  <->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( N  -  2 ) ) ) )
273 isclwwlk 24895 . . . . . . . . 9  |-  ( ( V  e.  _V  /\  E  e.  _V )  ->  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e.  ( V ClWWalks  E )  <->  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( (
# `  ( w substr  <.
0 ,  ( N  -  2 ) >.
) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) )
2741, 273syl 16 . . . . . . . 8  |-  ( V USGrph  E  ->  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
)  e.  ( V ClWWalks  E )  <->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) )
275274adantr 465 . . . . . . 7  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  ( V ClWWalks  E )  <->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
) ) )
276275anbi1d 704 . . . . . 6  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
( w substr  <. 0 ,  ( N  -  2 ) >. )  e.  ( V ClWWalks  E )  /\  ( # `
 ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( N  -  2 ) )  <-> 
( ( ( w substr  <. 0 ,  ( N  -  2 ) >.
)  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
) ,  ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  0 ) }  e.  ran  E
)  /\  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) ) ) )
277272, 276bitrd 253 . . . . 5  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  (
( V ClWWalksN  E ) `  ( N  -  2
) )  <->  ( (
( w substr  <. 0 ,  ( N  -  2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.  ran  E  /\  { ( lastS  `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) ) ,  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 ) }  e.  ran  E )  /\  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) ) ) )
2782773adant2 1015 . . . 4  |-  ( ( V USGrph  E  /\  X  e.  V  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. )  e.  (
( V ClWWalksN  E ) `  ( N  -  2
) )  <->  ( (
( w substr  <. 0 ,  ( N  -  2 ) >. )  e. Word  V  /\  A. i  e.  ( 0..^ ( ( # `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  -  1 ) ) { ( ( w substr  <. 0 ,  ( N  -  2 )
>. ) `  i ) ,  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  ( i  +  1 ) ) }  e.