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

Theorem eupath2lem3 25705
Description: Lemma for eupath2 25706. (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 5267 . . . . . . . . . . 11  |-  ( F
" ( ( 1 ... N )  u. 
{ ( N  + 
1 ) } ) )  =  ( ( F " ( 1 ... N ) )  u.  ( F " { ( N  + 
1 ) } ) )
2 1z 10974 . . . . . . . . . . . . 13  |-  1  e.  ZZ
3 eupath2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN0 )
4 nn0uz 11200 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
5 1m1e0 10685 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
65fveq2i 5884 . . . . . . . . . . . . . . 15  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
74, 6eqtr4i 2454 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
83, 7syl6eleq 2517 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )
9 fzsuc2 11860 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  N  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
102, 8, 9sylancr 667 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... N )  u.  { ( N  +  1 ) } ) )
1110imaeq2d 5187 . . . . . . . . . . 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 25696 . . . . . . . . . . . . . . 15  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
1512, 13, 14syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-onto-> A )
16 f1ofn 5832 . . . . . . . . . . . . . 14  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F  Fn  ( 1 ... ( # `
 F ) ) )
1715, 16syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  F  Fn  ( 1 ... ( # `  F
) ) )
18 eupath2.6 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  +  1 )  <_  ( # `  F
) )
19 nn0p1nn 10916 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  ( N  +  1 )  e.  NN )
203, 19syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
21 nnuz 11201 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2517 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
23 eupacl 25695 . . . . . . . . . . . . . . . . 17  |-  ( F ( V EulPaths  E ) P  ->  ( # `  F
)  e.  NN0 )
2412, 23syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  F
)  e.  NN0 )
2524nn0zd 11045 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  F
)  e.  ZZ )
26 elfz5 11799 . . . . . . . . . . . . . . 15  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2722, 25, 26syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
2818, 27mpbird 235 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )
29 fnsnfv 5941 . . . . . . . . . . . . 13  |-  ( ( F  Fn  ( 1 ... ( # `  F
) )  /\  ( N  +  1 )  e.  ( 1 ... ( # `  F
) ) )  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3017, 28, 29syl2anc 665 . . . . . . . . . . . 12  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  =  ( F " { ( N  +  1 ) } ) )
3130uneq2d 3620 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } )  =  ( ( F "
( 1 ... N
) )  u.  ( F " { ( N  +  1 ) } ) ) )
321, 11, 313eqtr4a 2489 . . . . . . . . . 10  |-  ( ph  ->  ( F " (
1 ... ( N  + 
1 ) ) )  =  ( ( F
" ( 1 ... N ) )  u. 
{ ( F `  ( N  +  1
) ) } ) )
3332reseq2d 5124 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) ) )
34 resundi 5137 . . . . . . . . 9  |-  ( E  |`  ( ( F "
( 1 ... N
) )  u.  {
( F `  ( N  +  1 ) ) } ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) )
3533, 34syl6eq 2479 . . . . . . . 8  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  ( E  |`  { ( F `  ( N  +  1
) ) } ) ) )
36 f1of 5831 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) ) --> A )
3715, 36syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) --> A )
3837, 28ffvelrnd 6038 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  ( N  +  1 ) )  e.  A )
39 fnressn 6091 . . . . . . . . . . 11  |-  ( ( E  Fn  A  /\  ( F `  ( N  +  1 ) )  e.  A )  -> 
( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
4013, 38, 39syl2anc 665 . . . . . . . . . 10  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >. } )
41 eupaseg 25699 . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  ( ( N  +  1 )  -  1 ) ) ,  ( P `  ( N  +  1
) ) } )
433nn0cnd 10934 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  CC )
44 ax-1cn 9604 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
45 pncan 9888 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  + 
1 )  -  1 )  =  N )
4643, 44, 45sylancl 666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  N )
4746fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P `  (
( N  +  1 )  -  1 ) )  =  ( P `
 N ) )
4847preq1d 4085 . . . . . . . . . . . . 13  |-  ( ph  ->  { ( P `  ( ( N  + 
1 )  -  1 ) ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
4942, 48eqtrd 2463 . . . . . . . . . . . 12  |-  ( ph  ->  ( E `  ( F `  ( N  +  1 ) ) )  =  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } )
5049opeq2d 4194 . . . . . . . . . . 11  |-  ( ph  -> 
<. ( F `  ( N  +  1 ) ) ,  ( E `
 ( F `  ( N  +  1
) ) ) >.  =  <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. )
5150sneqd 4010 . . . . . . . . . 10  |-  ( ph  ->  { <. ( F `  ( N  +  1
) ) ,  ( E `  ( F `
 ( N  + 
1 ) ) )
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } )
5240, 51eqtrd 2463 . . . . . . . . 9  |-  ( ph  ->  ( E  |`  { ( F `  ( N  +  1 ) ) } )  =  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } )
5352uneq2d 3620 . . . . . . . 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 2463 . . . . . . 7  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... ( N  +  1 ) ) ) )  =  ( ( E  |`  ( F " (
1 ... N ) ) )  u.  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) )
5554oveq2d 6321 . . . . . 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 5883 . . . . 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 5198 . . . . . . . 8  |-  ( F
" ( 1 ... N ) )  C_  ran  F
58 f1ofo 5838 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-onto-> A )
59 forn 5813 . . . . . . . . 9  |-  ( F : ( 1 ... ( # `  F
) ) -onto-> A  ->  ran  F  =  A )
6015, 58, 593syl 18 . . . . . . . 8  |-  ( ph  ->  ran  F  =  A )
6157, 60syl5sseq 3512 . . . . . . 7  |-  ( ph  ->  ( F " (
1 ... N ) ) 
C_  A )
62 fnssres 5707 . . . . . . 7  |-  ( ( E  Fn  A  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
6313, 61, 62syl2anc 665 . . . . . 6  |-  ( ph  ->  ( E  |`  ( F " ( 1 ... N ) ) )  Fn  ( F "
( 1 ... N
) ) )
64 fvex 5891 . . . . . . . 8  |-  ( F `
 ( N  + 
1 ) )  e. 
_V
65 prex 4663 . . . . . . . 8  |-  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  e.  _V
6664, 65fnsn 5654 . . . . . . 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 25697 . . . . . . . 8  |-  ( ( F ( V EulPaths  E ) P  /\  E  Fn  A )  ->  A  e.  Fin )
6912, 13, 68syl2anc 665 . . . . . . 7  |-  ( ph  ->  A  e.  Fin )
70 ssfi 7801 . . . . . . 7  |-  ( ( A  e.  Fin  /\  ( F " ( 1 ... N ) ) 
C_  A )  -> 
( F " (
1 ... N ) )  e.  Fin )
7169, 61, 70syl2anc 665 . . . . . 6  |-  ( ph  ->  ( F " (
1 ... N ) )  e.  Fin )
72 snfi 7660 . . . . . . 7  |-  { ( F `  ( N  +  1 ) ) }  e.  Fin
7372a1i 11 . . . . . 6  |-  ( ph  ->  { ( F `  ( N  +  1
) ) }  e.  Fin )
743nn0red 10933 . . . . . . . . . 10  |-  ( ph  ->  N  e.  RR )
7574ltp1d 10544 . . . . . . . . 9  |-  ( ph  ->  N  <  ( N  +  1 ) )
76 peano2re 9813 . . . . . . . . . . 11  |-  ( N  e.  RR  ->  ( N  +  1 )  e.  RR )
7774, 76syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  RR )
7874, 77ltnled 9789 . . . . . . . . 9  |-  ( ph  ->  ( N  <  ( N  +  1 )  <->  -.  ( N  +  1 )  <_  N )
)
7975, 78mpbid 213 . . . . . . . 8  |-  ( ph  ->  -.  ( N  + 
1 )  <_  N
)
80 f1of1 5830 . . . . . . . . . . 11  |-  ( F : ( 1 ... ( # `  F
) ) -1-1-onto-> A  ->  F :
( 1 ... ( # `
 F ) )
-1-1-> A )
8115, 80syl 17 . . . . . . . . . 10  |-  ( ph  ->  F : ( 1 ... ( # `  F
) ) -1-1-> A )
823nn0zd 11045 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
8382peano2zd 11050 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  +  1 )  e.  ZZ )
84 eluz2 11172 . . . . . . . . . . . . 13  |-  ( (
# `  F )  e.  ( ZZ>= `  ( N  +  1 ) )  <-> 
( ( N  + 
1 )  e.  ZZ  /\  ( # `  F
)  e.  ZZ  /\  ( N  +  1
)  <_  ( # `  F
) ) )
8583, 25, 18, 84syl3anbrc 1189 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  ( N  +  1
) ) )
86 peano2uzr 11221 . . . . . . . . . . . 12  |-  ( ( N  e.  ZZ  /\  ( # `  F )  e.  ( ZZ>= `  ( N  +  1 ) ) )  ->  ( # `
 F )  e.  ( ZZ>= `  N )
)
8782, 85, 86syl2anc 665 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  F
)  e.  ( ZZ>= `  N ) )
88 fzss2 11845 . . . . . . . . . . 11  |-  ( (
# `  F )  e.  ( ZZ>= `  N )  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
8987, 88syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... N
)  C_  ( 1 ... ( # `  F
) ) )
90 f1elima 6179 . . . . . . . . . 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 1264 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  e.  ( 1 ... N ) ) )
92 elfz5 11799 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 1 ... N )  <->  ( N  +  1 )  <_  N ) )
9322, 82, 92syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 1 ... N )  <-> 
( N  +  1 )  <_  N )
)
9491, 93bitrd 256 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) )  <-> 
( N  +  1 )  <_  N )
)
9579, 94mtbird 302 . . . . . . 7  |-  ( ph  ->  -.  ( F `  ( N  +  1
) )  e.  ( F " ( 1 ... N ) ) )
96 disjsn 4060 . . . . . . 7  |-  ( ( ( F " (
1 ... N ) )  i^i  { ( F `
 ( N  + 
1 ) ) } )  =  (/)  <->  -.  ( F `  ( N  +  1 ) )  e.  ( F "
( 1 ... N
) ) )
9795, 96sylibr 215 . . . . . 6  |-  ( ph  ->  ( ( F "
( 1 ... N
) )  i^i  {
( F `  ( N  +  1 ) ) } )  =  (/) )
98 eupagra 25692 . . . . . . 7  |-  ( F ( V EulPaths  E ) P  ->  V UMGrph  E )
99 umgrares 25049 . . . . . . 7  |-  ( V UMGrph  E  ->  V UMGrph  ( E  |`  ( F " (
1 ... N ) ) ) )
10012, 98, 993syl 18 . . . . . 6  |-  ( ph  ->  V UMGrph  ( E  |`  ( F " ( 1 ... N ) ) ) )
101 relumgra 25039 . . . . . . . . 9  |-  Rel UMGrph
102101brrelexi 4894 . . . . . . . 8  |-  ( V UMGrph  E  ->  V  e.  _V )
10312, 98, 1023syl 18 . . . . . . 7  |-  ( ph  ->  V  e.  _V )
104 eupapf 25698 . . . . . . . . 9  |-  ( F ( V EulPaths  E ) P  ->  P : ( 0 ... ( # `  F ) ) --> V )
10512, 104syl 17 . . . . . . . 8  |-  ( ph  ->  P : ( 0 ... ( # `  F
) ) --> V )
1063, 4syl6eleq 2517 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
107 elfzuzb 11801 . . . . . . . . 9  |-  ( N  e.  ( 0 ... ( # `  F
) )  <->  ( N  e.  ( ZZ>= `  0 )  /\  ( # `  F
)  e.  ( ZZ>= `  N ) ) )
108106, 87, 107sylanbrc 668 . . . . . . . 8  |-  ( ph  ->  N  e.  ( 0 ... ( # `  F
) ) )
109105, 108ffvelrnd 6038 . . . . . . 7  |-  ( ph  ->  ( P `  N
)  e.  V )
110 peano2nn0 10917 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( N  +  1 )  e. 
NN0 )
1113, 110syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( N  +  1 )  e.  NN0 )
112111, 4syl6eleq 2517 . . . . . . . . . 10  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
0 ) )
113 elfz5 11799 . . . . . . . . . 10  |-  ( ( ( N  +  1 )  e.  ( ZZ>= ` 
0 )  /\  ( # `
 F )  e.  ZZ )  ->  (
( N  +  1 )  e.  ( 0 ... ( # `  F
) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
114112, 25, 113syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( ( N  + 
1 )  e.  ( 0 ... ( # `  F ) )  <->  ( N  +  1 )  <_ 
( # `  F ) ) )
11518, 114mpbird 235 . . . . . . . 8  |-  ( ph  ->  ( N  +  1 )  e.  ( 0 ... ( # `  F
) ) )
116105, 115ffvelrnd 6038 . . . . . . 7  |-  ( ph  ->  ( P `  ( N  +  1 ) )  e.  V )
117 umgra1 25051 . . . . . . 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 1265 . . . . . 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 25628 . . . . 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 2463 . . . 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 4435 . . 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 295 . 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 5881 . . . . . . . . . 10  |-  ( x  =  U  ->  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  x
)  =  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) )
125124breq2d 4435 . . . . . . . . 9  |-  ( x  =  U  ->  (
2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x )  <->  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U
) ) )
126125notbid 295 . . . . . . . 8  |-  ( x  =  U  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  x
)  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
127126elrab3 3229 . . . . . . 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 17 . . . . . 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 2492 . . . . . 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 258 . . . . 5  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
132131adantr 466 . . . 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 10976 . . . . . . . 8  |-  2  e.  ZZ
134133a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  e.  ZZ )
135 vdgrfif 25625 . . . . . . . . . . 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 1264 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) : V --> NN0 )
137136, 119ffvelrnd 6038 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e. 
NN0 )
138137nn0zd 11045 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  ZZ )
139138adantr 466 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  e.  ZZ )
140 vdgrfif 25625 . . . . . . . . . . 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 1264 . . . . . . . . . 10  |-  ( ph  ->  ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) : V --> NN0 )
142141, 119ffvelrnd 6038 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  NN0 )
143142nn0zd 11045 . . . . . . . 8  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  ZZ )
144143adantr 466 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
)  e.  ZZ )
145 iddvds 14315 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  2 )
146133, 145ax-mp 5 . . . . . . . . 9  |-  2  ||  2
147 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  U )
148 simplr 760 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
149148, 147eqtr3d 2465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
150147, 149preq12d 4087 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U ,  U } )
151 dfsn2 4011 . . . . . . . . . . . . . . 15  |-  { U }  =  { U ,  U }
152150, 151syl6eqr 2481 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { U } )
153152opeq2d 4194 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >.  = 
<. ( F `  ( N  +  1 ) ) ,  { U } >. )
154153sneqd 4010 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. }  =  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } )
155154oveq2d 6321 . . . . . . . . . . 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 5883 . . . . . . . . . 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 730 . . . . . . . . . . 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 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
160157, 158, 159vdgr1d 25629 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U } >. } ) `  U )  =  2 )
161156, 160eqtrd 2463 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  2 )
162146, 161syl5breqr 4460 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =  U )  -> 
2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1
) ) ,  {
( P `  N
) ,  ( P `
 ( N  + 
1 ) ) }
>. } ) `  U
) )
163 dvds0 14317 . . . . . . . . . 10  |-  ( 2  e.  ZZ  ->  2  ||  0 )
164133, 163ax-mp 5 . . . . . . . . 9  |-  2  ||  0
165103ad2antrr 730 . . . . . . . . . 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 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  ->  U  e.  V )
168109ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  e.  V )
169 simpr 462 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =/=  U )
170116ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  e.  V )
171 simplr 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  N
)  =  ( P `
 ( N  + 
1 ) ) )
172171, 169eqnetrrd 2714 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( P `  ( N  +  1 ) )  =/=  U )
173165, 166, 167, 168, 169, 170, 172vdgr1a 25632 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =  ( P `  ( N  +  1
) ) )  /\  ( P `  N )  =/=  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  0 )
174164, 173syl5breqr 4460 . . . . . . . 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 2738 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  2  ||  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U ) )
176 dvdsadd2b 14346 . . . . . . 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 1268 . . . . . 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 10934 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  e.  CC )
179137nn0cnd 10934 . . . . . . . . 9  |-  ( ph  ->  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  e.  CC )
180178, 179addcomd 9842 . . . . . . . 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 4435 . . . . . . 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 466 . . . . . 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 256 . . . . 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 295 . . . 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 462 . . . . . . 7  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( P `  N )  =  ( P `  ( N  +  1 ) ) )
186185eqeq2d 2436 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  ( ( P `  0 )  =  ( P `  N )  <->  ( P `  0 )  =  ( P `  ( N  +  1 ) ) ) )
187185preq2d 4086 . . . . . 6  |-  ( (
ph  /\  ( P `  N )  =  ( P `  ( N  +  1 ) ) )  ->  { ( P `  0 ) ,  ( P `  N ) }  =  { ( P ` 
0 ) ,  ( P `  ( N  +  1 ) ) } )
188186, 187ifbieq2d 3936 . . . . 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 2492 . . . 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 286 . . 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 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =  U )
192191preq1d 4085 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1
) ) }  =  { U ,  ( P `
 ( N  + 
1 ) ) } )
193192opeq2d 4194 . . . . . . . . . . . 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 4010 . . . . . . . . . . 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 6321 . . . . . . . . . 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 5883 . . . . . . . . 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 730 . . . . . . . . . 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 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  e.  V )
200116ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  e.  V )
201 simplr 760 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )
202191, 201eqnetrrd 2714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
203202necomd 2691 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  ( P `  ( N  +  1 ) )  =/=  U )
204197, 198, 199, 200, 203vdgr1b 25630 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { U , 
( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
205196, 204eqtrd 2463 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  N )  =  U )  ->  (
( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `
 N ) ,  ( P `  ( N  +  1 ) ) } >. } ) `
 U )  =  1 )
206205oveq2d 6321 . . . . . . 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 4435 . . . . . 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 295 . . . . 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 10774 . . . . . . . . . . . 12  |-  2  e.  NN
210209a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  NN )
211 1lt2 10783 . . . . . . . . . . . 12  |-  1  <  2
212211a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  <  2 )
213 ndvdsp1 14389 . . . . . . . . . . 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 1264 . . . . . . . . . 10  |-  ( ph  ->  ( 2  ||  (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  ->  -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 ) ) )
215214con2d 118 . . . . . . . . 9  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  ->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U ) ) )
216 n2dvds1 14353 . . . . . . . . . . . 12  |-  -.  2  ||  1
217 opoe 14760 . . . . . . . . . . . 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 689 . . . . . . . . . . 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 435 . . . . . . . . . 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 17 . . . . . . . . 9  |-  ( ph  ->  ( -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  -> 
2  ||  ( (
( V VDeg  ( E  |`  ( F " (
1 ... N ) ) ) ) `  U
)  +  1 ) ) )
221215, 220impbid 193 . . . . . . . 8  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  -.  2  ||  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) ) )
222221, 131bitrd 256 . . . . . . 7  |-  ( ph  ->  ( 2  ||  (
( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U )  +  1 )  <->  U  e.  if ( ( P ` 
0 )  =  ( P `  N ) ,  (/) ,  { ( P `  0 ) ,  ( P `  N ) } ) ) )
223222notbid 295 . . . . . 6  |-  ( ph  ->  ( -.  2  ||  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  1 )  <->  -.  U  e.  if ( ( P `
 0 )  =  ( P `  N
) ,  (/) ,  {
( P `  0
) ,  ( P `
 N ) } ) ) )
224223ad2antrr 730 . . . . 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 5891 . . . . . . 7  |-  ( P `
 N )  e. 
