Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eupath2lem3 Unicode version

Theorem eupath2lem3 23918
Description: Lemma for eupath2 23919. (Contributed by Mario Carneiro, 8-Apr-2015.)
Hypotheses
Ref Expression
eupath2.1  |-  ( ph  ->  E  Fn  A )
eupath2.3  |-  ( ph  ->  F ( V EulPaths  E ) P )
eupath2.5  |-  ( ph  ->  N  e.  NN0 )
eupath2.6  |-  ( ph  ->  ( N  +  1 )  <_  ( # `  F
) )
eupath2.7  |-  ( ph  ->  U  e.  V )
eupath2.8  |-  ( ph  ->  { x  e.  V  |  -.  2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
) }  =  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) )
Assertion
Ref Expression
eupath2lem3  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... ( N  +  1 ) ) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
Distinct variable groups:    x, E    x, F    x, N    x, V    x, U
Allowed substitution hints:    ph( x)    A( x)    P( x)

Proof of Theorem eupath2lem3
StepHypRef Expression
1 imaundi 5109 . . . . . . . . . . 11  |-  ( F
" ( ( 1 ... N )  u. 
{ ( N  + 
1 ) } ) )  =  ( ( F " ( 1 ... N ) )  u.  ( F " { ( N  + 
1 ) } ) )
2 1z 10069 . . . . . . . . . . . . 13  |-  1  e.  ZZ
3 eupath2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN0 )
4 nn0uz 10278 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
5 1m1e0 9830 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
65fveq2i 5544 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
74, 6eqtr4i 2319 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
83, 7syl6eleq 2386 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )
9 fzsuc2 10858 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
102, 8, 9sylancr 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
1110imaeq2d 5028 . . . . . . . . . . 11  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( F "
( ( 1 ... N )  u.  {
( N  +  1 ) } ) ) )
12 eupath2.3 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F ( V EulPaths  E ) P )
13 eupath2.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  Fn  A )
14 eupaf1o 23900 . . . . . . . . . . . . . . 15  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
1512, 13, 14syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
16 f1ofn 5489 . . . . . . . . . . . . . 14  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F  Fn  ( 1 ... ( # `
 F ) ) )
