Theorem eupath2lem3 23612

Description: Lemma for eupath2 23613. (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 5261	. . . . . . . . . . 11 |- ( F " ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) )
2		1z 10688	. . . . . . . . . . . . 13 |- 1 e. ZZ
3		eupath2.5	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
4		nn0uz 10907	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
5		1m1e0 10402	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
6	5	fveq2i 5706	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
7	4, 6	eqtr4i 2466	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
8	3, 7	syl6eleq 2533	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
9		fzsuc2 11526	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
10	2, 8, 9	sylancr 663	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
11	10	imaeq2d 5181	. . . . . . . . . . 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 23603	. . . . . . . . . . . . . . 15 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
15	12, 13, 14	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
16		f1ofn 5654	. . . . . . . . . . . . . 14 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F Fn ( 1 ... ( # ` F ) ) )
17	15, 16	syl 16	. . . . . . . . . . . . 13 |- ( ph -> F Fn ( 1 ... ( # ` F ) ) )
18		eupath2.6	. . . . . . . . . . . . . 14 |- ( ph -> ( N + 1 ) <_ ( # ` F ) )
19		nn0p1nn 10631	. . . . . . . . . . . . . . . . 17 |- ( N e. NN0 -> ( N + 1 ) e. NN )
20	3, 19	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
21		nnuz 10908	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
22	20, 21	syl6eleq 2533	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
23		eupacl 23602	. . . . . . . . . . . . . . . . 17 |- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )
24	12, 23	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( # ` F ) e. NN0 )
25	24	nn0zd 10757	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` F ) e. ZZ )
26		elfz5 11457	. . . . . . . . . . . . . . 15 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
27	22, 25, 26	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
28	18, 27	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ( 1 ... ( # ` F ) ) )
29		fnsnfv 5763	. . . . . . . . . . . . 13 |- ( ( F Fn ( 1 ... ( # ` F ) ) /\ ( N + 1 ) e. ( 1 ... ( # ` F ) ) ) -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
30	17, 28, 29	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
31	30	uneq2d 3522	. . . . . . . . . . 11 |- ( ph -> ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) ) )
32	1, 11, 31	3eqtr4a 2501	. . . . . . . . . 10 |- ( ph -> ( F " ( 1 ... ( N + 1 ) ) ) = ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) )
33	32	reseq2d 5122	. . . . . . . . 9 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) )
34		resundi 5136	. . . . . . . . 9 |- ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) )
35	33, 34	syl6eq 2491	. . . . . . . 8 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) )
36		f1of 5653	. . . . . . . . . . . . 13 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) --> A )
37	15, 36	syl 16	. . . . . . . . . . . 12 |- ( ph -> F : ( 1 ... ( # ` F ) ) --> A )
38	37, 28	ffvelrnd 5856	. . . . . . . . . . 11 |- ( ph -> ( F ` ( N + 1 ) ) e. A )
39		fnressn 5906	. . . . . . . . . . 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 661	. . . . . . . . . 10 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } )
41		eupaseg 23606	. . . . . . . . . . . . . 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 661	. . . . . . . . . . . . 13 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } )
43	3	nn0cnd 10650	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
44		ax-1cn 9352	. . . . . . . . . . . . . . . 16 |- 1 e. CC
45		pncan 9628	. . . . . . . . . . . . . . . 16 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
46	43, 44, 45	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
47	46	fveq2d 5707	. . . . . . . . . . . . . 14 |- ( ph -> ( P ` ( ( N + 1 ) - 1 ) ) = ( P ` N ) )
48	47	preq1d 3972	. . . . . . . . . . . . 13 |- ( ph -> { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
49	42, 48	eqtrd 2475	. . . . . . . . . . . 12 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
50	49	opeq2d 4078	. . . . . . . . . . 11 |- ( ph -> <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. = <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. )
51	50	sneqd 3901	. . . . . . . . . 10 |- ( ph -> { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
52	40, 51	eqtrd 2475	. . . . . . . . 9 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
53	52	uneq2d 3522	. . . . . . . 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 2475	. . . . . . 7 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
55	54	oveq2d 6119	. . . . . 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 5705	. . . . 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 5192	. . . . . . . 8 |- ( F " ( 1 ... N ) ) C_ ran F
58		f1ofo 5660	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -onto-> A )
59		forn 5635	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -onto-> A -> ran F = A )
60	15, 58, 59	3syl 20	. . . . . . . 8 |- ( ph -> ran F = A )
61	57, 60	syl5sseq 3416	. . . . . . 7 |- ( ph -> ( F " ( 1 ... N ) ) C_ A )
62		fnssres 5536	. . . . . . 7 |- ( ( E Fn A /\ ( F " ( 1 ... N ) ) C_ A ) -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
63	13, 61, 62	syl2anc 661	. . . . . 6 |- ( ph -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
64		fvex 5713	. . . . . . . 8 |- ( F ` ( N + 1 ) ) e. _V
65		prex 4546	. . . . . . . 8 |- { ( P ` N ) , ( P ` ( N + 1 ) ) } e. _V
66	64, 65	fnsn 5483	. . . . . . 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 23604	. . . . . . . 8 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> A e. Fin )
69	12, 13, 68	syl2anc 661	. . . . . . 7 |- ( ph -> A e. Fin )
70		ssfi 7545	. . . . . . 7 |- ( ( A e. Fin /\ ( F " ( 1 ... N ) ) C_ A ) -> ( F " ( 1 ... N ) ) e. Fin )
71	69, 61, 70	syl2anc 661	. . . . . 6 |- ( ph -> ( F " ( 1 ... N ) ) e. Fin )
72		snfi 7402	. . . . . . 7 |- { ( F ` ( N + 1 ) ) } e. Fin
73	72	a1i 11	. . . . . 6 |- ( ph -> { ( F ` ( N + 1 ) ) } e. Fin )
74	3	nn0red 10649	. . . . . . . . . 10 |- ( ph -> N e. RR )
75	74	ltp1d 10275	. . . . . . . . 9 |- ( ph -> N < ( N + 1 ) )
76		peano2re 9554	. . . . . . . . . . 11 |- ( N e. RR -> ( N + 1 ) e. RR )
77	74, 76	syl 16	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. RR )
78	74, 77	ltnled 9533	. . . . . . . . 9 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79	75, 78	mpbid 210	. . . . . . . 8 |- ( ph -> -. ( N + 1 ) <_ N )
80		f1of1 5652	. . . . . . . . . . 11 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -1-1-> A )
81	15, 80	syl 16	. . . . . . . . . 10 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-> A )
82	3	nn0zd 10757	. . . . . . . . . . . 12 |- ( ph -> N e. ZZ )
83	82	peano2zd 10762	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
84		eluz2 10879	. . . . . . . . . . . . 13 |- ( ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( N + 1 ) <_ ( # ` F ) ) )
85	83, 25, 18, 84	syl3anbrc 1172	. . . . . . . . . . . 12 |- ( ph -> ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) )
86		peano2uzr 10922	. . . . . . . . . . . 12 |- ( ( N e. ZZ /\ ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
87	82, 85, 86	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( # ` F ) e. ( ZZ>= ` N ) )
88		fzss2 11510	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
89	87, 88	syl 16	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
90		f1elima 5988	. . . . . . . . . 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 1218	. . . . . . . . 9 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) e. ( 1 ... N ) ) )
92		elfz5 11457	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
93	22, 82, 92	syl2anc 661	. . . . . . . . 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 301	. . . . . . 7 |- ( ph -> -. ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) )
96		disjsn 3948	. . . . . . 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 23599	. . . . . . 7 |- ( F ( V EulPaths E ) P -> V UMGrph E )
99		umgrares 23270	. . . . . . 7 |- ( V UMGrph E -> V UMGrph ( E |` ( F " ( 1 ... N ) ) ) )
100	12, 98, 99	3syl 20	. . . . . 6 |- ( ph -> V UMGrph ( E |` ( F " ( 1 ... N ) ) ) )
101		relumgra 23260	. . . . . . . . 9 |- Rel UMGrph
102	101	brrelexi 4891	. . . . . . . 8 |- ( V UMGrph E -> V e. _V )
103	12, 98, 102	3syl 20	. . . . . . 7 |- ( ph -> V e. _V )
104		eupapf 23605	. . . . . . . . 9 |- ( F ( V EulPaths E ) P -> P : ( 0 ... ( # ` F ) ) --> V )
105	12, 104	syl 16	. . . . . . . 8 |- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
106	3, 4	syl6eleq 2533	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` 0 ) )
107		elfzuzb 11459	. . . . . . . . 9 |- ( N e. ( 0 ... ( # ` F ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ( ZZ>= ` N ) ) )
108	106, 87, 107	sylanbrc 664	. . . . . . . 8 |- ( ph -> N e. ( 0 ... ( # ` F ) ) )
109	105, 108	ffvelrnd 5856	. . . . . . 7 |- ( ph -> ( P ` N ) e. V )
110		peano2nn0 10632	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
111	3, 110	syl 16	. . . . . . . . . . 11 |- ( ph -> ( N + 1 ) e. NN0 )
112	111, 4	syl6eleq 2533	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
113		elfz5 11457	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
114	112, 25, 113	syl2anc 661	. . . . . . . . 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 5856	. . . . . . 7 |- ( ph -> ( P ` ( N + 1 ) ) e. V )
117		umgra1 23272	. . . . . . 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 1219	. . . . . 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 23584	. . . . 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 2475	. . . 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 4316	. . 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 294	. 2 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) ) ` U ) <-> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) ) )
124		fveq2 5703	. . . . . . . . . 10 |- ( x = U -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
125	124	breq2d 4316	. . . . . . . . 9 |- ( x = U -> ( 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
126	125	notbid 294	. . . . . . . 8 |- ( x = U -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
127	126	elrab3 3130	. . . . . . 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 16	. . . . . 6 |- ( ph -> ( U e. { x e. V | -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) } <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
129		eupath2.8	. . . . . . 7 |- ( ph -> { x e. V | -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )
130	129	eleq2d 2510	. . . . . 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 465	. . . 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 10690	. . . . . . . 8 |- 2 e. ZZ
134	133	a1i 11	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
135		vdgrfif 23581	. . . . . . . . . . 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 1218	. . . . . . . . . 10 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
137	136, 119	ffvelrnd 5856	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. NN0 )
138	137	nn0zd 10757	. . . . . . . 8 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
139	138	adantr 465	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
140		vdgrfif 23581	. . . . . . . . . . 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 1218	. . . . . . . . . 10 |- ( ph -> ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) : V --> NN0 )
142	141, 119	ffvelrnd 5856	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. NN0 )
143	142	nn0zd 10757	. . . . . . . 8 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
144	143	adantr 465	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
145		iddvds 13558	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 2 )
146	133, 145	ax-mp 5	. . . . . . . . 9 |- 2 || 2
147		simpr 461	. . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) = U )
150	147, 149	preq12d 3974	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , U } )
151		dfsn2 3902	. . . . . . . . . . . . . . 15 |- { U } = { U , U }
152	150, 151	syl6eqr 2493	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U } )
153	152	opeq2d 4078	. . . . . . . . . . . . 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 3901	. . . . . . . . . . . 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 6119	. . . . . . . . . . 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 5705	. . . . . . . . . 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 725	. . . . . . . . . . 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 725	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
160	157, 158, 159	vdgr1d 23585	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U } >. } ) ` U ) = 2 )
161	156, 160	eqtrd 2475	. . . . . . . . 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 4340	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
163		dvds0 13560	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 0 )
164	133, 163	ax-mp 5	. . . . . . . . 9 |- 2 || 0
165	103	ad2antrr 725	. . . . . . . . . 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 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> U e. V )
168	109	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) e. V )
169		simpr 461	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) =/= U )
170	116	ad2antrr 725	. . . . . . . . . 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 2640	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) =/= U )
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 23588	. . . . . . . . 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 4340	. . . . . . . 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 2701	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
176		dvdsadd2b 13587	. . . . . . 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 1222	. . . . . 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 10650	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. CC )
179	137	nn0cnd 10650	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. CC )
180	178, 179	addcomd 9583	. . . . . . . 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 4316	. . . . . . 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 465	. . . . . 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 294	. . . 4 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) <-> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) ) )
185		simpr 461	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
186	185	eqeq2d 2454	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
187	185	preq2d 3973	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
188	186, 187	ifbieq2d 3826	. . . . 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 2510	. . . 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 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
192	191	preq1d 3972	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
193	192	opeq2d 4078	. . . . . . . . . . . 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 3901	. . . . . . . . . . 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 6119	. . . . . . . . . 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 5705	. . . . . . . . 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 725	. . . . . . . . . 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 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
200	116	ad2antrr 725	. . . . . . . . . 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 2640	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
203	202	necomd 2707	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) =/= U )
204	197, 198, 199, 200, 203	vdgr1b 23586	. . . . . . . . 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 2475	. . . . . . . 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 6119	. . . . . . 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 4316	. . . . . 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 294	. . . . 5 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
209		2nn 10491	. . . . . . . . . . . 12 |- 2 e. NN
210	209	a1i 11	. . . . . . . . . . 11 |- ( ph -> 2 e. NN )
211		1lt2 10500	. . . . . . . . . . . 12 |- 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 < 2 )
213		ndvdsp1 13625	. . . . . . . . . . 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 1218	. . . . . . . . . 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 13594	. . . . . . . . . . . 12 |- -. 2 || 1
217		opoe 13890	. . . . . . . . . . . 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 685	. . . . . . . . . . 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 434	. . . . . . . . . 10 |- ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) -> 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
220	138, 219	syl 16	. . . . . . . . 9 |- ( ph -> ( -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) -> 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
221	215, 220	impbid 191	. . . . . . . 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 294	. . . . . 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 725	. . . . 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 5713	. . . . . . 7 |- ( P ` N ) e. _V
226	225	eupath2lem2 23611	. . . . . 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 713	. . . . 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 461	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` ( N + 1 ) ) = U )
230	229	preq2d 3973	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
231	230	opeq2d 4078	. . . . . . . . . . . 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 3901	. . . . . . . . . . 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 6119	. . . . . . . . . 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 5705	. . . . . . . . 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 725	. . . . . . . . . 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 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> U e. V )
238	109	ad2antrr 725	. . . . . . . . . 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 2642	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
241	235, 236, 237, 238, 240	vdgr1c 23587	. . . . . . . . 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 2475	. . . . . . . 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 6119	. . . . . . 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 4316	. . . . . 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 294	. . . . 5 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 1 ) ) )
246	223	ad2antrr 725	. . . . 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 2705	. . . . . . . 8 |- ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` ( N + 1 ) ) =/= ( P ` N ) )
248		fvex 5713	. . . . . . . . 9 |- ( P ` ( N + 1 ) ) e. _V
249	248	eupath2lem2 23611	. . . . . . . 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 472	. . . . . . 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 330	. . . . . 6 |- ( ( ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( -. U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
252	251	adantll 713	. . . . 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 725	. . . . . . . . . 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 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U e. V )
257	109	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) e. V )
258		simprl 755	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) =/= U )
259	116	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` ( N + 1 ) ) e. V )
260		simprr 756	. . . . . . . . . 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 23588	. . . . . . . . 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 6119	. . . . . . . 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 9581	. . . . . . . . 9 |- ( ph -> ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 0 ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
264	263	ad2antrr 725	. . . . . . . 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 2475	. . . . . . 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 4316	. . . . . 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 294	. . . . 5 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( -. 2 || ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) ) <-> -. 2 || ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) ) )
268	131	ad2antrr 725	. . . . 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 2707	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` N ) )
270	260	necomd 2707	. . . . . . . . . 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 2628	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
273		neeq1 2628	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` ( N + 1 ) ) <-> ( P ` 0 ) =/= ( P ` ( N + 1 ) ) ) )
274	272, 273	bibi12d 321	. . . . . . . . 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 640	. . . . . . 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 2636	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` N ) )
278		biorf 405	. . . . . . . . . 10 |- ( -. U = ( P ` N ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` N ) \/ U = ( P ` 0 ) ) ) )
279	277, 278	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` N ) \/ U = ( P ` 0 ) ) ) )
280		orcom 387	. . . . . . . . 9 |- ( ( U = ( P ` N ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` N ) ) )
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 703	. . . . . . 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 2636	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> -. U = ( P ` ( N + 1 ) ) )
284		biorf 405	. . . . . . . . . 10 |- ( -. U = ( P ` ( N + 1 ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) ) )
285	283, 284	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U = ( P ` 0 ) <-> ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) ) )
286		orcom 387	. . . . . . . . 9 |- ( ( U = ( P ` ( N + 1 ) ) \/ U = ( P ` 0 ) ) <-> ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) )
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 703	. . . . . . 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 23610	. . . . . . 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 16	. . . . . 6 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) <-> ( ( P ` 0 ) =/= ( P ` N ) /\ ( U = ( P ` 0 ) \/ U = ( P ` N ) ) ) ) )
292		eupath2lem1 23610	. . . . . . 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 16	. . . . . 6 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) <-> ( ( P ` 0 ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` 0 ) \/ U = ( P ` ( N + 1 ) ) ) ) ) )
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 2702	. . 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 2701	. 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 368   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2618   {crab 2731   _Vcvv 2984   u. cun 3338   i^i cin 3339   C_ wss 3340   (/)c0 3649   ifcif 3803   {csn 3889   {cpr 3891   <.cop 3895   class class class wbr 4304   ran crn 4853   |` cres 4854   "cima 4855   Fn wfn 5425   -->wf 5426   -1-1->wf1 5427   -onto->wfo 5428   -1-1-onto->wf1o 5429   ` cfv 5430  (class class class)co 6103   Fincfn 7322   CCcc 9292   RRcr 9293   0cc0 9294   1c1 9295   + caddc 9297   < clt 9430   <_ cle 9431   - cmin 9607   NNcn 10334   2c2 10383   NN0cn0 10591   ZZcz 10658   ZZ>=cuz 10873   ...cfz 11449   #chash 12115   || cdivides 13547   UMGrph cumg 23258   VDeg cvdg 23575   EulPaths ceup 23595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-cnex 9350  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1