_V
226225eupath2lem2 25704 . . . . . 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 718 . . . . 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 282 . . . 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 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  ( N  +  1 ) )  =  U )
230229preq2d 4086 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  { ( P `  N ) ,  ( P `  ( N  +  1 ) ) }  =  { ( P `  N ) ,  U } )
231230opeq2d 4194 . . . . . . . . . . . 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 4010 . . . . . . . . . . 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 6321 . . . . . . . . . 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 5883 . . . . . . . . 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 730 . . . . . . . . . 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 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  ->  U  e.  V )
238109ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  e.  V )
239 simplr 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  ( P `
 ( N  + 
1 ) ) )
240239, 229neeqtrd 2715 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( P `  N
)  =/=  U )
241235, 236, 237, 238, 240vdgr1c 25631 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  U } >. } ) `  U )  =  1 )
242234, 241eqtrd 2463 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  ( P `  ( N  +  1 ) )  =  U )  -> 
( ( V VDeg  { <. ( F `  ( N  +  1 ) ) ,  { ( P `  N ) ,  ( P `  ( N  +  1
) ) } >. } ) `  U )  =  1 )
243242oveq2d 6321 . . . . . . 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 4435 . . . . . 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 295 . . . . 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 730 . . . . 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 2689 . . . . . . . 8  |-  ( ( P `  N )  =/=  ( P `  ( N  +  1
) )  <->  ( P `  ( N  +  1 ) )  =/=  ( P `  N )
)
248 fvex 5891 . . . . . . . . 9  |-  ( P `
 ( N  + 
1 ) )  e. 
_V
249248eupath2lem2 25704 . . . . . . . 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 474 . . . . . . 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 331 . . . . . 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 718 . . . . 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 282 . . . 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 730 . . . . . . . . . 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 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  e.  V
)
257109ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  e.  V
)
258 simprl 762 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  N )  =/=  U
)
259116ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( P `  ( N  +  1
) )  e.  V
)
260 simprr 764 . . . . . . . . . 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 25632 . . . . . . . . 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 6321 . . . . . . . 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 9840 . . . . . . . . 9  |-  ( ph  ->  ( ( ( V VDeg  ( E  |`  ( F " ( 1 ... N ) ) ) ) `  U )  +  0 )  =  ( ( V VDeg  ( E  |`  ( F "
( 1 ... N
) ) ) ) `
 U ) )
264263ad2antrr 730 . . . . . . . 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 2463 . . . . . . 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 4435 . . . . . 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 295 . . . . 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 730 . . . . 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 2691 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  N )
)
270260necomd 2691 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  U  =/=  ( P `  ( N  +  1 ) ) )
271269, 2702thd 243 . . . . . . . . 9  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =/=  ( P `  N
)  <->  U  =/=  ( P `  ( N  +  1 ) ) ) )
272 neeq1 2701 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  N )  <->  ( P `  0 )  =/=  ( P `  N
) ) )
273 neeq1 2701 . . . . . . . . . 10  |-  ( U  =  ( P ` 
0 )  ->  ( U  =/=  ( P `  ( N  +  1
) )  <->  ( P `  0 )  =/=  ( P `  ( N  +  1 ) ) ) )
274272, 273bibi12d 322 . . . . . . . . 9  |-  ( U  =  ( P ` 
0 )  ->  (
( U  =/=  ( P `  N )  <->  U  =/=  ( P `  ( N  +  1
) ) )  <->  ( ( P `  0 )  =/=  ( P `  N
)  <->  ( P ` 
0 )  =/=  ( P `  ( N  +  1 ) ) ) ) )
275271, 274syl5ibcom 223 . . . . . . . 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 644 . . . . . . 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 2621 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  N ) )
278 biorf 406 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 N )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  N )  \/  U  =  ( P `  0 ) ) ) )
279277, 278syl 17 . . . . . . . . 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 388 . . . . . . . . 9  |-  ( ( U  =  ( P `
 N )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  N ) ) )
281279, 280syl6bb 264 . . . . . . . 8  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  ( U  =  ( P `  0
)  <->  ( U  =  ( P `  0
)  \/  U  =  ( P `  N
) ) ) )
282281anbi2d 708 . . . . . . 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 2621 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( P `  N )  =/=  ( P `  ( N  +  1 ) ) )  /\  (
( P `  N
)  =/=  U  /\  ( P `  ( N  +  1 ) )  =/=  U ) )  ->  -.  U  =  ( P `  ( N  +  1 ) ) )
284 biorf 406 . . . . . . . . . 10  |-  ( -.  U  =  ( P `
 ( N  + 
1 ) )  -> 
( U  =  ( P `  0 )  <-> 
( U  =  ( P `  ( N  +  1 ) )  \/  U  =  ( P `  0 ) ) ) )
285283, 284syl 17 . . . . . . . . 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 388 . . . . . . . . 9  |-  ( ( U  =  ( P `
 ( N  + 
1 ) )  \/  U  =  ( P `
 0 ) )  <-> 
( U  =  ( P `  0 )  \/  U  =  ( P `  ( N  +  1 ) ) ) )
287285, 286syl6bb 264 . . . . . . . 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 708 . . . . . . 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 286 . . . . . 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 25703 . . . . . . 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 17 . . . . . 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 25703 . . . . . . 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 17 . . . . . 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 288 . . . . 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 282 . . . 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 2739 . . 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 2738 . 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 256 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 187    \/ wo 369    /\ wa 370    = wceq 1437    e. wcel 1872    =/= wne 2614   {crab 2775   _Vcvv 3080    u. cun 3434    i^i cin 3435    C_ wss 3436   (/)c0 3761   ifcif 3911   {csn 3998   {cpr 4000   <.cop 4004   class class class wbr 4423   ran crn 4854    |` cres 4855   "cima 4856    Fn wfn 5596   -->wf 5597   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600   ` cfv 5601  (class class class)co 6305   Fincfn 7580   CCcc 9544   RRcr 9545   0cc0 9546   1c1 9547    + caddc 9549    < clt 9682    <_ cle 9683    - cmin 9867   NNcn 10616   2c2 10666   NN0cn0 10876   ZZcz 10944   ZZ>=cuz 11166   ...cfz 11791   #chash 12521    || cdvds 14304   UMGrph cumg 25037   VDeg cvdg 25619   EulPaths ceup 25688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1