1715, 16syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  ( 1 ... ( # `  F
) ) )
18 eupath2.6 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  +  1 )  <_  ( # `  F
) )
19 nn0p1nn 10019 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
203, 19syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
21 nnuz 10279 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2386 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
23 eupacl 23899 . . . . . . . . . . . . . . . . 17  |-  ( F ( V EulPaths  E ) P  ->  ( # `  F
)  e.  NN0 )
2412, 23syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  F
)  e.  NN0 )
2524nn0zd 10131 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  F
)  e.  ZZ )
26 elfz5 10806 . . . . . . . . . . . . . . 15  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2722, 25, 26syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2818, 27mpbird 223 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )
29 fnsnfv 5598 . . . . . . . . . . . . 13  |-  ( ( F  Fn  ( 1 ... ( # `  F
) )  /\  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3017, 28, 29syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3130uneq2d 3342 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } )  =  ( ( F "
( 1 ... N
) )  u.  ( F " { ( N  +  1 ) } ) ) )
321, 11, 313eqtr4a 2354 . . . . . . . . . 10  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( ( F
" ( 1 ... N ) )  u. 
{ ( F `  ( N  +  1
) ) } ) )
3332reseq2d 4971 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) ) )
34 resundi 4985 . . . . . . . . 9  |-  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )
3533, 34syl6eq 2344 . . . . . . . 8  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) ) )
36 f1of 5488 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) ) --> A )
3715, 36syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) --> A )
38 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( F : ( 1 ... ( # `  F
) ) --> A  /\  ( N  +  1
)  e.  ( 1 ... ( # `  F
) ) )  -> 
( F `  ( N  +  1 ) )  e.  A )
3937, 28, 38syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( N  +  1 ) )  e.  A )
40 fnressn 5721 . . . . . . . . . . 11  |-  ( ( E  Fn  A  /\  ( F `  ( N  +  1 ) )  e.  A )  -> 
( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
4113, 39, 40syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
42 eupaseg 23903 . . . . . . . . . . . . . 14  |-  ( ( F ( V EulPaths  E ) P  /\  ( N  +  1 )  e.  ( 1 ... ( # `
 F ) ) )  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  {
( P `  (
( N  +  1 )  -  1 ) ) ,  ( P `
 ( N  + 
1 ) ) } )
4312, 28, 42syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  ( ( N  +  1 )  -  1 ) ) ,  ( P `  ( N  +  1
) ) } )
443nn0cnd 10036 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  CC )
45 ax-1cn 8811 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
46 pncan 9073 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
4744, 45, 46sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
4847fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P `  (
( N  +  1 )  -  1 ) )  =  ( P `
 N ) )
4948preq1d 3725 . . . . . . . . . . . . 13  |-  ( ph  ->  { ( P `  ( ( N  + 
1 )  -  1 ) ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5043, 49eqtrd 2328 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5150opeq2d 3819 . . . . . . . . . . 11  |-  ( ph  -> 
<. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >.  =  <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. )
5251sneqd 3666 . . . . . . . . . 10  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  ( E `  ( F `
 ( N  + 
1 ) ) )
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )
5341, 52eqtrd 2328 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } )
5453uneq2d 3342 . . . . . . . 8  |-  ( ph  ->  ( ( E  |`  ( F " ( 1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )  =  ( ( E  |`  ( F " ( 1 ... N
) ) )  u. 
{ <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) )
5535, 54eqtrd 2328 . . . . . . 7  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) )
5655oveq2d 5890 . . . . . 6  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... ( N  + 
1 ) ) ) ) )  =  ( V VDeg  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) ) )
5756fveq1d 5543 . . . . 5  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... ( N  +  1 ) ) ) ) ) `
 U )  =  ( ( V VDeg  (
( E  |`  ( F " ( 1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) ) `  U ) )
58 imassrn 5041 . . . . . . . 8  |-  ( F
" ( 1 ... N ) )  C_  ran  F
59 f1ofo 5495 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-onto-> A )
60 forn 5470 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -onto-> A  ->  ran  F  =  A )
6115, 59, 603syl 18 . . . . . . . 8  |-  ( ph  ->  ran  F  =  A )
6258, 61syl5sseq 3239 . . . . . . 7  |-  ( ph  ->  ( F " (
1 ... N ) ) 
C_  A )
63 fnssres 5373 . . . . . . 7  |-  ( ( E  Fn  A  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
6413, 62, 63syl2anc 642 . . . . . 6  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
65 fvex 5555 . . . . . . . 8  |-  ( F `
 ( N  + 
1 ) )  e. 
_V
66 prex 4233 . . . . . . . 8  |-  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  e.  _V
6765, 66fnsn 5320 . . . . . . 7  |-  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. }  Fn  { ( F `  ( N  +  1 ) ) }
6867a1i 10 . . . . . 6  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  Fn  { ( F `  ( N  +  1 ) ) } )
69 eupafi 23901 . . . . . . . 8  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  A  e.  Fin )
7012, 13, 69syl2anc 642 . . . . . . 7  |-  ( ph  ->  A  e.  Fin )
71 ssfi 7099 . . . . . . 7  |-  ( ( A  e.  Fin  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( F " (
1 ... N ) )  e.  Fin )
7270, 62, 71syl2anc 642 . . . . . 6  |-  ( ph  ->  ( F " (
1 ... N ) )  e.  Fin )
73 snfi 6957 . . . . . . 7  |-  { ( F `  ( N  +  1 ) ) }  e.  Fin
7473a1i 10 . . . . . 6  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  e.  Fin )
753nn0red 10035 . . . . . . . . . 10  |-  ( ph  ->  N  e.  RR )
7675ltp1d 9703 . . . . . . . . 9  |-  ( ph  ->  N  <  ( N  +  1 ) )
77 peano2re 9001 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
7875, 77syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  RR )
7975, 78ltnled 8982 . . . . . . . . 9  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
8076, 79mpbid 201 . . . . . . . 8  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
81 f1of1 5487 . . . . . . . . . . 11  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-1-1-> A )
8215, 81syl 15 . . . . . . . . . 10  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-> A )
833nn0zd 10131 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
8483peano2zd 10136 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
85 eluz2 10252 . . . . . . . . . . . . 13  |-  ( (
# `  F )  e.  ( ZZ>= `  ( N  +  1 ) )  <-> 
( ( N  + 
1 )  e.  ZZ  /\  ( # `  F
)  e.  ZZ  /\  ( N  +  1
)  <_  ( # `  F
) ) )
8684, 25, 18, 85syl3anbrc 1136 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  ( N  +  1
) ) )
87 peano2uzr 10290 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  ( # `  F )  e.  ( ZZ>= `  ( N  +  1 ) ) )  ->  ( # `
 F )  e.  ( ZZ>= `  N )
)
8883, 86, 87syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  N ) )
89 fzss2 10847 . . . . . . . . . . 11  |-  ( (
# `  F )  e.  ( ZZ>= `  N )  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
9088, 89syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
91 f1elima 5803 . . . . . . . . . 10  |-  ( ( F : ( 1 ... ( # `  F
) ) -1-1-> A  /\  ( N  +  1
)  e.  ( 1 ... ( # `  F
) )  /\  (
1 ... N )  C_  ( 1 ... ( # `
 F ) ) )  ->  ( ( F `  ( N  +  1 ) )  e.  ( F "
( 1 ... N
) )  <->  ( N  +  1 )  e.  ( 1 ... N
) ) )
9282, 28, 90, 91syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  e.  ( 1 ... N ) ) )
93 elfz5 10806 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... N )  <->  ( N  +  1 )  <_  N ) )
9422, 83, 93syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... N )  <-> 
( N  +  1 )  <_  N )
)
9592, 94bitrd 244 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  <_  N )
)
9680, 95mtbird 292 . . . . . . 7  |-  ( ph  ->  -.  ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) ) )
97 disjsn 3706 . . . . . . 7  |-  ( ( ( F " (
1 ... N ) )  i^i  { ( F `
 ( N  + 
1 ) ) } )  =  (/)  <->  -.  ( F `  ( N  +  1 ) )  e.  ( F "
( 1 ... N
) ) )
9896, 97sylibr 203 . . . . . 6  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  i^i  {
( F `  ( N  +  1 ) ) } )  =  (/) )
99 eupagra 23897 . . . . . . 7  |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
100 umgrares 23891 . . . . . . 7  |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  ( F " (
1 ... N ) ) ) )
10112, 99, 1003syl 18 . . . . . 6  |-  ( ph  ->  V UMGrph  ( E  |`  ( F " ( 1 ... N ) ) ) )
102 relumgra 23881 . . . . . . . . 9  |-  Rel UMGrph
103102brrelexi 4745 . . . . . . . 8  |-  ( V UMGrph  E  ->  V  e.  _V )
10412, 99, 1033syl 18 . . . . . . 7  |-  ( ph  ->  V  e.  _V )
105 eupapf 23902 . . . . . . . . 9  |-  ( F ( V EulPaths  E ) P  ->  P : ( 0 ... ( # `  F ) ) --> V )
10612, 105syl 15 . . . . . . . 8  |-  ( ph  ->  P : ( 0 ... ( # `  F
) ) --> V )
1073, 4syl6eleq 2386 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
108 elfzuzb 10808 . . . . . . . . 9  |-  ( N  e.  ( 0 ... ( # `  F
) )  <->  ( N  e.  ( ZZ>= `  0 )  /\  ( # `  F
)  e.  ( ZZ>= `  N ) ) )
109107, 88, 108sylanbrc 645 . . . . . . . 8  |-  ( ph  ->  N  e.  ( 0 ... ( # `  F
) ) )
110 ffvelrn 5679 . . . . . . . 8  |-  ( ( P : ( 0 ... ( # `  F
) ) --> V  /\  N  e.  ( 0 ... ( # `  F
) ) )  -> 
( P `  N
)  e.  V )
111106, 109, 110syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( P `  N
)  e.  V )
112 peano2nn0 10020 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
1133, 112syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
114113, 4syl6eleq 2386 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
115 elfz5 10806 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
0 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 0 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
116114, 25, 115syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 0 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
11718, 116mpbird 223 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  ( 0 ... ( # `  F
) ) )
118 ffvelrn 5679 . . . . . . . 8  |-  ( ( P : ( 0 ... ( # `  F
) ) --> V  /\  ( N  +  1
)  e.  ( 0 ... ( # `  F
) ) )  -> 
( P `  ( N  +  1 ) )  e.  V )
119106, 117, 118syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( P `  ( N  +  1 ) )  e.  V )
120 umgra1 23893 . . . . . . 7  |-  ( ( ( V  e.  _V  /\  ( F `  ( N  +  1 ) )  e.  A )  /\  ( ( P `
 N )  e.  V  /\  ( P `
 ( N  + 
1 ) )  e.  V ) )  ->  V UMGrph  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } )
121104, 39, 111, 119, 120syl22anc 1183 . . . . . 6  |-  ( ph  ->  V UMGrph  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } )
122 eupath2.7 . . . . . 6  |-  ( ph  ->  U  e.  V )
12364, 68, 72, 74, 98, 101, 121, 122vdgrun 23908 . . . . 5  |-  ( ph  ->  ( ( V VDeg  (
( E  |`  ( F " ( 1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) ) `  U )  =  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) ) )
12457, 123eqtrd 2328 . . . 4  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... ( N  +  1 ) ) ) ) ) `
 U )  =  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) ) )
125124breq2d 4051 . . 3  |-  ( ph  ->  ( 2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... ( N  + 
1 ) ) ) ) ) `  U
)  <->  2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) ) ) )
126125notbid 285 . 2  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... ( N  +  1 ) ) ) ) ) `
 U )  <->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) ) ) )
127 fveq2 5541 . . . . . . . . . 10  |-  ( x  =  U  ->  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
)  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )
128127breq2d 4051 . . . . . . . . 9  |-  ( x  =  U  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x )  <->  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) ) )
129128notbid 285 . . . . . . . 8  |-  ( x  =  U  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
)  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
130129elrab3 2937 . . . . . . 7  |-  ( U  e.  V  ->  ( U  e.  { x  e.  V  |  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x ) }  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
131122, 130syl 15 . . . . . 6  |-  ( ph  ->  ( U  e.  {
x  e.  V  |  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
) }  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
132 eupath2.8 . . . . . . 7  |-  ( ph  ->  { x  e.  V  |  -.  2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
) }  =  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) )
133132eleq2d 2363 . . . . . 6  |-  ( ph  ->  ( U  e.  {
x  e.  V  |  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
) }  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
134131, 133bitr3d 246 . . . . 5  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
135134adantr 451 . . . 4  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  <-> 
U  e.  if ( ( P `  0
)  =  ( P `
 N ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  N
) } ) ) )
136 2z 10070 . . . . . . . 8  |-  2  e.  ZZ
137136a1i 10 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  e.  ZZ )
138 vdgrf 23906 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  ( E  |`  ( F
" ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) )  /\  ( F " ( 1 ... N ) )  e. 
Fin )  ->  ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
139104, 64, 72, 138syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) : V --> NN0 )
140 ffvelrn 5679 . . . . . . . . . 10  |-  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) : V --> NN0  /\  U  e.  V
)  ->  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  NN0 )
141139, 122, 140syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e. 
NN0 )
142141nn0zd 10131 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ )
143142adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  ZZ )
144 vdgrf 23906 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  {
<. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. }  Fn  { ( F `
 ( N  + 
1 ) ) }  /\  { ( F `
 ( N  + 
1 ) ) }  e.  Fin )  -> 
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0 )
145104, 68, 74, 144syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0 )
146 ffvelrn 5679 . . . . . . . . . 10  |-  ( ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0  /\  U  e.  V )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
147145, 122, 146syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
148147nn0zd 10131 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  ZZ )
149148adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  e.  ZZ )
150 iddvds 12558 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  2 )
151136, 150ax-mp 8 . . . . . . . . 9  |-  2  ||  2
152 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  U )
153 simplr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
154153, 152eqtr3d 2330 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
155152, 154preq12d 3727 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U ,  U } )
156 dfsn2 3667 . . . . . . . . . . . . . . 15  |-  { U }  =  { U ,  U }
157155, 156syl6eqr 2346 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U } )
158157opeq2d 3819 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { U } >. )
159158sneqd 3666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } )
160159oveq2d 5890 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )  =  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) )
161160fveq1d 5543 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  { U } >. } ) `  U ) )
162104ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  V  e.  _V )
16365a1i 10 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
164122ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
165162, 163, 164vdgr1d 23909 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) `  U )  =  2 )
166161, 165eqtrd 2328 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  2 )
167151, 166syl5breqr 4075 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
168 dvds0 12560 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  0 )
169136, 168ax-mp 8 . . . . . . . . 9  |-  2  ||  0
170104ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  V  e.  _V )
17165a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
172122ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  U  e.  V )
173111ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  e.  V )
174 simpr 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =/=  U )
175119ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  e.  V )
176 simplr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
177176, 174eqnetrrd 2479 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  =/=  U )
178170, 171, 172, 173, 174, 175, 177vdgr1a 23912 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  0 )
179169, 178syl5breqr 4075 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
180167, 179pm2.61dane 2537 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
181 dvdsadd2b 12587 . . . . . . 7  |-  ( ( 2  e.  ZZ  /\  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ  /\  ( ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  e.  ZZ  /\  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) ) )  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  <->  2  ||  ( ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  +  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) ) )
182137, 143, 149, 180, 181syl112anc 1186 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( 2 
||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  <->  2  ||  ( ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  +  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) ) )
183147nn0cnd 10036 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  CC )
184141nn0cnd 10036 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  CC )
185183, 184addcomd 9030 . . . . . . . 8  |-  ( ph  ->  ( ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  +  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )  =  ( ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) ) )
186185breq2d 4051 . . . . . . 7  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  +  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) )  <->  2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) ) ) )
187186adantr 451 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( 2 
||  ( ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  +  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )  <->  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) ) ) )
188182, 187bitrd 244 . . . . 5  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( 2 
||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  <->  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) ) ) )
189188notbid 285 . . . 4  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  <->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) ) ) )
190 simpr 447 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( P `  N )  =  ( P `  ( N  +  1 ) ) )
191190eqeq2d 2307 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( P `  0 )  =  ( P `  N )  <->  ( P `  0 )  =  ( P `  ( N  +  1 ) ) ) )
192190preq2d 3726 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  { ( P `  0 ) ,  ( P `  N ) }  =  { ( P ` 
0 ) ,  ( P `  ( N  +  1 ) ) } )
193191, 192ifbieq2d 3598 . . . . 5  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  if (
( P `  0
)  =  ( P `
 N ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  N
) } )  =  if ( ( P `
 0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  {
( P `  0
) ,  ( P `
 ( N  + 
1 ) ) } ) )
194193eleq2d 2363 . . . 4  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
195135, 189, 1943bitr3d 274 . . 3  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  <-> 
U  e.  if ( ( P `  0
)  =  ( P `
 ( N  + 
1 ) ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  ( N  +  1 ) ) } ) ) )
196 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =  U )
197196preq1d 3725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  =  { U ,  ( P `
 ( N  + 
1 ) ) } )
198197opeq2d 3819 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >.  =  <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. )
199198sneqd 3666 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. }  =  { <. ( F `  ( N  +  1
) ) ,  { U ,  ( P `  ( N  +  1 ) ) } >. } )
200199oveq2d 5890 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } )  =  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) )
201200fveq1d 5543 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
202104ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  V  e.  _V )
20365a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( F `  ( N  +  1 ) )  e.  _V )
204122ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
205119ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  e.  V )
206 simplr 731 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )
207196, 206eqnetrrd 2479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
208207necomd 2542 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  =/=  U )
209202, 203, 204, 205, 208vdgr1b 23910 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
210201, 209eqtrd 2328 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
211210oveq2d 5890 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )  =  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) )
212211breq2d 4051 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
2  ||  ( (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  <->  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
213212notbid 285 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  <->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
214 2nn 9893 . . . . . . . . . . . 12  |-  2  e.  NN
215214a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  NN )
216 1lt2 9902 . . . . . . . . . . . 12  |-  1  <  2
217216a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  1  <  2 )
218 ndvdsp1 12624 . . . . . . . . . . 11  |-  ( ( ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ  /\  2  e.  NN  /\  1  <  2 )  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  ->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
219142, 215, 217, 218syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( 2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  ->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
220219con2d 107 . . . . . . . . 9  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  ->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) ) )
221 2prm 12790 . . . . . . . . . . . . 13  |-  2  e.  Prime
222 nprmdvds1 12806 . . . . . . . . . . . . 13  |-  ( 2  e.  Prime  ->  -.  2  ||  1 )
223221, 222ax-mp 8 . . . . . . . . . . . 12  |-  -.  2  ||  1
224 opoe 12880 . . . . . . . . . . . 12  |-  ( ( ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  ZZ  /\  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) )  /\  ( 1  e.  ZZ  /\  -.  2  ||  1 ) )  ->  2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 ) )
2252, 223, 224mpanr12 666 . . . . . . . . . . 11  |-  ( ( ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ  /\  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )  ->  2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 ) )
226225ex 423 . . . . . . . . . 10  |-  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  e.  ZZ  ->  ( -.  2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  ->  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
227142, 226syl 15 . . . . . . . . 9  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  -> 
2  ||  ( (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
228220, 227impbid 183 . . . . . . . 8  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
229228, 134bitrd 244 . . . . . . 7  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
230229notbid 285 . . . . . 6  |-  ( ph  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 )  <->  -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } ) ) )
231230ad2antrr 706 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 )  <->  -.  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
232 fvex 5555 . . . . . . 7  |-  ( P `
 N )  e. 
