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

Theorem eupath2lem3 23535
Description: Lemma for eupath2 23536. (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 5246 . . . . . . . . . . 11  |-  ( F
" ( ( 1 ... N )  u. 
{ ( N  + 
1 ) } ) )  =  ( ( F " ( 1 ... N ) )  u.  ( F " { ( N  + 
1 ) } ) )
2 1z 10672 . . . . . . . . . . . . 13  |-  1  e.  ZZ
3 eupath2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN0 )
4 nn0uz 10891 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
5 1m1e0 10386 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
65fveq2i 5691 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
74, 6eqtr4i 2464 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
83, 7syl6eleq 2531 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )
9 fzsuc2 11510 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
102, 8, 9sylancr 658 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
1110imaeq2d 5166 . . . . . . . . . . 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 23526 . . . . . . . . . . . . . . 15  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
1512, 13, 14syl2anc 656 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
16 f1ofn 5639 . . . . . . . . . . . . . 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 10615 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
203, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
21 nnuz 10892 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2531 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
23 eupacl 23525 . . . . . . . . . . . . . . . . 17  |-  ( F ( V EulPaths  E ) P  ->  ( # `  F
)  e.  NN0 )
2412, 23syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  F
)  e.  NN0 )
2524nn0zd 10741 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  F
)  e.  ZZ )
26 elfz5 11441 . . . . . . . . . . . . . . 15  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2722, 25, 26syl2anc 656 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2818, 27mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )
29 fnsnfv 5748 . . . . . . . . . . . . 13  |-  ( ( F  Fn  ( 1 ... ( # `  F
) )  /\  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3017, 28, 29syl2anc 656 . . . . . . . . . . . 12  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3130uneq2d 3507 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } )  =  ( ( F "
( 1 ... N
) )  u.  ( F " { ( N  +  1 ) } ) ) )
321, 11, 313eqtr4a 2499 . . . . . . . . . 10  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( ( F
" ( 1 ... N ) )  u. 
{ ( F `  ( N  +  1
) ) } ) )
3332reseq2d 5106 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) ) )
34 resundi 5121 . . . . . . . . 9  |-  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )
3533, 34syl6eq 2489 . . . . . . . 8  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) ) )
36 f1of 5638 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) ) --> A )
3715, 36syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) --> A )
3837, 28ffvelrnd 5841 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( N  +  1 ) )  e.  A )
39 fnressn 5891 . . . . . . . . . . 11  |-  ( ( E  Fn  A  /\  ( F `  ( N  +  1 ) )  e.  A )  -> 
( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
4013, 38, 39syl2anc 656 . . . . . . . . . 10  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
41 eupaseg 23529 . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  ( ( N  +  1 )  -  1 ) ) ,  ( P `  ( N  +  1
) ) } )
433nn0cnd 10634 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  CC )
44 ax-1cn 9336 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
45 pncan 9612 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
4643, 44, 45sylancl 657 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
4746fveq2d 5692 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P `  (
( N  +  1 )  -  1 ) )  =  ( P `
 N ) )
4847preq1d 3957 . . . . . . . . . . . . 13  |-  ( ph  ->  { ( P `  ( ( N  + 
1 )  -  1 ) ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
4942, 48eqtrd 2473 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5049opeq2d 4063 . . . . . . . . . . 11  |-  ( ph  -> 
<. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >.  =  <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. )
5150sneqd 3886 . . . . . . . . . 10  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  ( E `  ( F `
 ( N  + 
1 ) ) )
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )
5240, 51eqtrd 2473 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } )
5352uneq2d 3507 . . . . . . . 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 2473 . . . . . . 7  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) )
5554oveq2d 6106 . . . . . 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 5690 . . . . 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 5177 . . . . . . . 8  |-  ( F
" ( 1 ... N ) )  C_  ran  F
58 f1ofo 5645 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-onto-> A )
59 forn 5620 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -onto-> A  ->  ran  F  =  A )
6015, 58, 593syl 20 . . . . . . . 8  |-  ( ph  ->  ran  F  =  A )
6157, 60syl5sseq 3401 . . . . . . 7  |-  ( ph  ->  ( F " (
1 ... N ) ) 
C_  A )
62 fnssres 5521 . . . . . . 7  |-  ( ( E  Fn  A  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
6313, 61, 62syl2anc 656 . . . . . 6  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
64 fvex 5698 . . . . . . . 8  |-  ( F `
 ( N  + 
1 ) )  e. 
_V
65 prex 4531 . . . . . . . 8  |-  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  e.  _V
6664, 65fnsn 5468 . . . . . . 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 23527 . . . . . . . 8  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  A  e.  Fin )
6912, 13, 68syl2anc 656 . . . . . . 7  |-  ( ph  ->  A  e.  Fin )
70 ssfi 7529 . . . . . . 7  |-  ( ( A  e.  Fin  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( F " (
1 ... N ) )  e.  Fin )
7169, 61, 70syl2anc 656 . . . . . 6  |-  ( ph  ->  ( F " (
1 ... N ) )  e.  Fin )
72 snfi 7386 . . . . . . 7  |-  { ( F `  ( N  +  1 ) ) }  e.  Fin
7372a1i 11 . . . . . 6  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  e.  Fin )
743nn0red 10633 . . . . . . . . . 10  |-  ( ph  ->  N  e.  RR )
7574ltp1d 10259 . . . . . . . . 9  |-  ( ph  ->  N  <  ( N  +  1 ) )
76 peano2re 9538 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
7774, 76syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  RR )
7874, 77ltnled 9517 . . . . . . . . 9  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
7975, 78mpbid 210 . . . . . . . 8  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
80 f1of1 5637 . . . . . . . . . . 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 10741 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
8382peano2zd 10746 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
84 eluz2 10863 . . . . . . . . . . . . 13  |-  ( (
# `  F )  e.  ( ZZ>= `  ( N  +  1 ) )  <-> 
( ( N  + 
1 )  e.  ZZ  /\  ( # `  F
)  e.  ZZ  /\  ( N  +  1
)  <_  ( # `  F
) ) )
8583, 25, 18, 84syl3anbrc 1167 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  ( N  +  1
) ) )
86 peano2uzr 10906 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  ( # `  F )  e.  ( ZZ>= `  ( N  +  1 ) ) )  ->  ( # `
 F )  e.  ( ZZ>= `  N )
)
8782, 85, 86syl2anc 656 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  N ) )
88 fzss2 11494 . . . . . . . . . . 11  |-  ( (
# `  F )  e.  ( ZZ>= `  N )  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
8987, 88syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
90 f1elima 5973 . . . . . . . . . 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 1213 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  e.  ( 1 ... N ) ) )
92 elfz5 11441 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... N )  <->  ( N  +  1 )  <_  N ) )
9322, 82, 92syl2anc 656 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... N )  <-> 
( N  +  1 )  <_  N )
)
9491, 93bitrd 253 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  <_  N )
)
9579, 94mtbird 301 . . . . . . 7  |-  ( ph  ->  -.  ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) ) )
96 disjsn 3933 . . . . . . 7  |-  ( ( ( F " (
1 ... N ) )  i^i  { ( F `
 ( N  + 
1 ) ) } )  =  (/)  <->  -.  ( F `  ( N  +  1 ) )  e.  ( F "
( 1 ... N
) ) )
9795, 96sylibr 212 . . . . . 6  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  i^i  {
( F `  ( N  +  1 ) ) } )  =  (/) )
98 eupagra 23522 . . . . . . 7  |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
99 umgrares 23193 . . . . . . 7  |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  ( F " (
1 ... N ) ) ) )
10012, 98, 993syl 20 . . . . . 6  |-  ( ph  ->  V UMGrph  ( E  |`  ( F " ( 1 ... N ) ) ) )
101 relumgra 23183 . . . . . . . . 9  |-  Rel UMGrph
102101brrelexi 4875 . . . . . . . 8  |-  ( V UMGrph  E  ->  V  e.  _V )
10312, 98, 1023syl 20 . . . . . . 7  |-  ( ph  ->  V  e.  _V )
104 eupapf 23528 . . . . . . . . 9  |-  ( F ( V EulPaths  E ) P  ->  P : ( 0 ... ( # `  F ) ) --> V )
10512, 104syl 16 . . . . . . . 8  |-  ( ph  ->  P : ( 0 ... ( # `  F
) ) --> V )
1063, 4syl6eleq 2531 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
107 elfzuzb 11443 . . . . . . . . 9  |-  ( N  e.  ( 0 ... ( # `  F
) )  <->  ( N  e.  ( ZZ>= `  0 )  /\  ( # `  F
)  e.  ( ZZ>= `  N ) ) )
108106, 87, 107sylanbrc 659 . . . . . . . 8  |-  ( ph  ->  N  e.  ( 0 ... ( # `  F
) ) )
109105, 108ffvelrnd 5841 . . . . . . 7  |-  ( ph  ->  ( P `  N
)  e.  V )
110 peano2nn0 10616 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
1113, 110syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
112111, 4syl6eleq 2531 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
113 elfz5 11441 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
0 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 0 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
114112, 25, 113syl2anc 656 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 0 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
11518, 114mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  ( 0 ... ( # `  F
) ) )
116105, 115ffvelrnd 5841 . . . . . . 7  |-  ( ph  ->  ( P `  ( N  +  1 ) )  e.  V )
117 umgra1 23195 . . . . . . 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 1214 . . . . . 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 23507 . . . . 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 2473 . . . 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 4301 . . 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 294 . 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 5688 . . . . . . . . . 10  |-  ( x  =  U  ->  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
)  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )
125124breq2d 4301 . . . . . . . . 9  |-  ( x  =  U  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x )  <->  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) ) )
126125notbid 294 . . . . . . . 8  |-  ( x  =  U  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
)  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
127126elrab3 3115 . . . . . . 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 2508 . . . . . 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 255 . . . . 5  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
132131adantr 462 . . . 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 10674 . . . . . . . 8  |-  2  e.  ZZ
134133a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  e.  ZZ )
135 vdgrfif 23504 . . . . . . . . . . 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 1213 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) : V --> NN0 )
137136, 119ffvelrnd 5841 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e. 
NN0 )
138137nn0zd 10741 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ )
139138adantr 462 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  ZZ )
140 vdgrfif 23504 . . . . . . . . . . 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 1213 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0 )
142141, 119ffvelrnd 5841 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
143142nn0zd 10741 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  ZZ )
144143adantr 462 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  e.  ZZ )
145 iddvds 13542 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  2 )
146133, 145ax-mp 5 . . . . . . . . 9  |-  2  ||  2
147 simpr 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  U )
148 simplr 749 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
149148, 147eqtr3d 2475 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
150147, 149preq12d 3959 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U ,  U } )
151 dfsn2 3887 . . . . . . . . . . . . . . 15  |-  { U }  =  { U ,  U }
152150, 151syl6eqr 2491 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U } )
153152opeq2d 4063 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { U } >. )
154153sneqd 3886 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } )
155154oveq2d 6106 . . . . . . . . . . 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 5690 . . . . . . . . . 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 720 . . . . . . . . . . 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 720 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
160157, 158, 159vdgr1d 23508 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) `  U )  =  2 )
161156, 160eqtrd 2473 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  2 )
162146, 161syl5breqr 4325 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
163 dvds0 13544 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  0 )
164133, 163ax-mp 5 . . . . . . . . 9  |-  2  ||  0
165103ad2antrr 720 . . . . . . . . . 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 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  U  e.  V )
168109ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  e.  V )
169 simpr 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =/=  U )
170116ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  e.  V )
171 simplr 749 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
172171, 169eqnetrrd 2626 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  =/=  U )
173165, 166, 167, 168, 169, 170, 172vdgr1a 23511 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  0 )
174164, 173syl5breqr 4325 . . . . . . . 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 2687 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
176 dvdsadd2b 13571 . . . . . . 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 1217 . . . . . 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 10634 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  CC )
179137nn0cnd 10634 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  CC )
180178, 179addcomd 9567 . . . . . . . 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 4301 . . . . . . 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 462 . . . . . 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 253 . . . . 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 294 . . . 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 458 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( P `  N )  =  ( P `  ( N  +  1 ) ) )
186185eqeq2d 2452 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( P `  0 )  =  ( P `  N )  <->  ( P `  0 )  =  ( P `  ( N  +  1 ) ) ) )
187185preq2d 3958 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  { ( P `  0 ) ,  ( P `  N ) }  =  { ( P ` 
0 ) ,  ( P `  ( N  +  1 ) ) } )
188186, 187ifbieq2d 3811 . . . . 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 2508 . . . 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 283 . . 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 458 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =  U )
192191preq1d 3957 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  =  { U ,  ( P `
 ( N  + 
1 ) ) } )
193192opeq2d 4063 . . . . . . . . . . . 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 3886 . . . . . . . . . . 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 6106 . . . . . . . . . 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 5690 . . . . . . . . 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 720 . . . . . . . . . 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 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
200116ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  e.  V )
201 simplr 749 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )
202191, 201eqnetrrd 2626 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
203202necomd 2693 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  =/=  U )
204197, 198, 199, 200, 203vdgr1b 23509 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
205196, 204eqtrd 2473 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
206205oveq2d 6106 . . . . . . 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 4301 . . . . . 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 294 . . . . 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 10475 . . . . . . . . . . . 12  |-  2  e.  NN
210209a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  NN )
211 1lt2 10484 . . . . . . . . . . . 12  |-  1  <  2
212211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  <  2 )
213 ndvdsp1 13609 . . . . . . . . . . 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 1213 . . . . . . . . . 10  |-  ( ph  ->  ( 2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  ->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
215214con2d 115 . . . . . . . . 9  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  ->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) ) )
216 n2dvds1 13578 . . . . . . . . . . . 12  |-  -.  2  ||  1
217 opoe 13874 . . . . . . . . . . . 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 ) )
2182, 216, 217mpanr12 680 . . . . . . . . . . 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 ) )
219218ex 434 . . . . . . . . . 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 ) ) )
220138, 219syl 16 . . . . . . . . 9  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  -> 
2  ||  ( (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
221215, 220impbid 191 . . . . . . . 8  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
222221, 131bitrd 253 . . . . . . 7  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
223222notbid 294 . . . . . 6  |-  ( ph  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 )  <->  -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } ) ) )
224223ad2antrr 720 . . . . 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 ) } ) ) )
225 fvex 5698 . . . . . . 7  |-  ( P `
 N )  e. 
_V
226225eupath2lem2 23534 . . . . . 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
) ) } ) ) )
227226adantll 708 . . . . 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 ) ) } ) ) )
228208, 224, 2273bitrd 279 . . . 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 ) ) } ) ) )
229 simpr 458 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
230229preq2d 3958 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  U } )
231230opeq2d 4063 . . . . . . . . . . . 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 } >. )
232231sneqd 3886 . . . . . . . . . . 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 } >. } )
233232oveq2d 6106 . . . . . . . . . 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 } >. } ) )
234233fveq1d 5690 . . . . . . . . 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
) )
235103ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  V  e.  _V )
23664a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( F `  ( N  +  1 ) )  e.  _V )
237119ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  U  e.  V )
238109ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  e.  V )
239 simplr 749 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  ( P `
 ( N  + 
1 ) ) )
240239, 229neeqtrd 2628 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  U )
241235, 236, 237, 238, 240vdgr1c 23510 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) `  U )  =  1 )
242234, 241eqtrd 2473 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  1 )
243242oveq2d 6106 . . . . . . 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 ) )
244243breq2d 4301 . . . . . 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 ) ) )
245244notbid 294 . . . . 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 ) ) )
246223ad2antrr 720 . . . . 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 ) } ) ) )
247 necom 2691 . . . . . . . 8  |-  ( ( P `  N )  =/=  ( P `  ( N  +  1
) )  <->  ( P `  ( N  +  1 ) )  =/=  ( P `  N )
)
248 fvex 5698 . . . . . . . . 9  |-  ( P `
 ( N  + 
1 ) )  e. 
_V
249248eupath2lem2 23534 . . . . . . . 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 ) } ) ) )
250247, 249sylanb 469 . . . . . . 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 ) } ) ) )
251250con1bid 330 . . . . . 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
) ) } ) ) )
252251adantll 708 . . . . 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
) ) } ) ) )
253245, 246, 2523bitrd 279 . . . 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
) ) } ) ) )
254103ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  V  e.  _V )
25564a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( F `  ( N  +  1
) )  e.  _V )
256119ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  e.  V
)
257109ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  e.  V
)
258 simprl 750 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  =/=  U
)
259116ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  e.  V
)
260 simprr 751 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  =/=  U
)
261254, 255, 256, 257, 258, 259, 260vdgr1a 23511 . . . . . . . . 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 )
262261oveq2d 6106 . . . . . . . 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 ) )
263179addid1d 9565 . . . . . . . . 9  |-  ( ph  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  0 )  =  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )
264263ad2antrr 720 . . . . . . . 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 ) )
265262, 264eqtrd 2473 . . . . . . 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 ) )
266265breq2d 4301 . . . . . 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 ) ) )
267266notbid 294 . . . . 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 ) ) )
268131ad2antrr 720 . . . . 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 ) } ) ) )
269258necomd 2693 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  N )
)
270260necomd 2693 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
271269, 2702thd 240 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =/=  ( P `  N
)  <->  U  =/=  ( P `  ( N  +  1 ) ) ) )
272 neeq1 2614 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  N )  <->  ( P `  0 )  =/=  ( P `  N
) ) )
273 neeq1 2614 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  ( N  +  1
) )  <->  ( P `  0 )  =/=  ( P `  ( N  +  1 ) ) ) )
274272, 273bibi12d 321 . . . . . . . . 9  |-  ( U  =  ( P ` 
0 )  ->  (
( U  =/=  ( P `  N )  <->  U  =/=  ( P `  ( N  +  1
) ) )  <->  ( ( P `  0 )  =/=  ( P `  N
)  <->  ( P ` 
0 )  =/=  ( P `  ( N  +  1 ) ) ) ) )
275271, 274syl5ibcom 220 . . . . . . . 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 ) ) ) ) )
276275pm5.32rd 635 . . . . . . 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
) ) ) )
277269neneqd 2622 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  N ) )
278 biorf 405 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 N )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  N )  \/  U  =  ( P `  0 ) ) ) )
279277, 278syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  N
)  \/  U  =  ( P `  0
) ) ) )
280 orcom 387 . . . . . . . . 9  |-  ( ( U  =  ( P `
 N )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  N ) ) )
281279, 280syl6bb 261 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  N
) ) ) )
282281anbi2d 698 . . . . . . 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 ) ) ) ) )
283270neneqd 2622 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  ( N  +  1 ) ) )
284 biorf 405 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 ( N  + 
1 ) )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0 ) ) ) )
285283, 284syl 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
) ) ) )
286 orcom 387 . . . . . . . . 9  |-  ( ( U  =  ( P `
 ( N  + 
1 ) )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  ( N  +  1 ) ) ) )
287285, 286syl6bb 261 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  ( N  +  1 ) ) ) ) )
288287anbi2d 698 . . . . . . 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
) ) ) ) ) )
289276, 282, 2883bitr3d 283 . . . . . 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
) ) ) ) ) )
290 eupath2lem1 23533 . . . . . . 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 ) ) ) ) )
291256, 290syl 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 ) ) ) ) )
292 eupath2lem1 23533 . . . . . . 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
) ) ) ) ) )
293256, 292syl 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
) ) ) ) ) )
294289, 291, 2933bitr4d 285 . . . . 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
) ) } ) ) )
295267, 268, 2943bitrd 279 . . . 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
) ) } ) ) )
296228, 253, 295pm2.61da2ne 2688 . . 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 ) ) } ) ) )
297190, 296pm2.61dane 2687 . 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
) ) } ) ) )
298123, 297bitrd 253 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1364    e. wcel 1761    =/= wne 2604   {crab 2717   _Vcvv 2970    u. cun 3323    i^i cin 3324    C_ wss 3325   (/)c0 3634   ifcif 3788   {csn 3874   {cpr 3876   <.cop 3880   class class class wbr 4289   ran crn 4837    |` cres 4838   "cima 4839    Fn wfn 5410   -->wf 5411   -1-1->wf1 5412   -onto->wfo 5413   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   Fincfn 7306   CCcc 9276   RRcr 9277   0cc0 9278   1c1 9279    + caddc 9281    < clt 9414    <_ cle 9415    - cmin 9591   NNcn 10318   2c2 10367   NN0cn0 10575   ZZcz 10642   ZZ>=cuz 10857   ...cfz 11433   #chash 12099    || cdivides 13531   UMGrph cumg 23181   VDeg cvdg 23498   EulPaths ceup 23518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346 &nbs