Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  extwwlkfablem2 Structured version   Unicode version

Theorem extwwlkfablem2 30811
Description: Lemma 2 for extwwlkfab 30823. (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 23407 . . . . . . . . . . 11  |-  ( V USGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
2 uzuzle23 30333 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( ZZ>= `  2 )
)
3 eluzge2nn0 30332 . . . . . . . . . . . 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 967 . . . . . . . . . 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 30572 . . . . . . . . 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 1007 . . . . . . 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 30571 . . . . . . . . . 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 1009 . . . . . . 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 12419 . . . . . . . . . . . 12  |-  ( w  e. Word  V  ->  (
w substr  <. 0 ,  ( N  -  2 )
>. )  e. Word  V )
17163ad2ant1 1009 . . . . . . . . . . 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 6199 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( (
# `  w )  -  1 )  =  ( N  -  1 ) )
2120adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  =  ( N  - 
1 ) )
22 1le3 10641 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  <_  3
23 1re 9488 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  e.  RR
2423a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  RR )
25 3re 10498 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  3  e.  RR
2625a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  RR )
27 eluzelre 10974 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  RR )
2824, 26, 27lesub2d 10050 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1  <_  3  <->  ( N  -  3 )  <_ 
( N  -  1 ) ) )
2922, 28mpbii 211 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  1 ) )
30 eluzelz 10973 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ZZ )
31 eluzel2 10969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  ZZ )
3230, 31zsubcld 10855 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  e.  ZZ )
33 peano2zm 10791 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
3430, 33syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ZZ )
35 eluz 10977 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  1
)  e.  ZZ )  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  1 ) ) )
3632, 34, 35syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  1 ) ) )
3729, 36mpbird 232 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
3837adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  1 )  e.  ( ZZ>= `  ( N  -  3
) ) )
3921, 38eqeltrd 2539 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
40 fzoss2 11680 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( # `  w
)  -  1 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( ( # `  w )  -  1 ) ) )
41 ssralv 3516 . . . . . . . . . . . . . . . . . 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
) )
4239, 40, 413syl 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 ) )
4342adantl 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 ) )
44 simpll 753 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  w  e. Word  V
)
45 1eluzge0 11002 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  ( ZZ>= `  0 )
46 fzss1 11600 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
4745, 46mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
48 ige3m2fz 30347 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... N
) )
4947, 48sseldd 3457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 0 ... N
) )
5049adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... N ) )
51 oveq2 6200 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
# `  w )  =  N  ->  ( 0 ... ( # `  w
) )  =  ( 0 ... N ) )
5251eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 0 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5352adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  e.  ( 0 ... ( # `  w ) )  <->  ( N  -  2 )  e.  ( 0 ... N
) ) )
5450, 53mpbird 232 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 0 ... ( # `  w
) ) )
5554ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( N  - 
2 )  e.  ( 0 ... ( # `  w ) ) )
56 2re 10494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  e.  RR
57 2lt3 10592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  2  <  3
5856, 25, 57ltleii 9600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  <_  3
5956a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  RR )
6059, 26, 27lesub2d 10050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  <_  3  <->  ( N  -  3 )  <_ 
( N  -  2 ) ) )
6158, 60mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  3 )  <_ 
( N  -  2 ) )
62 2z 10781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  2  e.  ZZ
6362a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  ZZ )
6430, 63zsubcld 10855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ZZ )
65 eluz 10977 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  -  3 )  e.  ZZ  /\  ( N  -  2
)  e.  ZZ )  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <-> 
( N  -  3 )  <_  ( N  -  2 ) ) )
6632, 64, 65syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  <->  ( N  - 
3 )  <_  ( N  -  2 ) ) )
6761, 66mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) ) )
68 fzoss2 11680 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  -  2 )  e.  ( ZZ>= `  ( N  -  3 ) )  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
6967, 68syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 0..^ ( N  -  3 ) )  C_  (
0..^ ( N  - 
2 ) ) )
7069sseld 3455 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7170ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) ) )
7271imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  i  e.  ( 0..^ ( N  - 
2 ) ) )
73 swrd0fv 12439 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 0 ... ( # `  w
) )  /\  i  e.  ( 0..^ ( N  -  2 ) ) )  ->  ( (
w substr  <. 0 ,  ( N  -  2 )
>. ) `  i )  =  ( w `  i ) )
7444, 55, 72, 73syl3anc 1219 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( ( w substr  <. 0 ,  ( N  -  2 ) >.
) `  i )  =  ( w `  i ) )
7574eqcomd 2459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( w `  i )  =  ( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  i ) )
76 elfzonn0 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  i  e.  NN0 )
7776adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  i  e.  NN0 )
78 peano2nn0 10723 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  NN0  ->  ( i  +  1 )  e. 
NN0 )
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e. 
NN0 )
80 uz3m2nn 30335 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  NN )
8180adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( N  -  2 )  e.  NN )
82 elfzo0 11690 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  <->  ( i  e. 
NN0  /\  ( N  -  3 )  e.  NN  /\  i  < 
( N  -  3 ) ) )
83 nn0cn 10692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( i  e.  NN0  ->  i  e.  CC )
84 ax-1cn 9443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  1  e.  CC
8583, 84jctir 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( i  e.  NN0  ->  ( i  e.  CC  /\  1  e.  CC ) )
8685adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  e.  CC  /\  1  e.  CC ) )
87 pncan 9719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  CC  /\  1  e.  CC )  ->  ( ( i  +  1 )  -  1 )  =  i )
8886, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  =  i )
8988eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
i  =  ( ( i  +  1 )  -  1 ) )
90 eluzelcn 10975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  CC )
9190adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  N  e.  CC )
92 2cnd 10497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
2  e.  CC )
9384a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  CC )
9491, 92, 93subsub4d 9853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( N  - 
2 )  -  1 )  =  ( N  -  ( 2  +  1 ) ) )
95 df-3 10484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  3  =  ( 2  +  1 )
9695oveq2i 6203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  -  3 )  =  ( N  -  (
2  +  1 ) )
9794, 96syl6reqr 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  3 )  =  ( ( N  -  2 )  -  1 ) )
9889, 97breq12d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  <-> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
9998biimpd 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( i  e.  NN0  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  <  ( N  -  3 )  ->  ( ( i  +  1 )  - 
1 )  <  (
( N  -  2 )  -  1 ) ) )
10099impancom 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
1011003adant2 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) ) )
102101imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( ( i  +  1 )  -  1 )  <  ( ( N  -  2 )  -  1 ) )
103 nn0re 10691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  NN0  ->  i  e.  RR )
104 peano2re 9645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  e.  RR  ->  (
i  +  1 )  e.  RR )
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  e.  NN0  ->  ( i  +  1 )  e.  RR )
1061053ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( i  +  1 )  e.  RR )
107106adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  e.  RR )
10827, 59resubcld 9879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  RR )
109108adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  RR )
11023a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
1  e.  RR )
111107, 109, 110ltsub1d 10051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
112102, 111mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( i  e.  NN0  /\  ( N  -  3 )  e.  NN  /\  i  <  ( N  - 
3 ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( i  +  1 )  <  ( N  -  2 ) )
113112ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( i  e.  NN0  /\  ( N  -  3
)  e.  NN  /\  i  <  ( N  - 
3 ) )  -> 
( N  e.  (
ZZ>= `  3 )  -> 
( i  +  1 )  <  ( N  -  2 ) ) )
11482, 113sylbi 195 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( i  +  1 )  <  ( N  -  2 ) ) )
115114impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  < 
( N  -  2 ) )
116 elfzo0 11690 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) )  <->  ( ( i  +  1 )  e. 
NN0  /\  ( N  -  2 )  e.  NN  /\  ( i  +  1 )  < 
( N  -  2 ) ) )
11779, 81, 115, 116syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  ( ZZ>= ` 
3 )  /\  i  e.  ( 0..^ ( N  -  3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  -  2 ) ) )
118117ex 434 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
119118ad2antll 728 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  ->  ( i  e.  ( 0..^ ( N  -  3 ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) ) )
120119imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( w  e. Word  V  /\  ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) ) )  /\  i  e.  ( 0..^ ( N  - 
3 ) ) )  ->  ( i  +  1 )  e.  ( 0..^ ( N  - 
2 ) ) )
121 swrd0fv 12439 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
12244, 55, 120, 121syl3anc 1219 . . . . . . . . . . . . . . . . . . . 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 ) ) )
123122eqcomd 2459 . . . . . . . . . . . . . . . . . . 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 ) ) )
12475, 123preq12d 4062 . . . . . . . . . . . . . . . . . 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 ) ) } )
125124eleq1d 2520 . . . . . . . . . . . . . . . . 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
) )
126125ralbidva 2836 . . . . . . . . . . . . . . . 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 ) )
12743, 126sylibd 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 ) )
128127impancom 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
) )
1291283adant3 1008 . . . . . . . . . . . . 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
) )
130129expdimp 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 ) )
131130impcom 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
)
132131adantr 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 )
133 simprl1 1033 . . . . . . . . . . . . . . . . 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 )
134 simprr 756 . . . . . . . . . . . . . . . . 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 )
1352adantr 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 )
)
136133, 134, 1353jca 1168 . . . . . . . . . . . . . . . 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 ) ) )
137136adantr 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 ) ) )
138 extwwlkfablem2lem 30808 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  V  /\  ( # `  w )  =  N  /\  N  e.  ( ZZ>= `  2 )
)  ->  ( # `  (
w substr  <. 0 ,  ( N  -  2 )
>. ) )  =  ( N  -  2 ) )
139137, 138syl 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 ) )
140139oveq1d 6207 . . . . . . . . . . . . 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 ) )
141140oveq2d 6208 . . . . . . . . . . . 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 ) ) )
142 2cnd 10497 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  2  e.  CC )
14384a1i 11 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  1  e.  CC )
14490, 142, 143subsub4d 9853 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  (
2  +  1 ) ) )
145 2p1e3 10548 . . . . . . . . . . . . . . . . 17  |-  ( 2  +  1 )  =  3
146145a1i 11 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 2  +  1 )  =  3 )
147146oveq2d 6208 . . . . . . . . . . . . . . 15  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 2  +  1 ) )  =  ( N  -  3 ) )
148144, 147eqtrd 2492 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
149148ad2antrr 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 ) )
150149oveq2d 6208 . . . . . . . . . . . 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 ) ) )
151141, 150eqtrd 2492 . . . . . . . . . . 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 ) ) )
152151raleqdv 3021 . . . . . . . . . 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 ) )
153132, 152mpbird 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
)
15420oveq2d 6208 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  w )  =  N  ->  ( 0..^ ( ( # `  w
)  -  1 ) )  =  ( 0..^ ( N  -  1 ) ) )
155154raleqdv 3021 . . . . . . . . . . . . . . . . . . 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 ) )
156 simplr 754 . . . . . . . . . . . . . . . . . . . . . . 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 )
157 oveq2 6200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
# `  w )  =  N  ->  ( 1 ... ( # `  w
) )  =  ( 1 ... N ) )
158157eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
# `  w )  =  N  ->  ( ( N  -  2 )  e.  ( 1 ... ( # `  w
) )  <->  ( N  -  2 )  e.  ( 1 ... N
) ) )
15948, 158syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
160159ad2antrr 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
) ) ) )
161160com12 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
) ) ) )
162161adantr 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 ) ) ) )
163162impcom 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
) ) )
164 swrd0fvlsw 12443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( lastS  `  ( w substr  <. 0 ,  ( N  - 
2 ) >. )
)  =  ( w `
 ( ( N  -  2 )  - 
1 ) ) )
165156, 163, 164syl2anc 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 ) ) )
16648adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... N ) )
167157adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( 1 ... ( # `
 w ) )  =  ( 1 ... N ) )
