Theorem eupath2lem3 25396

Description: Lemma for eupath2 25397. (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 5236	. . . . . . . . . . 11 |- ( F " ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) )
2		1z 10935	. . . . . . . . . . . . 13 |- 1 e. ZZ
3		eupath2.5	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
4		nn0uz 11161	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
5		1m1e0 10645	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
6	5	fveq2i 5852	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
7	4, 6	eqtr4i 2434	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
8	3, 7	syl6eleq 2500	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
9		fzsuc2 11792	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
10	2, 8, 9	sylancr 661	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
11	10	imaeq2d 5157	. . . . . . . . . . 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 25387	. . . . . . . . . . . . . . 15 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
15	12, 13, 14	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
16		f1ofn 5800	. . . . . . . . . . . . . 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 10876	. . . . . . . . . . . . . . . . 17 |- ( N e. NN0 -> ( N + 1 ) e. NN )
20	3, 19	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
21		nnuz 11162	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
22	20, 21	syl6eleq 2500	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
23		eupacl 25386	. . . . . . . . . . . . . . . . 17 |- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )
24	12, 23	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> ( # ` F ) e. NN0 )
25	24	nn0zd 11006	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` F ) e. ZZ )
26		elfz5 11734	. . . . . . . . . . . . . . 15 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
27	22, 25, 26	syl2anc 659	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
28	18, 27	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ( 1 ... ( # ` F ) ) )
29		fnsnfv 5909	. . . . . . . . . . . . 13 |- ( ( F Fn ( 1 ... ( # ` F ) ) /\ ( N + 1 ) e. ( 1 ... ( # ` F ) ) ) -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
30	17, 28, 29	syl2anc 659	. . . . . . . . . . . 12 |- ( ph -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
31	30	uneq2d 3597	. . . . . . . . . . 11 |- ( ph -> ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) ) )
32	1, 11, 31	3eqtr4a 2469	. . . . . . . . . 10 |- ( ph -> ( F " ( 1 ... ( N + 1 ) ) ) = ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) )
33	32	reseq2d 5094	. . . . . . . . 9 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) )
34		resundi 5107	. . . . . . . . 9 |- ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) )
35	33, 34	syl6eq 2459	. . . . . . . 8 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) )
36		f1of 5799	. . . . . . . . . . . . 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 6010	. . . . . . . . . . 11 |- ( ph -> ( F ` ( N + 1 ) ) e. A )
39		fnressn 6063	. . . . . . . . . . 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 659	. . . . . . . . . 10 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } )
41		eupaseg 25390	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 13 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } )
43	3	nn0cnd 10895	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
44		ax-1cn 9580	. . . . . . . . . . . . . . . 16 |- 1 e. CC
45		pncan 9862	. . . . . . . . . . . . . . . 16 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
46	43, 44, 45	sylancl 660	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
47	46	fveq2d 5853	. . . . . . . . . . . . . 14 |- ( ph -> ( P ` ( ( N + 1 ) - 1 ) ) = ( P ` N ) )
48	47	preq1d 4057	. . . . . . . . . . . . 13 |- ( ph -> { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
49	42, 48	eqtrd 2443	. . . . . . . . . . . 12 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
50	49	opeq2d 4166	. . . . . . . . . . 11 |- ( ph -> <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. = <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. )
51	50	sneqd 3984	. . . . . . . . . 10 |- ( ph -> { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
52	40, 51	eqtrd 2443	. . . . . . . . 9 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
53	52	uneq2d 3597	. . . . . . . 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 2443	. . . . . . 7 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
55	54	oveq2d 6294	. . . . . 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 5851	. . . . 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 5168	. . . . . . . 8 |- ( F " ( 1 ... N ) ) C_ ran F
58		f1ofo 5806	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -onto-> A )
59		forn 5781	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -onto-> A -> ran F = A )
60	15, 58, 59	3syl 18	. . . . . . . 8 |- ( ph -> ran F = A )
61	57, 60	syl5sseq 3490	. . . . . . 7 |- ( ph -> ( F " ( 1 ... N ) ) C_ A )
62		fnssres 5675	. . . . . . 7 |- ( ( E Fn A /\ ( F " ( 1 ... N ) ) C_ A ) -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
63	13, 61, 62	syl2anc 659	. . . . . 6 |- ( ph -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
64		fvex 5859	. . . . . . . 8 |- ( F ` ( N + 1 ) ) e. _V
65		prex 4633	. . . . . . . 8 |- { ( P ` N ) , ( P ` ( N + 1 ) ) } e. _V
66	64, 65	fnsn 5622	. . . . . . 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 25388	. . . . . . . 8 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> A e. Fin )
69	12, 13, 68	syl2anc 659	. . . . . . 7 |- ( ph -> A e. Fin )
70		ssfi 7775	. . . . . . 7 |- ( ( A e. Fin /\ ( F " ( 1 ... N ) ) C_ A ) -> ( F " ( 1 ... N ) ) e. Fin )
71	69, 61, 70	syl2anc 659	. . . . . 6 |- ( ph -> ( F " ( 1 ... N ) ) e. Fin )
72		snfi 7634	. . . . . . 7 |- { ( F ` ( N + 1 ) ) } e. Fin
73	72	a1i 11	. . . . . 6 |- ( ph -> { ( F ` ( N + 1 ) ) } e. Fin )
74	3	nn0red 10894	. . . . . . . . . 10 |- ( ph -> N e. RR )
75	74	ltp1d 10516	. . . . . . . . 9 |- ( ph -> N < ( N + 1 ) )
76		peano2re 9787	. . . . . . . . . . 11 |- ( N e. RR -> ( N + 1 ) e. RR )
77	74, 76	syl 17	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. RR )
78	74, 77	ltnled 9764	. . . . . . . . 9 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79	75, 78	mpbid 210	. . . . . . . 8 |- ( ph -> -. ( N + 1 ) <_ N )
80		f1of1 5798	. . . . . . . . . . 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 11006	. . . . . . . . . . . 12 |- ( ph -> N e. ZZ )
83	82	peano2zd 11011	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
84		eluz2 11133	. . . . . . . . . . . . 13 |- ( ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( N + 1 ) <_ ( # ` F ) ) )
85	83, 25, 18, 84	syl3anbrc 1181	. . . . . . . . . . . 12 |- ( ph -> ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) )
86		peano2uzr 11182	. . . . . . . . . . . 12 |- ( ( N e. ZZ /\ ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
87	82, 85, 86	syl2anc 659	. . . . . . . . . . 11 |- ( ph -> ( # ` F ) e. ( ZZ>= ` N ) )
88		fzss2 11778	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
89	87, 88	syl 17	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
90		f1elima 6152	. . . . . . . . . 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 1230	. . . . . . . . 9 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) e. ( 1 ... N ) ) )
92		elfz5 11734	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
93	22, 82, 92	syl2anc 659	. . . . . . . . 9 |- ( ph -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
94	91, 93	bitrd 253	. . . . . . . 8 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) <_ N ) )
95	79, 94	mtbird 299	. . . . . . 7 |- ( ph -> -. ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) )
96		disjsn 4032	. . . . . . 7 |- ( ( ( F " ( 1 ... N ) ) i^i { ( F ` ( N + 1 ) ) } ) = (/) <-> -. ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) )
97	95, 96	sylibr 212	. . . . . 6 |- ( ph -> ( ( F " ( 1 ... N ) ) i^i { ( F ` ( N + 1 ) ) } ) = (/) )
98		eupagra 25383	. . . . . . 7 |- ( F ( V EulPaths E ) P -> V UMGrph E )
99		umgrares 24741	. . . . . . 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 24731	. . . . . . . . 9 |- Rel UMGrph
102	101	brrelexi 4864	. . . . . . . 8 |- ( V UMGrph E -> V e. _V )
103	12, 98, 102	3syl 18	. . . . . . 7 |- ( ph -> V e. _V )
104		eupapf 25389	. . . . . . . . 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 2500	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` 0 ) )
107		elfzuzb 11736	. . . . . . . . 9 |- ( N e. ( 0 ... ( # ` F ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ( ZZ>= ` N ) ) )
108	106, 87, 107	sylanbrc 662	. . . . . . . 8 |- ( ph -> N e. ( 0 ... ( # ` F ) ) )
109	105, 108	ffvelrnd 6010	. . . . . . 7 |- ( ph -> ( P ` N ) e. V )
110		peano2nn0 10877	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
111	3, 110	syl 17	. . . . . . . . . . 11 |- ( ph -> ( N + 1 ) e. NN0 )
112	111, 4	syl6eleq 2500	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
113		elfz5 11734	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
114	112, 25, 113	syl2anc 659	. . . . . . . . 9 |- ( ph -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
115	18, 114	mpbird 232	. . . . . . . 8 |- ( ph -> ( N + 1 ) e. ( 0 ... ( # ` F ) ) )
116	105, 115	ffvelrnd 6010	. . . . . . 7 |- ( ph -> ( P ` ( N + 1 ) ) e. V )
117		umgra1 24743	. . . . . . 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 1231	. . . . . 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 25319	. . . . 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 2443	. . . 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 4407	. . 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 292	. 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 5849	. . . . . . . . . 10 |- ( x = U -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
125	124	breq2d 4407	. . . . . . . . 9 |- ( x = U -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
126	125	notbid 292	. . . . . . . 8 |- ( x = U -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
127	126	elrab3 3208	. . . . . . 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 2472	. . . . . 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 255	. . . . 5 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) )
132	131	adantr 463	. . . 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 10937	. . . . . . . 8 |- 2 e. ZZ
134	133	a1i 11	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
135		vdgrfif 25316	. . . . . . . . . . 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 1230	. . . . . . . . . 10 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
137	136, 119	ffvelrnd 6010	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. NN0 )
138	137	nn0zd 11006	. . . . . . . 8 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
139	138	adantr 463	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
140		vdgrfif 25316	. . . . . . . . . . 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 1230	. . . . . . . . . 10 |- ( ph -> ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) : V --> NN0 )
142	141, 119	ffvelrnd 6010	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. NN0 )
143	142	nn0zd 11006	. . . . . . . 8 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
144	143	adantr 463	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
145		iddvds 14206	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 2 )
146	133, 145	ax-mp 5	. . . . . . . . 9 |- 2 || 2
147		simpr 459	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
148		simplr 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
149	148, 147	eqtr3d 2445	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) = U )
150	147, 149	preq12d 4059	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , U } )
151		dfsn2 3985	. . . . . . . . . . . . . . 15 |- { U } = { U , U }
152	150, 151	syl6eqr 2461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U } )
153	152	opeq2d 4166	. . . . . . . . . . . . 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 3984	. . . . . . . . . . . 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 6294	. . . . . . . . . . 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 5851	. . . . . . . . . 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 724	. . . . . . . . . . 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 724	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
160	157, 158, 159	vdgr1d 25320	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U } >. } ) ` U ) = 2 )
161	156, 160	eqtrd 2443	. . . . . . . . 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 4431	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
163		dvds0 14208	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 0 )
164	133, 163	ax-mp 5	. . . . . . . . 9 |- 2 || 0
165	103	ad2antrr 724	. . . . . . . . . 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 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> U e. V )
168	109	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) e. V )
169		simpr 459	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) =/= U )
170	116	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) e. V )
171		simplr 754	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
172	171, 169	eqnetrrd 2697	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) =/= U )
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 25323	. . . . . . . . 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 4431	. . . . . . . 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 2721	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
176		dvdsadd2b 14237	. . . . . . 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 1234	. . . . . 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 10895	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. CC )
179	137	nn0cnd 10895	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. CC )
180	178, 179	addcomd 9816	. . . . . . . 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 4407	. . . . . . 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 463	. . . . . 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 253	. . . . 5 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) <-> 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) ) )
184	183	notbid 292	. . . 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 459	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
186	185	eqeq2d 2416	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
187	185	preq2d 4058	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
188	186, 187	ifbieq2d 3910	. . . . 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 2472	. . . 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 283	. . 3 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
191		simpr 459	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
192	191	preq1d 4057	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
193	192	opeq2d 4166	. . . . . . . . . . . 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 3984	. . . . . . . . . . 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 6294	. . . . . . . . . 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 5851	. . . . . . . . 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 724	. . . . . . . . . 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 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
200	116	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) e. V )
201		simplr 754	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
202	191, 201	eqnetrrd 2697	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
203	202	necomd 2674	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) =/= U )
204	197, 198, 199, 200, 203	vdgr1b 25321	. . . . . . . . 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 2443	. . . . . . . 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 6294	. . . . . . 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 4407	. . . . . 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 292	. . . . 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 10734	. . . . . . . . . . . 12 |- 2 e. NN
210	209	a1i 11	. . . . . . . . . . 11 |- ( ph -> 2 e. NN )
211		1lt2 10743	. . . . . . . . . . . 12 |- 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 < 2 )
213		ndvdsp1 14276	. . . . . . . . . . 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 1230	. . . . . . . . . 10 |- ( ph -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) -> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
215	214	con2d 115	. . . . . . . . 9 |- ( ph -> ( 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) -> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
216		n2dvds1 14244	. . . . . . . . . . . 12 |- -. 2 || 1
217		opoe 14544	. . . . . . . . . . . 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 683	. . . . . . . . . . 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 432	. . . . . . . . . 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 190	. . . . . . . 8 |- ( ph -> ( 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
222	221, 131	bitrd 253	. . . . . . 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 292	. . . . . 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 724	. . . . 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 5859	. . . . . . 7 |- ( P ` N ) e. _V
226	225	eupath2lem2 25395	. . . . . 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 712	. . . . 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 279	. . . 4 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
229		simpr 459	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` ( N + 1 ) ) = U )
230	229	preq2d 4058	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
231	230	opeq2d 4166	. . . . . . . . . . . 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 3984	. . . . . . . . . . 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 6294	. . . . . . . . . 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 5851	. . . . . . . . 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 724	. . . . . . . . . 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 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> U e. V )
238	109	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) e. V )
239		simplr 754	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
240	239, 229	neeqtrd 2698	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
241	235, 236, 237, 238, 240	vdgr1c 25322	. . . . . . . . 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 2443	. . . . . . . 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 6294	. . . . . . 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 4407	. . . . . 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 292	. . . . 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 724	. . . . 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 2672	. . . . . . . 8 |- ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` ( N + 1 ) ) =/= ( P ` N ) )
248		fvex 5859	. . . . . . . . 9 |- ( P ` ( N + 1 ) ) e. _V
249	248	eupath2lem2 25395	. . . . . . . 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 470	. . . . . . 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 328	. . . . . 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 712	. . . . 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 279	. . . 4 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
254	103	ad2antrr 724	. . . . . . . . . 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 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U e. V )
257	109	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) e. V )
258		simprl 756	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) =/= U )
259	116	ad2antrr 724	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` ( N + 1 ) ) e. V )
260		simprr 758	. . . . . . . . . 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 25323	. . . . . . . . 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 6294	. . . . . . . 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 9814	. . . . . . . . 9 |- ( ph -> ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 0 ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
264	263	ad2antrr 724	. . . . . . . 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 2443	. . . . . . 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 4407	. . . . . 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 292	. . . . 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 724	. . . . 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 2674	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` N ) )
270	260	necomd 2674	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` ( N + 1 ) ) )
271	269, 270	2thd 240	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) )
272		neeq1 2684	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
273		neeq1 2684	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` ( N + 1 ) ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) )
274	272, 273	bibi12d 319	. . . . . . . . 9 |- ( U = ( P ` 0 ) -> ( ( U =/= ( P ` N ) <-> U =/= ( P ` ( N + 1 ) ) ) <-> ( ( P ` 0 ) =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) ) )
275	271, 274	syl5ibcom 220	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) -> ( ( P ` 0 ) =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) ) )
276	275	pm5.32rd 638	. . . . . . 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 2605	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` N ) )
278		biorf 403	. . . . . . . . . 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 385	. . . . . . . . 9 |- ( ( U = ( P ` N ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) )
281	279, 280	syl6bb 261	. . . . . . . 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 702	. . . . . . 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 2605	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` ( N + 1 ) ) )
284		biorf 403	. . . . . . . . . 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 385	. . . . . . . . 9 |- ( ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) )
287	285, 286	syl6bb 261	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) )
288	287	anbi2d 702	. . . . . . 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 283	. . . . . 6 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
290		eupath2lem1 25394	. . . . . . 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 25394	. . . . . . 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 285	. . . . 5 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
295	267, 268, 294	3bitrd 279	. . . 4 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
296	228, 253, 295	pm2.61da2ne 2722	. . 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 2721	. 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 253	1 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 366   /\ wa 367   = wceq 1405   e. wcel 1842   =/= wne 2598   {crab 2758   _Vcvv 3059   u. cun 3412   i^i cin 3413   C_ wss 3414   (/)c0 3738   ifcif 3885   {csn 3972   {cpr 3974   <.cop 3978   class class class wbr 4395   ran crn 4824   |` cres 4825   "cima 4826   Fn wfn 5564   -->wf 5565   -1-1->wf1 5566   -onto->wfo 5567   -1-1-onto->wf1o 5568   ` cfv 5569  (class class class)co 6278   Fincfn 7554   CCcc 9520   RRcr 9521   0cc0 9522   1c1 9523   + caddc 9525   < clt 9658   <_ cle 9659   - cmin 9841   NNcn 10576   2c2 10626   NN0cn0 10836   ZZcz 10905   ZZ>=cuz 11127   ...cfz 11726   #chash 12452   || cdvds 14195   UMGrph cumg 24729   VDeg cvdg 25310   EulPaths ceup 25379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 95