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

Theorem eupath2lem3 21662
Description: Lemma for eupath2 21663. (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 5251 . . . . . . . . . . 11  |-  ( F
" ( ( 1 ... N )  u. 
{ ( N  + 
1 ) } ) )  =  ( ( F " ( 1 ... N ) )  u.  ( F " { ( N  + 
1 ) } ) )
2 1z 10275 . . . . . . . . . . . . 13  |-  1  e.  ZZ
3 eupath2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN0 )
4 nn0uz 10484 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
5 1m1e0 10032 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
65fveq2i 5698 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
74, 6eqtr4i 2435 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
83, 7syl6eleq 2502 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )
9 fzsuc2 11068 . . . . . . . . . . . . 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 5170 . . . . . . . . . . 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 21653 . . . . . . . . . . . . . . 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 5642 . . . . . . . . . . . . . 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 10223 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
203, 19syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
21 nnuz 10485 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2502 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
23 eupacl 21652 . . . . . . . . . . . . . . . . 17  |-  ( F ( V EulPaths  E ) P  ->  ( # `  F
)  e.  NN0 )
2412, 23syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  F
)  e.  NN0 )
2524nn0zd 10337 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  F
)  e.  ZZ )
26 elfz5 11015 . . . . . . . . . . . . . . 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 5753 . . . . . . . . . . . . 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 3469 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } )  =  ( ( F "
( 1 ... N
) )  u.  ( F " { ( N  +  1 ) } ) ) )
321, 11, 313eqtr4a 2470 . . . . . . . . . 10  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( ( F
" ( 1 ... N ) )  u. 
{ ( F `  ( N  +  1
) ) } ) )
3332reseq2d 5113 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) ) )
34 resundi 5127 . . . . . . . . 9  |-  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )
3533, 34syl6eq 2460 . . . . . . . 8  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) ) )
36 f1of 5641 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) ) --> A )
3715, 36syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) --> A )
3837, 28ffvelrnd 5838 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( N  +  1 ) )  e.  A )
39 fnressn 5885 . . . . . . . . . . 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 21656 . . . . . . . . . . . . . 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 10240 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  CC )
44 ax-1cn 9012 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
45 pncan 9275 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
4643, 44, 45sylancl 644 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
4746fveq2d 5699 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P `  (
( N  +  1 )  -  1 ) )  =  ( P `
 N ) )
4847preq1d 3857 . . . . . . . . . . . . 13  |-  ( ph  ->  { ( P `  ( ( N  + 
1 )  -  1 ) ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
4942, 48eqtrd 2444 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5049opeq2d 3959 . . . . . . . . . . 11  |-  ( ph  -> 
<. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >.  =  <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. )
5150sneqd 3795 . . . . . . . . . 10  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  ( E `  ( F `
 ( N  + 
1 ) ) )
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )
5240, 51eqtrd 2444 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } )
5352uneq2d 3469 . . . . . . . 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 2444 . . . . . . 7  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) )
5554oveq2d 6064 . . . . . 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 5697 . . . . 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 5183 . . . . . . . 8  |-  ( F
" ( 1 ... N ) )  C_  ran  F
58 f1ofo 5648 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-onto-> A )
59 forn 5623 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -onto-> A  ->  ran  F  =  A )
6015, 58, 593syl 19 . . . . . . . 8  |-  ( ph  ->  ran  F  =  A )
6157, 60syl5sseq 3364 . . . . . . 7  |-  ( ph  ->  ( F " (
1 ... N ) ) 
C_  A )
62 fnssres 5525 . . . . . . 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 5709 . . . . . . . 8  |-  ( F `
 ( N  + 
1 ) )  e. 
_V
65 prex 4374 . . . . . . . 8  |-  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  e.  _V
6664, 65fnsn 5471 . . . . . . 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 21654 . . . . . . . 8  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  A  e.  Fin )
6912, 13, 68syl2anc 643 . . . . . . 7  |-  ( ph  ->  A  e.  Fin )
70 ssfi 7296 . . . . . . 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 7154 . . . . . . 7  |-  { ( F `  ( N  +  1 ) ) }  e.  Fin
7372a1i 11 . . . . . 6  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  e.  Fin )
743nn0red 10239 . . . . . . . . . 10  |-  ( ph  ->  N  e.  RR )
7574ltp1d 9905 . . . . . . . . 9  |-  ( ph  ->  N  <  ( N  +  1 ) )
76 peano2re 9203 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
7774, 76syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  RR )
7874, 77ltnled 9184 . . . . . . . . 9  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
7975, 78mpbid 202 . . . . . . . 8  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
80 f1of1 5640 . . . . . . . . . . 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 10337 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
8382peano2zd 10342 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
84 eluz2 10458 . . . . . . . . . . . . 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 10496 . . . . . . . . . . . 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 11056 . . . . . . . . . . 11  |-  ( (
# `  F )  e.  ( ZZ>= `  N )  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
8987, 88syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
90 f1elima 5976 . . . . . . . . . 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 11015 . . . . . . . . . 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 3836 . . . . . . 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 21649 . . . . . . 7  |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
99 umgrares 21320 . . . . . . 7  |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  ( F " (
1 ... N ) ) ) )
10012, 98, 993syl 19 . . . . . 6  |-  ( ph  ->  V UMGrph  ( E  |`  ( F " ( 1 ... N ) ) ) )
101 relumgra 21310 . . . . . . . . 9  |-  Rel UMGrph
102101brrelexi 4885 . . . . . . . 8  |-  ( V UMGrph  E  ->  V  e.  _V )
10312, 98, 1023syl 19 . . . . . . 7  |-  ( ph  ->  V  e.  _V )
104 eupapf 21655 . . . . . . . . 9  |-  ( F ( V EulPaths  E ) P  ->  P : ( 0 ... ( # `  F ) ) --> V )
10512, 104syl 16 . . . . . . . 8  |-  ( ph  ->  P : ( 0 ... ( # `  F
) ) --> V )
1063, 4syl6eleq 2502 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
107 elfzuzb 11017 . . . . . . . . 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 5838 . . . . . . 7  |-  ( ph  ->  ( P `  N
)  e.  V )
110 peano2nn0 10224 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
1113, 110syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
112111, 4syl6eleq 2502 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
113 elfz5 11015 . . . . . . . . . 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 5838 . . . . . . 7  |-  ( ph  ->  ( P `  ( N  +  1 ) )  e.  V )
117 umgra1 21322 . . . . . . 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 21634 . . . . 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 2444 . . . 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 4192 . . 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 5695 . . . . . . . . . 10  |-  ( x  =  U  ->  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
)  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )
125124breq2d 4192 . . . . . . . . 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 3061 . . . . . . 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 2479 . . . . . 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 10276 . . . . . . . 8  |-  2  e.  ZZ
134133a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  e.  ZZ )
135 vdgrfif 21631 . . . . . . . . . . 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 5838 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e. 
NN0 )
138137nn0zd 10337 . . . . . . . 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 21631 . . . . . . . . . . 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 5838 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
143142nn0zd 10337 . . . . . . . 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 12826 . . . . . . . . . 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 2446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
150147, 149preq12d 3859 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U ,  U } )
151 dfsn2 3796 . . . . . . . . . . . . . . 15  |-  { U }  =  { U ,  U }
152150, 151syl6eqr 2462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U } )
153152opeq2d 3959 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { U } >. )
154153sneqd 3795 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } )
155154oveq2d 6064 . . . . . . . . . . 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 5697 . . . . . . . . . 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 21635 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) `  U )  =  2 )
161156, 160eqtrd 2444 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  2 )
162146, 161syl5breqr 4216 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
163 dvds0 12828 . . . . . . . . . 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 2595 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  =/=  U )
173165, 166, 167, 168, 169, 170, 172vdgr1a 21638 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  0 )
174164, 173syl5breqr 4216 . . . . . . . 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 2653 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
176 dvdsadd2b 12855 . . . . . . 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 10240 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  CC )
179137nn0cnd 10240 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  CC )
180178, 179addcomd 9232 . . . . . . . 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 4192 . . . . . . 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 2423 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( P `  0 )  =  ( P `  N )  <->  ( P `  0 )  =  ( P `  ( N  +  1 ) ) ) )
187185preq2d 3858 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  { ( P `  0 ) ,  ( P `  N ) }  =  { ( P ` 
0 ) ,  ( P `  ( N  +  1 ) ) } )
188186, 187ifbieq2d 3727 . . . . 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 2479 . . . 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 3857 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  =  { U ,  ( P `
 ( N  + 
1 ) ) } )
193192opeq2d 3959 . . . . . . . . . . . 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 3795 . . . . . . . . . . 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 6064 . . . . . . . . . 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 5697 . . . . . . . . 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 2595 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
203202necomd 2658 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  =/=  U )
204197, 198, 199, 200, 203vdgr1b 21636 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
205196, 204eqtrd 2444 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
206205oveq2d 6064 . . . . . . 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 4192 . . . . . 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 10097 . . . . . . . . . . . 12  |-  2  e.  NN
210209a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  NN )
211 1lt2 10106 . . . . . . . . . . . 12  |-  1  <  2
212211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  <  2 )
213 ndvdsp1 12892 . . . . . . . . . . 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 13058 . . . . . . . . . . . . 13  |-  2  e.  Prime
217 nprmdvds1 13074 . . . . . . . . . . . . 13  |-  ( 2  e.  Prime  ->  -.  2  ||  1 )
218216, 217ax-mp 8 . . . . . . . . . . . 12  |-  -.  2  ||  1
219 opoe 13148 . . . . . . . . . . . 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 5709 . . . . . . 7  |-  ( P `
 N )  e. 
_V
228227eupath2lem2 21661 . . . . . 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 3858 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  U } )
233232opeq2d 3959 . . . . . . . . . . . 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 3795 . . . . . . . . . . 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 6064 . . . . . . . . . 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 5697 . . . . . . . . 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 2597 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  U )
243237, 238, 239, 240, 242vdgr1c 21637 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) `  U )  =  1 )
244236, 243eqtrd 2444 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  1 )
245244oveq2d 6064 . . . . . . 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 4192 . . . . . 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 2656 . . . . . . . 8  |-  ( ( P `  N )  =/=  ( P `  ( N  +  1
) )  <->  ( P `  ( N  +  1 ) )  =/=  ( P `  N )
)
250 fvex 5709 . . . . . . . . 9  |-  ( P `
 ( N  + 
1 ) )  e. 
_V
251250eupath2lem2 21661 . . . . . . . 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 21638 . . . . . . . . 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 6064 . . . . . . . 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 9230 . . . . . . . . 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 2444 . . . . . . 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 4192 . . . . . 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 2658 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  N )
)
272262necomd 2658 . . . . . . . . . 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 2583 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  N )  <->  ( P `  0 )  =/=  ( P `  N
) ) )
275 neeq1 2583 . . . . . . . . . 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 2591 . . . . . . . . . 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 2591 . . . . . . . . . 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 21660 . . . . . . 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 21660 . . . . . . 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 2654 . . 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 2653 . 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 1649    e. wcel 1721    =/= wne 2575   {crab 2678   _Vcvv 2924    u. cun 3286    i^i cin 3287    C_ wss 3288   (/)c0 3596   ifcif 3707   {csn 3782   {cpr 3783   <.cop 3785   class class class wbr 4180   ran crn 4846    |` cres 4847   "cima 4848    Fn wfn 5416   -->wf 5417   -1-1->wf1 5418   -onto->wfo 5419   -1-1-onto->wf1o 5420   ` cfv 5421  (class class class)co 6048   Fincfn 7076   CCcc 8952   RRcr 8953   0cc0 8954   1c1 8955    + caddc 8957    < clt 9084    <_ cle 9085    - cmin 9255   NNcn 9964   2c2 10013   NN0cn0 10185   ZZcz 10246   ZZ>=cuz 10452   ...cfz 11007   #chash 11581    || cdivides 12815   Primecprime 13042   UMGrph cumg 21308   VDeg cvdg 21625   EulPaths ceup 21645
This theorem is referenced by:  eupath2  21663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393