168166, 167eleqtrrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( N  -  2 )  e.  ( 1 ... ( # `  w
) ) )
169168ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
# `  w )  =  N  ->  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e.  ( 1 ... ( # `
 w ) ) ) )
170169ad2antrr 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
) ) ) )
171170com12 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
) ) ) )
172171adantr 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 ) ) ) )
173172impcom 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
) ) )
174 swrd0fv0 12440 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  e. Word  V  /\  ( N  -  2
)  e.  ( 1 ... ( # `  w
) ) )  -> 
( ( w substr  <. 0 ,  ( N  - 
2 ) >. ) `  0 )  =  ( w `  0
) )
175156, 173, 174syl2anc 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 ) )
176165, 175preq12d 4062 . . . . . . . . . . . . . . . . . . . . 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 ) } )
177 cnm2m1cnm3 30319 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  CC  ->  (
( N  -  2 )  -  1 )  =  ( N  - 
3 ) )
17890, 177syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  2 )  -  1 )  =  ( N  -  3 ) )
179178fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
2 )  -  1 ) )  =  ( w `  ( N  -  3 ) ) )
180179ad2antrl 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
) ) )
181 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( w `  0 )  =  ( w `  ( N  -  2
) )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
182181eqcoms 2463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( w `  ( N  -  2 ) )  =  ( w ` 
0 )  ->  (
w `  0 )  =  ( w `  ( N  -  2
) ) )
183182ad2antll 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
) ) )
184180, 183preq12d 4062 . . . . . . . . . . . . . . . . . . . . . 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 ) ) } )
185 eluzfz2b 11563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  <->  N  e.  (
3 ... N ) )
186 fzval3 11708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ZZ  ->  (
3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
18730, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3 ... N )  =  ( 3..^ ( N  +  1 ) ) )
188187eleq2d 2521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  <->  N  e.  (
3..^ ( N  + 
1 ) ) ) )
189 peano2z 10789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
190 zadd2cl 30328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  2 )  e.  ZZ )
191 1le2 10638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  1  <_  2
19223a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  1  e.  RR )
19356a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  2  e.  RR )
194 zre 10753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( N  e.  ZZ  ->  N  e.  RR )
195192, 193, 194leadd2d 10037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( N  e.  ZZ  ->  (
1  <_  2  <->  ( N  +  1 )  <_ 
( N  +  2 ) ) )
196191, 195mpbii 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( N  e.  ZZ  ->  ( N  +  1 )  <_  ( N  + 
2 ) )
197189, 190, 1963jca 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( N  e.  ZZ  ->  (
( N  +  1 )  e.  ZZ  /\  ( N  +  2
)  e.  ZZ  /\  ( N  +  1
)  <_  ( N  +  2 ) ) )
19830, 197syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_  ( N  + 
2 ) ) )
199 eluz2 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  <->  ( ( N  +  1 )  e.  ZZ  /\  ( N  +  2 )  e.  ZZ  /\  ( N  +  1 )  <_ 
( N  +  2 ) ) )
200198, 199sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) ) )
201 fzoss2 11680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( N  +  2 )  e.  ( ZZ>= `  ( N  +  1 ) )  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
202200, 201syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( N  +  1 ) )  C_  (
3..^ ( N  + 
2 ) ) )
203202sseld 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( N  +  1 ) )  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
204188, 203sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3 ... N
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) ) )
205185, 204syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( ZZ>= `  3 )  ->  N  e.  ( 3..^ ( N  +  2 ) ) ) )
206205pm2.43i 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( N  + 
2 ) ) )
207 3cn 10499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  3  e.  CC
208207a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  3
)  ->  3  e.  CC )
209208, 90, 143addsub12d 9845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  ( 3  -  1 ) ) )
210 3m1e2 10541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( 3  -  1 )  =  2
211210oveq2i 6203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  +  ( 3  -  1 ) )  =  ( N  +  2 )
212209, 211syl6eq 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  +  ( N  - 
1 ) )  =  ( N  +  2 ) )
213212oveq2d 6208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3..^ ( 3  +  ( N  -  1 ) ) )  =  ( 3..^ ( N  + 
2 ) ) )
214206, 213eleqtrrd 2542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) ) )
215214, 34jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  e.  ( 3..^ ( 3  +  ( N  - 
1 ) ) )  /\  ( N  - 
1 )  e.  ZZ ) )
216 fzosubel3 11704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  ( 3..^ ( 3  +  ( N  -  1 ) ) )  /\  ( N  -  1 )  e.  ZZ )  -> 
( N  -  3 )  e.  ( 0..^ ( N  -  1 ) ) )
217 fveq2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  i )  =  ( w `  ( N  -  3
) ) )
218 oveq1 6199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  ( N  - 
3 )  ->  (
i  +  1 )  =  ( ( N  -  3 )  +  1 ) )
219218fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( N  - 
3 )  ->  (
w `  ( i  +  1 ) )  =  ( w `  ( ( N  - 
3 )  +  1 ) ) )
220217, 219preq12d 4062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  =  ( N  - 
3 )  ->  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( ( N  -  3 )  +  1 ) ) } )
221220eleq1d 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  =  ( N  - 
3 )  ->  ( { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  E  <->  { ( w `  ( N  -  3 ) ) ,  ( w `
 ( ( N  -  3 )  +  1 ) ) }  e.  ran  E ) )
