Theorem eupath2lem3 25763

Description: Lemma for eupath2 25764. (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

Step	Hyp	Ref	Expression
1		imaundi 5270	. . . . . . . . . . 11 |- ( F " ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) )
2		1z 11001	. . . . . . . . . . . . 13 |- 1 e. ZZ
3		eupath2.5	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
4		nn0uz 11227	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
5		1m1e0 10711	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
6	5	fveq2i 5895	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
7	4, 6	eqtr4i 2487	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
8	3, 7	syl6eleq 2550	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
9		fzsuc2 11888	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
10	2, 8, 9	sylancr 674	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
11	10	imaeq2d 5190	. . . . . . . . . . 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 25754	. . . . . . . . . . . . . . 15 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
15	12, 13, 14	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
16		f1ofn 5842	. . . . . . . . . . . . . 14 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F Fn ( 1 ... ( # ` F ) ) )
17	15, 16	syl 17	. . . . . . . . . . . . 13 |- ( ph -> F Fn ( 1 ... ( # ` F ) ) )
18		eupath2.6	. . . . . . . . . . . . . 14 |- ( ph -> ( N + 1 ) <_ ( # ` F ) )
19		nn0p1nn 10943	. . . . . . . . . . . . . . . . 17 |- ( N e. NN0 -> ( N + 1 ) e. NN )
20	3, 19	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
21		nnuz 11228	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
22	20, 21	syl6eleq 2550	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
23		eupacl 25753	. . . . . . . . . . . . . . . . 17 |- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )
24	12, 23	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( # ` F ) e. NN0 )
25	24	nn0zd 11072	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` F ) e. ZZ )
26		elfz5 11827	. . . . . . . . . . . . . . 15 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
27	22, 25, 26	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
28	18, 27	mpbird 240	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ( 1 ... ( # ` F ) ) )
29		fnsnfv 5953	. . . . . . . . . . . . 13 |- ( ( F Fn ( 1 ... ( # ` F ) ) /\ ( N + 1 ) e. ( 1 ... ( # ` F ) ) ) -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
30	17, 28, 29	syl2anc 671	. . . . . . . . . . . 12 |- ( ph -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
31	30	uneq2d 3600	. . . . . . . . . . 11 |- ( ph -> ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) ) )
32	1, 11, 31	3eqtr4a 2522	. . . . . . . . . 10 |- ( ph -> ( F " ( 1 ... ( N + 1 ) ) ) = ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) )
33	32	reseq2d 5127	. . . . . . . . 9 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) )
34		resundi 5140	. . . . . . . . 9 |- ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) )
35	33, 34	syl6eq 2512	. . . . . . . 8 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) )
36		f1of 5841	. . . . . . . . . . . . 13 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) --> A )
37	15, 36	syl 17	. . . . . . . . . . . 12 |- ( ph -> F : ( 1 ... ( # ` F ) ) --> A )
38	37, 28	ffvelrnd 6051	. . . . . . . . . . 11 |- ( ph -> ( F ` ( N + 1 ) ) e. A )
39		fnressn 6105	. . . . . . . . . . 11 |- ( ( E Fn A /\ ( F ` ( N + 1 ) ) e. A ) -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } )
40	13, 38, 39	syl2anc 671	. . . . . . . . . 10 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } )
41		eupaseg 25757	. . . . . . . . . . . . . 14 |- ( ( F ( V EulPaths E ) P /\ ( N + 1 ) e. ( 1 ... ( # ` F ) ) ) -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } )
42	12, 28, 41	syl2anc 671	. . . . . . . . . . . . 13 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } )
43	3	nn0cnd 10961	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
44		ax-1cn 9628	. . . . . . . . . . . . . . . 16 |- 1 e. CC
45		pncan 9912	. . . . . . . . . . . . . . . 16 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
46	43, 44, 45	sylancl 673	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
47	46	fveq2d 5896	. . . . . . . . . . . . . 14 |- ( ph -> ( P ` ( ( N + 1 ) - 1 ) ) = ( P ` N ) )
48	47	preq1d 4070	. . . . . . . . . . . . 13 |- ( ph -> { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
49	42, 48	eqtrd 2496	. . . . . . . . . . . 12 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
50	49	opeq2d 4187	. . . . . . . . . . 11 |- ( ph -> <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. = <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. )
51	50	sneqd 3992	. . . . . . . . . 10 |- ( ph -> { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
52	40, 51	eqtrd 2496	. . . . . . . . 9 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
53	52	uneq2d 3600	. . . . . . . 8 |- ( ph -> ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
54	35, 53	eqtrd 2496	. . . . . . 7 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
55	54	oveq2d 6336	. . . . . 6 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) ) = ( V VDeg ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ) )
56	55	fveq1d 5894	. . . . 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 5201	. . . . . . . 8 |- ( F " ( 1 ... N ) ) C_ ran F
58		f1ofo 5848	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -onto-> A )
59		forn 5823	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -onto-> A -> ran F = A )
60	15, 58, 59	3syl 18	. . . . . . . 8 |- ( ph -> ran F = A )
61	57, 60	syl5sseq 3492	. . . . . . 7 |- ( ph -> ( F " ( 1 ... N ) ) C_ A )
62		fnssres 5715	. . . . . . 7 |- ( ( E Fn A /\ ( F " ( 1 ... N ) ) C_ A ) -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
63	13, 61, 62	syl2anc 671	. . . . . 6 |- ( ph -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
64		fvex 5902	. . . . . . . 8 |- ( F ` ( N + 1 ) ) e. _V
65		prex 4659	. . . . . . . 8 |- { ( P ` N ) , ( P ` ( N + 1 ) ) } e. _V
66	64, 65	fnsn 5658	. . . . . . 7 |- { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } Fn { ( F ` ( N + 1 ) ) }
67	66	a1i 11	. . . . . 6 |- ( ph -> { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } Fn { ( F ` ( N + 1 ) ) } )
68		eupafi 25755	. . . . . . . 8 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> A e. Fin )
69	12, 13, 68	syl2anc 671	. . . . . . 7 |- ( ph -> A e. Fin )
70		ssfi 7823	. . . . . . 7 |- ( ( A e. Fin /\ ( F " ( 1 ... N ) ) C_ A ) -> ( F " ( 1 ... N ) ) e. Fin )
71	69, 61, 70	syl2anc 671	. . . . . 6 |- ( ph -> ( F " ( 1 ... N ) ) e. Fin )
72		snfi 7681	. . . . . . 7 |- { ( F ` ( N + 1 ) ) } e. Fin
73	72	a1i 11	. . . . . 6 |- ( ph -> { ( F ` ( N + 1 ) ) } e. Fin )
74	3	nn0red 10960	. . . . . . . . . 10 |- ( ph -> N e. RR )
75	74	ltp1d 10570	. . . . . . . . 9 |- ( ph -> N < ( N + 1 ) )
76		peano2re 9837	. . . . . . . . . . 11 |- ( N e. RR -> ( N + 1 ) e. RR )
77	74, 76	syl 17	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. RR )
78	74, 77	ltnled 9813	. . . . . . . . 9 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79	75, 78	mpbid 215	. . . . . . . 8 |- ( ph -> -. ( N + 1 ) <_ N )
80		f1of1 5840	. . . . . . . . . . 11 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -1-1-> A )
81	15, 80	syl 17	. . . . . . . . . 10 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-> A )
82	3	nn0zd 11072	. . . . . . . . . . . 12 |- ( ph -> N e. ZZ )
83	82	peano2zd 11077	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
84		eluz2 11199	. . . . . . . . . . . . 13 |- ( ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( N + 1 ) <_ ( # ` F ) ) )
85	83, 25, 18, 84	syl3anbrc 1198	. . . . . . . . . . . 12 |- ( ph -> ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) )
86		peano2uzr 11248	. . . . . . . . . . . 12 |- ( ( N e. ZZ /\ ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
87	82, 85, 86	syl2anc 671	. . . . . . . . . . 11 |- ( ph -> ( # ` F ) e. ( ZZ>= ` N ) )
88		fzss2 11873	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
89	87, 88	syl 17	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
90		f1elima 6194	. . . . . . . . . 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 ) ) )
91	81, 28, 89, 90	syl3anc 1276	. . . . . . . . 9 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) e. ( 1 ... N ) ) )
92		elfz5 11827	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
93	22, 82, 92	syl2anc 671	. . . . . . . . 9 |- ( ph -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
94	91, 93	bitrd 261	. . . . . . . 8 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) <_ N ) )
95	79, 94	mtbird 307	. . . . . . 7 |- ( ph -> -. ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) )
96		disjsn 4044	. . . . . . 7 |- ( ( ( F " ( 1 ... N ) ) i^i { ( F ` ( N + 1 ) ) } ) = (/) <-> -. ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) )
97	95, 96	sylibr 217	. . . . . 6 |- ( ph -> ( ( F " ( 1 ... N ) ) i^i { ( F ` ( N + 1 ) ) } ) = (/) )
98		eupagra 25750	. . . . . . 7 |- ( F ( V EulPaths E ) P -> V UMGrph E )
99		umgrares 25107	. . . . . . 7 |- ( V UMGrph E -> V UMGrph ( E |` ( F " ( 1 ... N ) ) ) )
100	12, 98, 99	3syl 18	. . . . . 6 |- ( ph -> V UMGrph ( E |` ( F " ( 1 ... N ) ) ) )
101		relumgra 25097	. . . . . . . . 9 |- Rel UMGrph
102	101	brrelexi 4897	. . . . . . . 8 |- ( V UMGrph E -> V e. _V )
103	12, 98, 102	3syl 18	. . . . . . 7 |- ( ph -> V e. _V )
104		eupapf 25756	. . . . . . . . 9 |- ( F ( V EulPaths E ) P -> P : ( 0 ... ( # ` F ) ) --> V )
105	12, 104	syl 17	. . . . . . . 8 |- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
106	3, 4	syl6eleq 2550	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` 0 ) )
107		elfzuzb 11829	. . . . . . . . 9 |- ( N e. ( 0 ... ( # ` F ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ( ZZ>= ` N ) ) )
108	106, 87, 107	sylanbrc 675	. . . . . . . 8 |- ( ph -> N e. ( 0 ... ( # ` F ) ) )
109	105, 108	ffvelrnd 6051	. . . . . . 7 |- ( ph -> ( P ` N ) e. V )
110		peano2nn0 10944	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
111	3, 110	syl 17	. . . . . . . . . . 11 |- ( ph -> ( N + 1 ) e. NN0 )
112	111, 4	syl6eleq 2550	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
113		elfz5 11827	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
114	112, 25, 113	syl2anc 671	. . . . . . . . 9 |- ( ph -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
115	18, 114	mpbird 240	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ( 0 ... ( # ` F ) ) )
116	105, 115	ffvelrnd 6051	. . . . . . 7 |- ( ph -> ( P ` ( N + 1 ) ) e. V )
117		umgra1 25109	. . . . . . 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 ) ) } >. } )
118	103, 38, 109, 116, 117	syl22anc 1277	. . . . . 6 |- ( ph -> V UMGrph { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
119		eupath2.7	. . . . . 6 |- ( ph -> U e. V )
120	63, 67, 71, 73, 97, 100, 118, 119	vdgrfiun 25686	. . . . 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 ) ) )
121	56, 120	eqtrd 2496	. . . 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 ) ) )
122	121	breq2d 4430	. . 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 ) ) ) )
123	122	notbid 300	. 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 5892	. . . . . . . . . 10 |- ( x = U -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
125	124	breq2d 4430	. . . . . . . . 9 |- ( x = U -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
126	125	notbid 300	. . . . . . . 8 |- ( x = U -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
127	126	elrab3 3209	. . . . . . 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 ) ) )
128	119, 127	syl 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 ) } ) )
130	129	eleq2d 2525	. . . . . 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 ) } ) ) )
131	128, 130	bitr3d 263	. . . . 5 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
132	131	adantr 471	. . . 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 11003	. . . . . . . 8 |- 2 e. ZZ
134	133	a1i 11	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
135		vdgrfif 25683	. . . . . . . . . . 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 )
136	103, 63, 71, 135	syl3anc 1276	. . . . . . . . . 10 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
137	136, 119	ffvelrnd 6051	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. NN0 )
138	137	nn0zd 11072	. . . . . . . 8 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
139	138	adantr 471	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
140		vdgrfif 25683	. . . . . . . . . . 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 )
141	103, 67, 73, 140	syl3anc 1276	. . . . . . . . . 10 |- ( ph -> ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) : V --> NN0 )
142	141, 119	ffvelrnd 6051	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. NN0 )
143	142	nn0zd 11072	. . . . . . . 8 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
144	143	adantr 471	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
145		iddvds 14371	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 2 )
146	133, 145	ax-mp 5	. . . . . . . . 9 |- 2 || 2
147		simpr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
148		simplr 767	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
149	148, 147	eqtr3d 2498	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) = U )
150	147, 149	preq12d 4072	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , U } )
151		dfsn2 3993	. . . . . . . . . . . . . . 15 |- { U } = { U , U }
152	150, 151	syl6eqr 2514	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U } )
153	152	opeq2d 4187	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. = <. ( F ` ( N + 1 ) ) , { U } >. )
154	153	sneqd 3992	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } = { <. ( F ` ( N + 1 ) ) , { U } >. } )
155	154	oveq2d 6336	. . . . . . . . . . 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 } >. } ) )
156	155	fveq1d 5894	. . . . . . . . . 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 ) )
157	103	ad2antrr 737	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> V e. _V )
158	64	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( F ` ( N + 1 ) ) e. _V )
159	119	ad2antrr 737	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
160	157, 158, 159	vdgr1d 25687	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U } >. } ) ` U ) = 2 )
161	156, 160	eqtrd 2496	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) = 2 )
162	146, 161	syl5breqr 4455	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
163		dvds0 14373	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 0 )
164	133, 163	ax-mp 5	. . . . . . . . 9 |- 2 || 0
165	103	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> V e. _V )
166	64	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( F ` ( N + 1 ) ) e. _V )
167	119	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> U e. V )
168	109	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) e. V )
169		simpr 467	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) =/= U )
170	116	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) e. V )
171		simplr 767	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
172	171, 169	eqnetrrd 2704	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) =/= U )
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 25690	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) = 0 )
174	164, 173	syl5breqr 4455	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
175	162, 174	pm2.61dane 2723	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
176		dvdsadd2b 14402	. . . . . . 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 ) ) ) )
177	134, 139, 144, 175, 176	syl112anc 1280	. . . . . 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 ) ) ) )
178	142	nn0cnd 10961	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. CC )
179	137	nn0cnd 10961	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. CC )
180	178, 179	addcomd 9866	. . . . . . . 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 ) ) )
181	180	breq2d 4430	. . . . . . 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 ) ) ) )
182	181	adantr 471	. . . . . 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 ) ) ) )
183	177, 182	bitrd 261	. . . . 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 ) ) ) )
184	183	notbid 300	. . . 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 467	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
186	185	eqeq2d 2472	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
187	185	preq2d 4071	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
188	186, 187	ifbieq2d 3918	. . . . 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 ) ) } ) )
189	188	eleq2d 2525	. . . 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 ) ) } ) ) )
190	132, 184, 189	3bitr3d 291	. . 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 467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
192	191	preq1d 4070	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
193	192	opeq2d 4187	. . . . . . . . . . . 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 ) ) } >. )
194	193	sneqd 3992	. . . . . . . . . . 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 ) ) } >. } )
195	194	oveq2d 6336	. . . . . . . . . 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 ) ) } >. } ) )
196	195	fveq1d 5894	. . . . . . . . 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 ) )
197	103	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> V e. _V )
198	64	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( F ` ( N + 1 ) ) e. _V )
199	119	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
200	116	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) e. V )
201		simplr 767	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
202	191, 201	eqnetrrd 2704	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
203	202	necomd 2691	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) =/= U )
204	197, 198, 199, 200, 203	vdgr1b 25688	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U , ( P ` ( N + 1 ) ) } >. } ) ` U ) = 1 )
205	196, 204	eqtrd 2496	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) = 1 )
206	205	oveq2d 6336	. . . . . . 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 ) )
207	206	breq2d 4430	. . . . . 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 ) ) )
208	207	notbid 300	. . . . 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 10801	. . . . . . . . . . . 12 |- 2 e. NN
210	209	a1i 11	. . . . . . . . . . 11 |- ( ph -> 2 e. NN )
211		1lt2 10810	. . . . . . . . . . . 12 |- 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 < 2 )
213		ndvdsp1 14445	. . . . . . . . . . 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 ) ) )
214	138, 210, 212, 213	syl3anc 1276	. . . . . . . . . 10 |- ( ph -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) -> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
215	214	con2d 120	. . . . . . . . 9 |- ( ph -> ( 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) -> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
216		n2dvds1 14409	. . . . . . . . . . . 12 |- -. 2 || 1
217		opoe 14816	. . . . . . . . . . . 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 ) )
218	2, 216, 217	mpanr12 696	. . . . . . . . . . 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 ) )
219	218	ex 440	. . . . . . . . . 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 ) ) )
220	138, 219	syl 17	. . . . . . . . 9 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) -> 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
221	215, 220	impbid 195	. . . . . . . 8 |- ( ph -> ( 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
222	221, 131	bitrd 261	. . . . . . 7 |- ( ph -> ( 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
223	222	notbid 300	. . . . . 6 |- ( ph -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) <-> -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
224	223	ad2antrr 737	. . . . 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 5902	. . . . . . 7 |- ( P ` N ) e. _V
226	225	eupath2lem2 25762	. . . . . 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 ) ) } ) ) )
227	226	adantll 725	. . . . 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 ) ) } ) ) )
228	208, 224, 227	3bitrd 287	. . . 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 467	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` ( N + 1 ) ) = U )
230	229	preq2d 4071	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
231	230	opeq2d 4187	. . . . . . . . . . . 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 } >. )
232	231	sneqd 3992	. . . . . . . . . . 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 } >. } )
233	232	oveq2d 6336	. . . . . . . . . 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 } >. } ) )
234	233	fveq1d 5894	. . . . . . . . 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 ) )
235	103	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> V e. _V )
236	64	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( F ` ( N + 1 ) ) e. _V )
237	119	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> U e. V )
238	109	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) e. V )
239		simplr 767	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
240	239, 229	neeqtrd 2705	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
241	235, 236, 237, 238, 240	vdgr1c 25689	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , U } >. } ) ` U ) = 1 )
242	234, 241	eqtrd 2496	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) = 1 )
243	242	oveq2d 6336	. . . . . . 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 ) )
244	243	breq2d 4430	. . . . . 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 ) ) )
245	244	notbid 300	. . . . 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 ) ) )
246	223	ad2antrr 737	. . . . 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 5902	. . . . . . . . 9 |- ( P ` ( N + 1 ) ) e. _V
249	248	eupath2lem2 25762	. . . . . . . 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 ) } ) ) )
250	247, 249	sylanb 479	. . . . . . 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 ) } ) ) )
251	250	con1bid 336	. . . . . 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 ) ) } ) ) )
252	251	adantll 725	. . . . 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 ) ) } ) ) )
253	245, 246, 252	3bitrd 287	. . . 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 ) ) } ) ) )
254	103	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> V e. _V )
255	64	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( F ` ( N + 1 ) ) e. _V )
256	119	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U e. V )
257	109	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) e. V )
258		simprl 769	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) =/= U )
259	116	ad2antrr 737	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` ( N + 1 ) ) e. V )
260		simprr 771	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` ( N + 1 ) ) =/= U )
261	254, 255, 256, 257, 258, 259, 260	vdgr1a 25690	. . . . . . . . 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 )
262	261	oveq2d 6336	. . . . . . . 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 ) )
263	179	addid1d 9864	. . . . . . . . 9 |- ( ph -> ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 0 ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
264	263	ad2antrr 737	. . . . . . . 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 ) )
265	262, 264	eqtrd 2496	. . . . . . 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 ) )
266	265	breq2d 4430	. . . . . 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 ) ) )
267	266	notbid 300	. . . . 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 ) ) )
268	131	ad2antrr 737	. . . . 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 ) } ) ) )
269	258	necomd 2691	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` N ) )
270	260	necomd 2691	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` ( N + 1 ) ) )
271	269, 270	2thd 248	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) )
272		neeq1 2698	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
273		neeq1 2698	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` ( N + 1 ) ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) )
274	272, 273	bibi12d 327	. . . . . . . . 9 |- ( U = ( P ` 0 ) -> ( ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) <-> ( ( P ` 0 ) =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) ) )
275	271, 274	syl5ibcom 228	. . . . . . . 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 ) ) ) ) )
276	275	pm5.32rd 650	. . . . . . 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 ) ) ) )
277	269	neneqd 2640	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` N ) )
278		biorf 411	. . . . . . . . . 10 |- ( -. U = ( P ` N ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` N ) \/ U = ( P ` 0 ) ) ) )
279	277, 278	syl 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 393	. . . . . . . . 9 |- ( ( U = ( P ` N ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) )
281	279, 280	syl6bb 269	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) )
282	281	anbi2d 715	. . . . . . 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 ) ) ) ) )
283	270	neneqd 2640	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` ( N + 1 ) ) )
284		biorf 411	. . . . . . . . . 10 |- ( -. U = ( P ` ( N + 1 ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) ) )
285	283, 284	syl 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 393	. . . . . . . . 9 |- ( ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) )
287	285, 286	syl6bb 269	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) )
288	287	anbi2d 715	. . . . . . 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 ) ) ) ) ) )
289	276, 282, 288	3bitr3d 291	. . . . . 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 25761	. . . . . . 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 ) ) ) ) )
291	256, 290	syl 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 25761	. . . . . . 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 ) ) ) ) ) )
293	256, 292	syl 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 ) ) ) ) ) )
294	289, 291, 293	3bitr4d 293	. . . . 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 ) ) } ) ) )
295	267, 268, 294	3bitrd 287	. . . 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 ) ) } ) ) )
296	228, 253, 295	pm2.61da2ne 2724	. . 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 ) ) } ) ) )
297	190, 296	pm2.61dane 2723	. 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 ) ) } ) ) )
298	123, 297	bitrd 261	1 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   = wceq 1455   e. wcel 1898   =/= wne 2633   {crab 2753   _Vcvv 3057   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3743   ifcif 3893   {csn 3980   {cpr 3982   <.cop 3986   class class class wbr 4418   ran crn 4857   |` cres 4858   "cima 4859   Fn wfn 5600   -->wf 5601   -1-1->wf1 5602   -onto->wfo 5603   -1-1-onto->wf1o 5604   ` cfv 5605  (class class class)co 6320   Fincfn 7600   CCcc 9568   RRcr 9569   0cc0 9570   1c1 9571   + caddc 9573   < clt 9706   <_ cle 9707   - cmin 9891   NNcn 10642   2c2 10692   NN0cn0 10903   ZZcz 10971   ZZ>=cuz 11193   ...cfz 11819   #chash 12553   || cdvds 14360   UMGrph cumg 25095   VDeg cvdg 25677   EulPaths ceup 25746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr