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

Theorem extwwlkfablem2 25885
Description: Lemma 2 for extwwlkfab 25897. (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 25144 . . . . . . . . . . 11  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
2 uzuzle23 11223 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
3 eluzge2nn0 11222 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  2
)  ->  N  e.  NN0 )
42, 3syl 17 . . . . . . . . . . 11  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  NN0 )
51, 4anim12i 576 . . . . . . . . . 10  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  N  e.  NN0 ) )
6 df-3an 1009 . . . . . . . . . 10  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  N  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  N  e.  NN0 ) )
75, 6sylibr 217 . . . . . . . . 9  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( V  e.  _V  /\  E  e. 
_V  /\  N  e.  NN0 ) )
8 isclwwlkn 25576 . . . . . . . . 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 17 . . . . . . . 8  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  <->  ( w  e.  ( V ClWWalks  E )  /\  ( # `  w
)  =  N ) ) )
1093adant2 1049 . . . . . . 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 25575 . . . . . . . . . 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 719 . . . . . . . . 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 17 . . . . . . . 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 1051 . . . . . . 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 261 . . . . . 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 12829 . . . . . . . . . . . 12  |-  ( w  e. Word  V  ->  (
w substr  <. 0 ,  ( N  -  2 )
>. )  e. Word  V )
17163ad2ant1 1051 . . . . . . . . . . 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 472 . . . . . . . . . 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 741 . . . . . . . . 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 6315 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( (
# `  w )  -  1 )  =  ( N  -  1 ) )
2120adantr 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  =  ( N  - 
1 ) )
22 1le3 10849 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  <_  3
23 1red 9676 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  RR )
24 3re 10705 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  3  e.  RR
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  RR )
26 eluzelre 11193 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  RR )
2723, 25, 26lesub2d 10242 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  <_  3  <->  ( N  -  3 )  <_ 
( N  -  1 ) ) )
2822, 27mpbii 216 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  1 ) )
29 eluzelz 11192 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
30 eluzel2 11187 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  ZZ )
3129, 30zsubcld 11068 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  e.  ZZ )
32 peano2zm 11004 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
3329, 32syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
34 eluz 11196 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  1
)  e.  ZZ )  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  1 ) ) )
3531, 33, 34syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  1 ) ) )
3628, 35mpbird 240 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
3736adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  1 )  e.  ( ZZ>= `  ( N  -  3
) ) )
3821, 37eqeltrd 2549 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
39 fzoss2 11973 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( ( # `  w )  -  1 ) ) )
40 ssralv 3479 . . . . . . . . . . . . . . . . . 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 18 . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  w  e. Word  V
)
44 1eluzge0 11226 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  ( ZZ>= `  0 )
45 fzss1 11863 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
47 ige3m2fz 11849 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... N
) )
4846, 47sseldd 3419 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 0 ... N
) )
4948adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... N ) )
50 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  w )  =  N  ->  ( 0 ... ( # `  w
) )  =  ( 0 ... N ) )
5150eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 0 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5251adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  e.  ( 0 ... ( # `  w ) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5349, 52mpbird 240 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... ( # `  w
) ) )
5453ad2antlr 741 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( N  - 
2 )  e.  ( 0 ... ( # `  w ) ) )
55 2re 10701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  RR
56 2lt3 10800 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  <  3
5755, 24, 56ltleii 9775 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  <_  3
5855a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  RR )
5958, 25, 26lesub2d 10242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  <_  3  <->  ( N  -  3 )  <_ 
( N  -  2 ) ) )
6057, 59mpbii 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  2 ) )
61 2z 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  2  e.  ZZ
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  ZZ )
6329, 62zsubcld 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ZZ )
64 eluz 11196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  2
)  e.  ZZ )  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  2 ) ) )
6531, 63, 64syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  2 ) ) )
6660, 65mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
67 fzoss2 11973 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
6866, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
6968sseld 3417 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7069ad2antll 743 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7170imp 436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) )
72 swrd0fv 12849 . . . . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . . . . 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 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  NN0 )
7675adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  i  e.  NN0 )
77 peano2nn0 10934 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e. 
NN0 )
79 uz3m2nn 11225 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  NN )
8079adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( N  -  2 )  e.  NN )
81 elfzo0 11984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  <->  ( i  e. 
NN0  /\  ( N  -  3 )  e.  NN  /\  i  < 
( N  -  3 ) ) )
82 nn0cn 10903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( i  e.  NN0  ->  i  e.  CC )
83 ax-1cn 9615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  1  e.  CC
8482, 83jctir 547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( i  e.  NN0  ->  ( i  e.  CC  /\  1  e.  CC ) )
8584adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  e.  CC  /\  1  e.  CC ) )
86 pncan 9901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  CC  /\  1  e.  CC )  ->  ( ( i  +  1 )  -  1 )  =  i )
8785, 86syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  =  i )
8887eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
i  =  ( ( i  +  1 )  -  1 ) )
89 eluzelcn 11194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  CC )
9089adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  CC )
91 2cnd 10704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
2  e.  CC )
92 1cnd 9677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  CC )
9390, 91, 92subsub4d 10036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  -  1 )  =  ( N  -  ( 2  +  1 ) ) )
94 df-3 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  3  =  ( 2  +  1 )
9594oveq2i 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  -  3 )  =  ( N  -  (
2  +  1 ) )
9693, 95syl6reqr 2524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  3 )  =  ( ( N  -  2 )  -  1 ) )
9788, 96breq12d 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  <-> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
9897biimpd 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  ->  ( ( i  +  1 )  - 
1 )  <  (
( N  -  2 )  -  1 ) ) )
9998impancom 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
100993adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
101100imp 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) )
102 nn0re 10902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  NN0  ->  i  e.  RR )
103 peano2re 9824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  RR  ->  (
i  +  1 )  e.  RR )
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  NN0  ->  ( i  +  1 )  e.  RR )
1051043ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( i  +  1 )  e.  RR )
106105adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  e.  RR )
10726, 58resubcld 10068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  RR )
108107adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  RR )
109 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  RR )
110106, 108, 109ltsub1d 10243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  <  ( N  -  2 ) )
112111ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( i  +  1 )  <  ( N  -  2 ) ) )
11381, 112sylbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( i  +  1 )  <  ( N  -  2 ) ) )
114113impcom 437 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  < 
( N  -  2 ) )
115 elfzo0 11984 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) )  <->  ( ( i  +  1 )  e. 
NN0  /\  ( N  -  2 )  e.  NN  /\  ( i  +  1 )  < 
( N  -  2 ) ) )
11678, 80, 114, 115syl3anbrc 1214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) ) )
117116ex 441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
118117ad2antll 743 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
119118imp 436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) )
120 swrd0fv 12849 . . . . . . . . . . . . . . . . . . . . 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 1292 . . . . . . . . . . . . . . . . . . . 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 2477 . . . . . . . . . . . . . . . . . . 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 4050 . . . . . . . . . . . . . . . . . 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 2533 . . . . . . . . . . . . . . . . 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 2828 . . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . 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 1050 . . . . . . . . . . . . 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 444 . . . . . . . . . . . 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 437 . . . . . . . . . . 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 472 . . . . . . . . . 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 1075 . . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . 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 1210 . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . 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 25882 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  ( ZZ>= `  2 )
)  ->  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) )
138136, 137syl 17 . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . 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 6324 . . . . . . . . . . . 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 10704 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  CC )
142 1cnd 9677 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  CC )
14389, 141, 142subsub4d 10036 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  (
2  +  1 ) ) )
144 2p1e3 10756 . . . . . . . . . . . . . . . . 17  |-  ( 2  +  1 )  =  3
145144a1i 11 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  +  1 )  =  3 )
146145oveq2d 6324 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  =  ( N  -  3 ) )
147143, 146eqtrd 2505 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
148147ad2antrr 740 . . . . . . . . . . . . 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 6324 . . . . . . . . . . . 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 2505 . . . . . . . . . . 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 2979 . . . . . . . . . 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 240 . . . . . . . . 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 6324 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( 0..^ ( ( # `  w
)  -  1 ) )  =  ( 0..^ ( N  -  1 ) ) )
154153raleqdv 2979 . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . . . . . 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 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  w )  =  N  ->  ( 1 ... ( # `  w
) )  =  ( 1 ... N ) )
157156eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 1 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 1 ... N
) ) )
15847, 157syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
159158ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . . . . 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 437 . . . . . . . . . . . . . . . . . . . . . . 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 12853 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( w `
 ( ( N  -  2 )  - 
1 ) ) )
164155, 162, 163syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... N ) )
166156adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( 1 ... ( # `
 w ) )  =  ( 1 ... N ) )