222221rspcv 3167 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
223215, 216, 2223syl 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 ) )
22490, 208, 143subsubd 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( ( N  - 
3 )  +  1 ) )
225210a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( 3  -  1 )  =  2 )
226225oveq2d 6208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  ( 3  -  1 ) )  =  ( N  -  2 ) )
227224, 226eqtr3d 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( ( N  -  3 )  +  1 )  =  ( N  -  2 ) )
228227fveq2d 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w `  ( ( N  - 
3 )  +  1 ) )  =  ( w `  ( N  -  2 ) ) )
229228preq2d 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  ( ZZ>= `  3
)  ->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( ( N  - 
3 )  +  1 ) ) }  =  { ( w `  ( N  -  3
) ) ,  ( w `  ( N  -  2 ) ) } )
230229eleq1d 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( {
( w `  ( N  -  3 ) ) ,  ( w `
 ( ( N  -  3 )  +  1 ) ) }  e.  ran  E  <->  { (
w `  ( N  -  3 ) ) ,  ( w `  ( N  -  2
) ) }  e.  ran  E ) )
231223, 230sylibd 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 ) )
232231adantr 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
) )
233232com12 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
) )
234233ad2antlr 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 ) )
235234imp 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 )
236184, 235eqeltrd 2539 . . . . . . . . . . . . . . . . . . . . 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 )
237176, 236eqeltrd 2539 . . . . . . . . . . . . . . . . . . . 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
)
238237exp41 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 ) ) ) )
239155, 238sylbid 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
) ) ) )
240239com13 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 ) ) ) )
241240imp 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 ) ) )
2422413adant3 1008 . . . . . . . . . . . . . . 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
) ) )
243242imp 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
) )
244243expd 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 ) ) )
245244impcom 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
) )
246245com12 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
) )
247246adantl 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
) )
248247impcom 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 )
24919, 153, 2483jca 1168 . . . . . . . 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
) )
250249exp31 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
) ) ) )
2512503ad2ant3 1011 . . . . . 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
) ) ) )
25215, 251sylbid 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 ) ) ) )
253252imp31 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 ) )
254 clwwlknprop 30575 . . . . . . . . . 10  |-  ( w  e.  ( ( V ClWWalksN  E ) `  N
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) ) )
255 simpl2 992 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  ->  w  e. Word  V )
256 simpl3r 1044 . . . . . . . . . . . 12  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  w  e. Word  V  /\  ( N  e.  NN0  /\  ( # `
 w )  =  N ) )  /\  N  e.  ( ZZ>= ` 
3 ) )  -> 
( # `  w )  =  N )
2572adantl 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 ) )
258255, 256, 2573jca 1168 . . . . . . . . . . 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 ) ) )
259258ex 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 ) ) ) )
260254, 259syl 16 . . . . . . . . 9  |-  ( w  e.  ( ( V ClWWalksN  E ) `  N
)  ->  ( N  e.  ( ZZ>= `  3 )  ->  ( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
261260com12 31 . . . . . . . 8  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( w  e.  ( ( V ClWWalksN  E ) `
 N )  -> 
( w  e. Word  V  /\  ( # `  w
)  =  N  /\  N  e.  ( ZZ>= ` 
2 ) ) ) )
2622613ad2ant3 1011 . . . . . . 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 ) ) ) )
263262imp 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 )
) )
264263adantr 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 )
) )
265264, 138syl 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 ) )
266253, 265jca 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 ) ) )
267 uznn0sub 10995 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  2
)  ->  ( N  -  2 )  e. 
NN0 )
2682, 267syl 16 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  3
)  ->  ( N  -  2 )  e. 
NN0 )
2691, 268anim12i 566 . . . . . . . 8  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
270 df-3an 967 . . . . . . . 8  |-  ( ( V  e.  _V  /\  E  e.  _V  /\  ( N  -  2 )  e.  NN0 )  <->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( N  -  2 )  e.  NN0 ) )
271269, 270sylibr 212 . . . . . . 7  |-  ( ( V USGrph  E  /\  N  e.  ( ZZ>= `  3 )
)  ->  ( V  e.  _V  /\  E  e. 
_V  /\  ( N  -  2 )  e. 
NN0 ) )
272 isclwwlkn 30572 . . . . . . 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 ) ) ) )
273271, 272syl 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 ) ) ) )
274 isclwwlk 30571 . . . . . . . . 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
) ) )
2751, 274syl 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
) ) )
276275adantr 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
) ) )
277276anbi1d 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 ) ) ) )
278273, 277bitrd 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 ) ) ) )
2792783adant2 1007 . . . 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  -