_V
233232eupath2lem2 23917 . . . . . 6  |-  ( ( ( P `  N
)  =/=  ( P `
 ( N  + 
1 ) )  /\  ( P `  N )  =  U )  -> 
( -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
234233adantll 694 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( -.  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } )  <-> 
U  e.  if ( ( P `  0
)  =  ( P `
 ( N  + 
1 ) ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  ( N  +  1 ) ) } ) ) )
235213, 231, 2343bitrd 270 . . . 4  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  <-> 
U  e.  if ( ( P `  0
)  =  ( P `
 ( N  + 
1 ) ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  ( N  +  1 ) ) } ) ) )
236 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
237236preq2d 3726 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  U } )
238237opeq2d 3819 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. )
239238sneqd 3666 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  U } >. } )
240239oveq2d 5890 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )  =  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) )
241240fveq1d 5543 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  U } >. } ) `  U
) )
242104ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  V  e.  _V )
24365a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
244122ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  U  e.  V )
245111ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  e.  V )
246 simplr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  ( P `
 ( N  + 
1 ) ) )
247246, 236neeqtrd 2481 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  U )
248242, 243, 244, 245, 247vdgr1c 23911 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) `  U )  =  1 )
249241, 248eqtrd 2328 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  1 )
250249oveq2d 5890 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  =  ( ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 ) )
251250breq2d 4051 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )  <->  2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 ) ) )
252251notbid 285 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  <->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
253230ad2antrr 706 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 )  <->  -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } ) ) )
254 necom 2540 . . . . . . . 8  |-  ( ( P `  N )  =/=  ( P `  ( N  +  1
) )  <->  ( P `  ( N  +  1 ) )  =/=  ( P `  N )
)
255 fvex 5555 . . . . . . . . 9  |-  ( P `
 ( N  + 
1 ) )  e. 
_V
256255eupath2lem2 23917 . . . . . . . 8  |-  ( ( ( P `  ( N  +  1 ) )  =/=  ( P `
 N )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  U  e.  if ( ( P `
 0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  {
( P `  0
) ,  ( P `
 ( N  + 
1 ) ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
257254, 256sylanb 458 . . . . . . 7  |-  ( ( ( P `  N
)  =/=  ( P `
 ( N  + 
1 ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  U  e.  if ( ( P `
 0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  {
( P `  0
) ,  ( P `
 ( N  + 
1 ) ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
258257con1bid 320 . . . . . 6  |-  ( ( ( P `  N
)  =/=  ( P `
 ( N  + 
1 ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
259258adantll 694 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
260252, 253, 2593bitrd 270 . . . 4  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
261104ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  V  e.  _V )
26265a1i 10 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( F `  ( N  +  1
) )  e.  _V )
263122ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  e.  V
)
264111ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  e.  V
)
265 simprl 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  =/=  U
)
266119ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  e.  V
)
267 simprr 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  =/=  U
)
268261, 262, 263, 264, 265, 266, 267vdgr1a 23912 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  =  0 )
269268oveq2d 5890 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  =  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  0 ) )
270184addid1d 9028 . . . . . . . . 9  |-  ( ph  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  0 )  =  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )
271270ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  0 )  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) )
272269, 271eqtrd 2328 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U ) )  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) )
273272breq2d 4051 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( 2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  <->  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
274273notbid 285 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
275134ad2antrr 706 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
276265necomd 2542 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  N )
)
277267necomd 2542 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
278276, 2772thd 231 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =/=  ( P `  N
)  <->  U  =/=  ( P `  ( N  +  1 ) ) ) )
279 neeq1 2467 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  N )  <->  ( P `  0 )  =/=  ( P `  N
) ) )
280 neeq1 2467 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  ( N  +  1
) )  <->  ( P `  0 )  =/=  ( P `  ( N  +  1 ) ) ) )
281279, 280bibi12d 312 . . . . . . . . 9  |-  ( U  =  ( P ` 
0 )  ->  (
( U  =/=  ( P `  N )  <->  U  =/=  ( P `  ( N  +  1
) ) )  <->  ( ( P `  0 )  =/=  ( P `  N
)  <->  ( P ` 
0 )  =/=  ( P `  ( N  +  1 ) ) ) ) )
282278, 281syl5ibcom 211 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  ->  ( ( P `  0 )  =/=  ( P `  N
)  <->  ( P ` 
0 )  =/=  ( P `  ( N  +  1 ) ) ) ) )
283282pm5.32rd 621 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( P `  0 )  =/=  ( P `  N )  /\  U  =  ( P ` 
0 ) )  <->  ( ( P `  0 )  =/=  ( P `  ( N  +  1 ) )  /\  U  =  ( P `  0
) ) ) )
284276neneqd 2475 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  N ) )
285 biorf 394 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 N )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  N )  \/  U  =  ( P `  0 ) ) ) )
286284, 285syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  N
)  \/  U  =  ( P `  0
) ) ) )
287 orcom 376 . . . . . . . . 9  |-  ( ( U  =  ( P `
 N )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  N ) ) )