167165, 166eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... ( # `  w
) ) )
168167ex 441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
169168ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . . . . 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 437 . . . . . . . . . . . . . . . . . . . . . . 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 12850 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 )  =  ( w `  0
) )
174155, 172, 173syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 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 4050 . . . . . . . . . . . . . . . . . . . . 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 10888 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  CC  ->  (
( N  -  2 )  -  1 )  =  ( N  - 
3 ) )
17789, 176syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
178177fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
2 )  -  1 ) )  =  ( w `  ( N  -  3 ) ) )
179178ad2antrl 742 . . . . . . . . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( w `  ( N  -  2 ) )  =  ( w ` 
0 )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
182181ad2antll 743 . . . . . . . . . . . . . . . . . . . . . . 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 4050 . . . . . . . . . . . . . . . . . . . . . 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 11834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  <->  N  e.  (
3 ... N ) )
185 fzval3 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ZZ  ->  (
3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
18629, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
187186eleq2d 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  <->  N  e.  (
3..^ ( N  + 
1 ) ) ) )
188 peano2z 11002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
189 zadd2cl 11071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  2 )  e.  ZZ )
190 1le2 10846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  1  <_  2
191 1red 9676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  1  e.  RR )
19255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  2  e.  RR )
193 zre 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  N  e.  RR )
194191, 192, 193leadd2d 10229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( N  e.  ZZ  ->  (
1  <_  2  <->  ( N  +  1 )  <_ 
( N  +  2 ) ) )
195190, 194mpbii 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  <_  ( N  + 
2 ) )
196188, 189, 1953jca 1210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ZZ  ->  (
( N  +  1 )  e.  ZZ  /\  ( N  +  2
)  e.  ZZ  /\  ( N  +  1
)  <_  ( N  +  2 ) ) )
19729, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_  ( N  + 
2 ) ) )
198 eluz2 11188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  <->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_ 
( N  +  2 ) ) )
199197, 198sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) ) )
200 fzoss2 11973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
201199, 200syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
202201sseld 3417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( N  +  1 ) )  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
203187, 202sylbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
204184, 203syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( ZZ>= `  3 )  ->  N  e.  ( 3..^ ( N  +  2 ) ) ) )
205204pm2.43i 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) )
206 3cn 10706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  3  e.  CC
207206a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  CC )
208207, 89, 142addsub12d 10028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  ( 3  -  1 ) ) )
209 3m1e2 10748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 3  -  1 )  =  2
210209oveq2i 6319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  +  ( 3  -  1 ) )  =  ( N  +  2 )
211208, 210syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  2 ) )
212211oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( 3  +  ( N  -  1 ) ) )  =  ( 3..^ ( N  + 
2 ) ) )
213205, 212eleqtrrd 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) ) )
214213, 33jca 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( 3  +  ( N  - 
1 ) ) )  /\  ( N  - 
1 )  e.  ZZ ) )
215 fzosubel3 12004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) )  /\  ( N  -  1 )  e.  ZZ )  -> 
( N  -  3 )  e.  ( 0..^ ( N  -  1 ) ) )
216 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  i )  =  ( w `  ( N  -  3
) ) )
217 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  ( N  - 
3 )  ->  (
i  +  1 )  =  ( ( N  -  3 )  +  1 ) )
218217fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  ( i  +  1 ) )  =  ( w `  ( ( N  - 
3 )  +  1 ) ) )
219216, 218preq12d 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  ( N  - 
3 )  ->  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( ( N  -  3 )  +  1 ) ) } )
220219eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  =  ( N  - 
3 )  ->  ( { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( w `  ( N  -  3 ) ) ,  ( w `
 ( ( N  -  3 )  +  1 ) ) }  e.  ran  E ) )
221220rspcv 3132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10033 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( ( N  - 
3 )  +  1 ) )
224209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  -  1 )  =  2 )
225224oveq2d 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( N  -  2 ) )
226223, 225eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  3 )  +  1 )  =  ( N  -  2 ) )
227226fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
3 )  +  1 ) )  =  ( w `  ( N  -  2 ) ) )
228227preq2d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( ( N  - 
3 )  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) } )
229228eleq1d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . . . . . . . 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 741 . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . . . . . . . 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 621 . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . 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 82 . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . 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 1050 . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . 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 443 . . . . . . . . . . . . 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 437 . . . . . . . . . . . 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 473 . . . . . . . . . 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 437 . . . . . . . . 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 1210 . . . . . . . 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 615 . . . . . . 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 1053 . . . . . 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 223 . . . . 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 439 . . . 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 25579 . . . . . . . . . 10  |-  ( w  e.  ( ( V ClWWalksN  E ) `  N
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) ) )
254 simpl2 1034 . . . . . . . . . . . 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 1086 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( # `  w )  =  N )
2562adantl 473 . . . . . . . . . . . 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 1210 . . . . . . . . . . 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 441 . . . . . . . . . 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 17 . . . . . . . . 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 1053 . . . . . . 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 436 . . . . . 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 472 . . . . 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 17 . . . 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 541 . . 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 11214 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  2 )  e. 
NN0 )
2672, 266syl 17 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e. 
NN0 )
2681, 267anim12i 576 . . . . . . . 8  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
269 df-3an 1009 . . . . . . . 8  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  -  2 )  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
270268, 269sylibr 217 . . . . . . 7  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( V  e.  _V  /\  E  e. 
_V  /\  ( N  -  2 )  e. 
NN0 ) )
271 isclwwlkn 25576 . . . . . . 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 17 . . . . . 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 25575 . . . . . . . . 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 17 . . . . . . . 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 472 . . . . . . 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 719 . . . . . 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 261 . . . . 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 1049 . . . 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 ) )