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

Theorem eupath2lem3 21701
Description: Lemma for eupath2 21702. (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 5284 . . . . . . . . . . 11  |-  ( F
" ( ( 1 ... N )  u. 
{ ( N  + 
1 ) } ) )  =  ( ( F " ( 1 ... N ) )  u.  ( F " { ( N  + 
1 ) } ) )
2 1z 10311 . . . . . . . . . . . . 13  |-  1  e.  ZZ
3 eupath2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN0 )
4 nn0uz 10520 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
5 1m1e0 10068 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
65fveq2i 5731 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
74, 6eqtr4i 2459 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
83, 7syl6eleq 2526 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )
9 fzsuc2 11104 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
102, 8, 9sylancr 645 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
1110imaeq2d 5203 . . . . . . . . . . 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 21692 . . . . . . . . . . . . . . 15  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
1512, 13, 14syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
16 f1ofn 5675 . . . . . . . . . . . . . 14  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F  Fn  ( 1 ... ( # `
 F ) ) )
1715, 16syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  ( 1 ... ( # `  F
) ) )
18 eupath2.6 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  +  1 )  <_  ( # `  F
) )
19 nn0p1nn 10259 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
203, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
21 nnuz 10521 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2526 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
23 eupacl 21691 . . . . . . . . . . . . . . . . 17  |-  ( F ( V EulPaths  E ) P  ->  ( # `  F
)  e.  NN0 )
2412, 23syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  F
)  e.  NN0 )
2524nn0zd 10373 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  F
)  e.  ZZ )
26 elfz5 11051 . . . . . . . . . . . . . . 15  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2722, 25, 26syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2818, 27mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )
29 fnsnfv 5786 . . . . . . . . . . . . 13  |-  ( ( F  Fn  ( 1 ... ( # `  F
) )  /\  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3017, 28, 29syl2anc 643 . . . . . . . . . . . 12  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3130uneq2d 3501 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } )  =  ( ( F "
( 1 ... N
) )  u.  ( F " { ( N  +  1 ) } ) ) )
321, 11, 313eqtr4a 2494 . . . . . . . . . 10  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( ( F
" ( 1 ... N ) )  u. 
{ ( F `  ( N  +  1
) ) } ) )
3332reseq2d 5146 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) ) )
34 resundi 5160 . . . . . . . . 9  |-  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )
3533, 34syl6eq 2484 . . . . . . . 8  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) ) )
36 f1of 5674 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) ) --> A )
3715, 36syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) --> A )
3837, 28ffvelrnd 5871 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( N  +  1 ) )  e.  A )
39 fnressn 5918 . . . . . . . . . . 11  |-  ( ( E  Fn  A  /\  ( F `  ( N  +  1 ) )  e.  A )  -> 
( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
4013, 38, 39syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
41 eupaseg 21695 . . . . . . . . . . . . . 14  |-  ( ( F ( V EulPaths  E ) P  /\  ( N  +  1 )  e.  ( 1 ... ( # `
 F ) ) )  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  {
( P `  (
( N  +  1 )  -  1 ) ) ,  ( P `
 ( N  + 
1 ) ) } )
4212, 28, 41syl2anc 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  ( ( N  +  1 )  -  1 ) ) ,  ( P `  ( N  +  1
) ) } )
433nn0cnd 10276 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  CC )
44 ax-1cn 9048 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
45 pncan 9311 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
4643, 44, 45sylancl 644 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
4746fveq2d 5732 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P `  (
( N  +  1 )  -  1 ) )  =  ( P `
 N ) )
4847preq1d 3889 . . . . . . . . . . . . 13  |-  ( ph  ->  { ( P `  ( ( N  + 
1 )  -  1 ) ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
4942, 48eqtrd 2468 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5049opeq2d 3991 . . . . . . . . . . 11  |-  ( ph  -> 
<. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >.  =  <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. )
5150sneqd 3827 . . . . . . . . . 10  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  ( E `  ( F `
 ( N  + 
1 ) ) )
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )
5240, 51eqtrd 2468 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } )
5352uneq2d 3501 . . . . . . . 8  |-  ( ph  ->  ( ( E  |`  ( F " ( 1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )  =  ( ( E  |`  ( F " ( 1 ... N
) ) )  u. 
{ <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) )
5435, 53eqtrd 2468 . . . . . . 7  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) )
5554oveq2d 6097 . . . . . 6  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... ( N  + 
1 ) ) ) ) )  =  ( V VDeg  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) ) )
5655fveq1d 5730 . . . . 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 ) )
57 imassrn 5216 . . . . . . . 8  |-  ( F
" ( 1 ... N ) )  C_  ran  F
58 f1ofo 5681 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-onto-> A )
59 forn 5656 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -onto-> A  ->  ran  F  =  A )
6015, 58, 593syl 19 . . . . . . . 8  |-  ( ph  ->  ran  F  =  A )
6157, 60syl5sseq 3396 . . . . . . 7  |-  ( ph  ->  ( F " (
1 ... N ) ) 
C_  A )
62 fnssres 5558 . . . . . . 7  |-  ( ( E  Fn  A  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
6313, 61, 62syl2anc 643 . . . . . 6  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
64 fvex 5742 . . . . . . . 8  |-  ( F `
 ( N  + 
1 ) )  e. 
_V
65 prex 4406 . . . . . . . 8  |-  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  e.  _V
6664, 65fnsn 5504 . . . . . . 7  |-  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. }  Fn  { ( F `  ( N  +  1 ) ) }
6766a1i 11 . . . . . 6  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  Fn  { ( F `  ( N  +  1 ) ) } )
68 eupafi 21693 . . . . . . . 8  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  A  e.  Fin )
6912, 13, 68syl2anc 643 . . . . . . 7  |-  ( ph  ->  A  e.  Fin )
70 ssfi 7329 . . . . . . 7  |-  ( ( A  e.  Fin  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( F " (
1 ... N ) )  e.  Fin )
7169, 61, 70syl2anc 643 . . . . . 6  |-  ( ph  ->  ( F " (
1 ... N ) )  e.  Fin )
72 snfi 7187 . . . . . . 7  |-  { ( F `  ( N  +  1 ) ) }  e.  Fin
7372a1i 11 . . . . . 6  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  e.  Fin )
743nn0red 10275 . . . . . . . . . 10  |-  ( ph  ->  N  e.  RR )
7574ltp1d 9941 . . . . . . . . 9  |-  ( ph  ->  N  <  ( N  +  1 ) )
76 peano2re 9239 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
7774, 76syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  RR )
7874, 77ltnled 9220 . . . . . . . . 9  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
7975, 78mpbid 202 . . . . . . . 8  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
80 f1of1 5673 . . . . . . . . . . 11  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-1-1-> A )
8115, 80syl 16 . . . . . . . . . 10  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-> A )
823nn0zd 10373 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
8382peano2zd 10378 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
84 eluz2 10494 . . . . . . . . . . . . 13  |-  ( (
# `  F )  e.  ( ZZ>= `  ( N  +  1 ) )  <-> 
( ( N  + 
1 )  e.  ZZ  /\  ( # `  F
)  e.  ZZ  /\  ( N  +  1
)  <_  ( # `  F
) ) )
8583, 25, 18, 84syl3anbrc 1138 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  ( N  +  1
) ) )
86 peano2uzr 10532 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  ( # `  F )  e.  ( ZZ>= `  ( N  +  1 ) ) )  ->  ( # `
 F )  e.  ( ZZ>= `  N )
)
8782, 85, 86syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  N ) )
88 fzss2 11092 . . . . . . . . . . 11  |-  ( (
# `  F )  e.  ( ZZ>= `  N )  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
8987, 88syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
90 f1elima 6009 . . . . . . . . . 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
) ) )
9181, 28, 89, 90syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  e.  ( 1 ... N ) ) )
92 elfz5 11051 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... N )  <->  ( N  +  1 )  <_  N ) )
9322, 82, 92syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... N )  <-> 
( N  +  1 )  <_  N )
)
9491, 93bitrd 245 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  <_  N )
)
9579, 94mtbird 293 . . . . . . 7  |-  ( ph  ->  -.  ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) ) )
96 disjsn 3868 . . . . . . 7  |-  ( ( ( F " (
1 ... N ) )  i^i  { ( F `
 ( N  + 
1 ) ) } )  =  (/)  <->  -.  ( F `  ( N  +  1 ) )  e.  ( F "
( 1 ... N
) ) )
9795, 96sylibr 204 . . . . . 6  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  i^i  {
( F `  ( N  +  1 ) ) } )  =  (/) )
98 eupagra 21688 . . . . . . 7  |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
99 umgrares 21359 . . . . . . 7  |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  ( F " (
1 ... N ) ) ) )
10012, 98, 993syl 19 . . . . . 6  |-  ( ph  ->  V UMGrph  ( E  |`  ( F " ( 1 ... N ) ) ) )
101 relumgra 21349 . . . . . . . . 9  |-  Rel UMGrph
102101brrelexi 4918 . . . . . . . 8  |-  ( V UMGrph  E  ->  V  e.  _V )
10312, 98, 1023syl 19 . . . . . . 7  |-  ( ph  ->  V  e.  _V )
104 eupapf 21694 . . . . . . . . 9  |-  ( F ( V EulPaths  E ) P  ->  P : ( 0 ... ( # `  F ) ) --> V )
10512, 104syl 16 . . . . . . . 8  |-  ( ph  ->  P : ( 0 ... ( # `  F
) ) --> V )
1063, 4syl6eleq 2526 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
107 elfzuzb 11053 . . . . . . . . 9  |-  ( N  e.  ( 0 ... ( # `  F
) )  <->  ( N  e.  ( ZZ>= `  0 )  /\  ( # `  F
)  e.  ( ZZ>= `  N ) ) )
108106, 87, 107sylanbrc 646 . . . . . . . 8  |-  ( ph  ->  N  e.  ( 0 ... ( # `  F
) ) )
109105, 108ffvelrnd 5871 . . . . . . 7  |-  ( ph  ->  ( P `  N
)  e.  V )
110 peano2nn0 10260 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
1113, 110syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
112111, 4syl6eleq 2526 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
113 elfz5 11051 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
0 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 0 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
114112, 25, 113syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 0 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
11518, 114mpbird 224 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  ( 0 ... ( # `  F
) ) )
116105, 115ffvelrnd 5871 . . . . . . 7  |-  ( ph  ->  ( P `  ( N  +  1 ) )  e.  V )
117 umgra1 21361 . . . . . . 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 ) ) }
>. } )
118103, 38, 109, 116, 117syl22anc 1185 . . . . . 6  |-  ( ph  ->  V UMGrph  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } )
119 eupath2.7 . . . . . 6  |-  ( ph  ->  U  e.  V )
12063, 67, 71, 73, 97, 100, 118, 119vdgrfiun 21673 . . . . 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 ) ) )
12156, 120eqtrd 2468 . . . 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
) ) )
122121breq2d 4224 . . 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 ) ) ) )
123122notbid 286 . 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
) ) ) )
124 fveq2 5728 . . . . . . . . . 10  |-  ( x  =  U  ->  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
)  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )
125124breq2d 4224 . . . . . . . . 9  |-  ( x  =  U  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x )  <->  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) ) )
126125notbid 286 . . . . . . . 8  |-  ( x  =  U  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
)  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
127126elrab3 3093 . . . . . . 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 ) ) )
128119, 127syl 16 . . . . . 6  |-  ( ph  ->  ( U  e.  {
x  e.  V  |  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
) }  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
129 eupath2.8 . . . . . . 7  |-  ( ph  ->  { x  e.  V  |  -.  2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
) }  =  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) )
130129eleq2d 2503 . . . . . 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 ) } ) ) )
131128, 130bitr3d 247 . . . . 5  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
132131adantr 452 . . . 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
) } ) ) )
133 2z 10312 . . . . . . . 8  |-  2  e.  ZZ
134133a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  e.  ZZ )
135 vdgrfif 21670 . . . . . . . . . . 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 )
136103, 63, 71, 135syl3anc 1184 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) : V --> NN0 )
137136, 119ffvelrnd 5871 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e. 
NN0 )
138137nn0zd 10373 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ )
139138adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  ZZ )
140 vdgrfif 21670 . . . . . . . . . . 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 )
141103, 67, 73, 140syl3anc 1184 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0 )
142141, 119ffvelrnd 5871 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
143142nn0zd 10373 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  ZZ )
144143adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  e.  ZZ )
145 iddvds 12863 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  2 )
146133, 145ax-mp 8 . . . . . . . . 9  |-  2  ||  2
147 simpr 448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  U )
148 simplr 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
149148, 147eqtr3d 2470 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
150147, 149preq12d 3891 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U ,  U } )
151 dfsn2 3828 . . . . . . . . . . . . . . 15  |-  { U }  =  { U ,  U }
152150, 151syl6eqr 2486 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U } )
153152opeq2d 3991 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { U } >. )
154153sneqd 3827 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } )
155154oveq2d 6097 . . . . . . . . . . 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 } >. } ) )
156155fveq1d 5730 . . . . . . . . . 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 ) )
157103ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  V  e.  _V )
15864a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
159119ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
160157, 158, 159vdgr1d 21674 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) `  U )  =  2 )
161156, 160eqtrd 2468 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  2 )
162146, 161syl5breqr 4248 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
163 dvds0 12865 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  0 )
164133, 163ax-mp 8 . . . . . . . . 9  |-  2  ||  0
165103ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  V  e.  _V )
16664a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
167119ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  U  e.  V )
168109ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  e.  V )
169 simpr 448 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =/=  U )
170116ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  e.  V )
171 simplr 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
172171, 169eqnetrrd 2621 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  =/=  U )
173165, 166, 167, 168, 169, 170, 172vdgr1a 21677 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  0 )
174164, 173syl5breqr 4248 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
175162, 174pm2.61dane 2682 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
176 dvdsadd2b 12892 . . . . . . 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 ) ) ) )
177134, 139, 144, 175, 176syl112anc 1188 . . . . . 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 ) ) ) )
178142nn0cnd 10276 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  CC )
179137nn0cnd 10276 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  CC )
180178, 179addcomd 9268 . . . . . . . 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 ) ) )
181180breq2d 4224 . . . . . . 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 ) ) ) )
182181adantr 452 . . . . . 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 ) ) ) )
183177, 182bitrd 245 . . . . 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 ) ) ) )
184183notbid 286 . . . 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 ) ) ) )
185 simpr 448 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( P `  N )  =  ( P `  ( N  +  1 ) ) )
186185eqeq2d 2447 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( P `  0 )  =  ( P `  N )  <->  ( P `  0 )  =  ( P `  ( N  +  1 ) ) ) )
187185preq2d 3890 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  { ( P `  0 ) ,  ( P `  N ) }  =  { ( P ` 
0 ) ,  ( P `  ( N  +  1 ) ) } )
188186, 187ifbieq2d 3759 . . . . 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 ) ) } ) )
189188eleq2d 2503 . . . 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
) ) } ) ) )
190132, 184, 1893bitr3d 275 . . 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 ) ) } ) ) )
191 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =  U )
192191preq1d 3889 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  =  { U ,  ( P `
 ( N  + 
1 ) ) } )
193192opeq2d 3991 . . . . . . . . . . . 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 ) ) } >. )
194193sneqd 3827 . . . . . . . . . . 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 ) ) } >. } )
195194oveq2d 6097 . . . . . . . . . 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 ) ) } >. } ) )
196195fveq1d 5730 . . . . . . . . 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 ) )
197103ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  V  e.  _V )
19864a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( F `  ( N  +  1 ) )  e.  _V )
199119ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
200116ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  e.  V )
201 simplr 732 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )
202191, 201eqnetrrd 2621 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
203202necomd 2687 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  =/=  U )
204197, 198, 199, 200, 203vdgr1b 21675 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
205196, 204eqtrd 2468 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
206205oveq2d 6097 . . . . . . 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 ) )
207206breq2d 4224 . . . . . 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 ) ) )
208207notbid 286 . . . . 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 ) ) )
209 2nn 10133 . . . . . . . . . . . 12  |-  2  e.  NN
210209a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  NN )
211 1lt2 10142 . . . . . . . . . . . 12  |-  1  <  2
212211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  <  2 )
213 ndvdsp1 12929 . . . . . . . . . . 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 ) ) )
214138, 210, 212, 213syl3anc 1184 . . . . . . . . . 10  |-  ( ph  ->  ( 2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  ->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
215214con2d 109 . . . . . . . . 9  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  ->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) ) )
216 2prm 13095 . . . . . . . . . . . . 13  |-  2  e.  Prime
217 nprmdvds1 13111 . . . . . . . . . . . . 13  |-  ( 2  e.  Prime  ->  -.  2  ||  1 )
218216, 217ax-mp 8 . . . . . . . . . . . 12  |-  -.  2  ||  1
219 opoe 13185 . . . . . . . . . . . 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 ) )
2202, 218, 219mpanr12 667 . . . . . . . . . . 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 ) )
221220ex 424 . . . . . . . . . 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 ) ) )
222138, 221syl 16 . . . . . . . . 9  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  -> 
2  ||  ( (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
223215, 222impbid 184 . . . . . . . 8  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
224223, 131bitrd 245 . . . . . . 7  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
225224notbid 286 . . . . . 6  |-  ( ph  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 )  <->  -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } ) ) )
226225ad2antrr 707 . . . . 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 ) } ) ) )
227 fvex 5742 . . . . . . 7  |-  ( P `
 N )  e. 
_V
228227eupath2lem2 21700 . . . . . 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
) ) } ) ) )
229228adantll 695 . . . . 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 ) ) } ) ) )
230208, 226, 2293bitrd 271 . . . 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 ) ) } ) ) )
231 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
232231preq2d 3890 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  U } )
233232opeq2d 3991 . . . . . . . . . . . 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 } >. )
234233sneqd 3827 . . . . . . . . . . 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 } >. } )
235234oveq2d 6097 . . . . . . . . . 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 } >. } ) )
236235fveq1d 5730 . . . . . . . . 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
) )
237103ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  V  e.  _V )
23864a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
239119ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  U  e.  V )
240109ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  e.  V )
241 simplr 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  ( P `
 ( N  + 
1 ) ) )
242241, 231neeqtrd 2623 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  U )
243237, 238, 239, 240, 242vdgr1c 21676 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) `  U )  =  1 )
244236, 243eqtrd 2468 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  1 )
245244oveq2d 6097 . . . . . . 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 ) )
246245breq2d 4224 . . . . . 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 ) ) )
247246notbid 286 . . . . 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 ) ) )
248225ad2antrr 707 . . . . 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 ) } ) ) )
249 necom 2685 . . . . . . . 8  |-  ( ( P `  N )  =/=  ( P `  ( N  +  1
) )  <->  ( P `  ( N  +  1 ) )  =/=  ( P `  N )
)
250 fvex 5742 . . . . . . . . 9  |-  ( P `
 ( N  + 
1 ) )  e. 
_V
251250eupath2lem2 21700 . . . . . . . 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 ) } ) ) )
252249, 251sylanb 459 . . . . . . 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 ) } ) ) )
253252con1bid 321 . . . . . 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
) ) } ) ) )
254253adantll 695 . . . . 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
) ) } ) ) )
255247, 248, 2543bitrd 271 . . . 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
) ) } ) ) )
256103ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  V  e.  _V )
25764a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( F `  ( N  +  1
) )  e.  _V )
258119ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  e.  V
)
259109ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  e.  V
)
260 simprl 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  =/=  U
)
261116ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  e.  V
)
262 simprr 734 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  =/=  U
)
263256, 257, 258, 259, 260, 261, 262vdgr1a 21677 . . . . . . . . 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 )
264263oveq2d 6097 . . . . . . . 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 ) )
265179addid1d 9266 . . . . . . . . 9  |-  ( ph  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  0 )  =  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )
266265ad2antrr 707 . . . . . . . 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 ) )
267264, 266eqtrd 2468 . . . . . . 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 ) )
268267breq2d 4224 . . . . . 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 ) ) )
269268notbid 286 . . . . 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 ) ) )
270131ad2antrr 707 . . . . 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 ) } ) ) )
271260necomd 2687 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  N )
)
272262necomd 2687 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
273271, 2722thd 232 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =/=  ( P `  N
)  <->  U  =/=  ( P `  ( N  +  1 ) ) ) )
274 neeq1 2609 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  N )  <->  ( P `  0 )  =/=  ( P `  N
) ) )
275 neeq1 2609 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  ( N  +  1
) )  <->  ( P `  0 )  =/=  ( P `  ( N  +  1 ) ) ) )
276274, 275bibi12d 313 . . . . . . . . 9  |-  ( U  =  ( P ` 
0 )  ->  (
( U  =/=  ( P `  N )  <->  U  =/=  ( P `  ( N  +  1
) ) )  <->  ( ( P `  0 )  =/=  ( P `  N
)  <->  ( P ` 
0 )  =/=  ( P `  ( N  +  1 ) ) ) ) )
277273, 276syl5ibcom 212 . . . . . . . 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 ) ) ) ) )
278277pm5.32rd 622 . . . . . . 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
) ) ) )
279271neneqd 2617 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  N ) )
280 biorf 395 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 N )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  N )  \/  U  =  ( P `  0 ) ) ) )
281279, 280syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  N
)  \/  U  =  ( P `  0
) ) ) )
282 orcom 377 . . . . . . . . 9  |-  ( ( U  =  ( P `
 N )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  N ) ) )
283281, 282syl6bb 253 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  N
) ) ) )
284283anbi2d 685 . . . . . . 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 ) ) ) ) )
285272neneqd 2617 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  ( N  +  1 ) ) )
286 biorf 395 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 ( N  + 
1 ) )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0 ) ) ) )
287285, 286syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0
) ) ) )
288 orcom 377 . . . . . . . . 9  |-  ( ( U  =  ( P `
 ( N  + 
1 ) )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  ( N  +  1 ) ) ) )
289287, 288syl6bb 253 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  ( N  +  1 ) ) ) ) )
290289anbi2d 685 . . . . . . 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
) ) ) ) ) )
291278, 284, 2903bitr3d 275 . . . . . 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
) ) ) ) ) )
292 eupath2lem1 21699 . . . . . . 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 ) ) ) ) )
293258, 292syl 16 . . . . . 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 ) ) ) ) )
294 eupath2lem1 21699 . . . . . . 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
) ) ) ) ) )
295258, 294syl 16 . . . . . 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
) ) ) ) ) )
296291, 293, 2953bitr4d 277 . . . . 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
) ) } ) ) )
297269, 270, 2963bitrd 271 . . . 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
) ) } ) ) )
298230, 255, 297pm2.61da2ne 2683 . . 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 ) ) } ) ) )
299190, 298pm2.61dane 2682 . 2  |-  ( ph  ->  ( -.  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
) ) } ) ) )
300123, 299bitrd 245 1  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... ( N  +  1 ) ) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  ( N  +  1 ) ) ,  (/) ,  { ( P `  0 ) ,  ( P `  ( N  +  1
) ) } ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1652    e. wcel 1725    =/= wne 2599   {crab 2709   _Vcvv 2956    u. cun 3318    i^i cin 3319    C_ wss 3320   (/)c0 3628   ifcif 3739   {csn 3814   {cpr 3815   <.cop 3817   class class class wbr 4212   ran crn 4879    |` cres 4880   "cima 4881    Fn wfn 5449   -->wf 5450   -1-1->wf1 5451   -onto->wfo 5452   -1-1-onto->wf1o 5453   ` cfv 5454  (class class class)co 6081   Fincfn 7109   CCcc 8988   RRcr 8989   0cc0 8990   1c1 8991    + caddc 8993    < clt 9120    <_ cle 9121    - cmin 9291   NNcn 10000   2c2 10049   NN0cn0 10221   ZZcz 10282   ZZ>=cuz 10488   ...cfz 11043   #chash 11618    || cdivides 12852   Primecprime 13079   UMGrph cumg 21347   VDeg cvdg 21664   EulPaths ceup 21684
This theorem is referenced by:  eupath2  21702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950 &nb