288286, 287syl6bb 252 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  N
) ) ) )
289288anbi2d 684 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( P `  0 )  =/=  ( P `  N )  /\  U  =  ( P ` 
0 ) )  <->  ( ( P `  0 )  =/=  ( P `  N
)  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  N ) ) ) ) )
290277neneqd 2475 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  ( N  +  1 ) ) )
291 biorf 394 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 ( N  + 
1 ) )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0 ) ) ) )
292290, 291syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0
) ) ) )
293 orcom 376 . . . . . . . . 9  |-  ( ( U  =  ( P `
 ( N  + 
1 ) )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  ( N  +  1 ) ) ) )
294292, 293syl6bb 252 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  ( N  +  1 ) ) ) ) )
295294anbi2d 684 . . . . . . 7  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( P `  0 )  =/=  ( P `  ( N  +  1
) )  /\  U  =  ( P ` 
0 ) )  <->  ( ( P `  0 )  =/=  ( P `  ( N  +  1 ) )  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  ( N  +  1
) ) ) ) ) )
296283, 289, 2953bitr3d 274 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( ( ( P `  0 )  =/=  ( P `  N )  /\  ( U  =  ( P `  0 )  \/  U  =  ( P `
 N ) ) )  <->  ( ( P `
 0 )  =/=  ( P `  ( N  +  1 ) )  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  ( N  +  1
) ) ) ) ) )
297 eupath2lem1 23916 . . . . . . 7  |-  ( U  e.  V  ->  ( U  e.  if (
( P `  0
)  =  ( P `
 N ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  N
) } )  <->  ( ( P `  0 )  =/=  ( P `  N
)  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  N ) ) ) ) )
298263, 297syl 15 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  ( ( P `
 0 )  =/=  ( P `  N
)  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  N ) ) ) ) )
299 eupath2lem1 23916 . . . . . . 7  |-  ( U  e.  V  ->  ( U  e.  if (
( P `  0
)  =  ( P `
 ( N  + 
1 ) ) ,  (/) ,  { ( P `
 0 ) ,  ( P `  ( N  +  1 ) ) } )  <->  ( ( P `  0 )  =/=  ( P `  ( N  +  1 ) )  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  ( N  +  1
) ) ) ) ) )
300263, 299syl 15 . . . . . 6  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  e.  if ( ( P `
 0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  {
( P `  0
) ,  ( P `
 ( N  + 
1 ) ) } )  <->  ( ( P `
 0 )  =/=  ( P `  ( N  +  1 ) )  /\  ( U  =  ( P ` 
0 )  \/  U  =  ( P `  ( N  +  1
) ) ) ) ) )
301296, 298, 3003bitr4d 276 . . . . 5  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
302274, 275, 3013bitrd 270 . . . 4  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
303235, 260, 302pm2.61da2ne 2538 . . 3  |-  ( (
ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
)  +  ( (