Theorem eupath2lem3 23535

Description: Lemma for eupath2 23536. (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 5246	. . . . . . . . . . 11 |- ( F " ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) )
2		1z 10672	. . . . . . . . . . . . 13 |- 1 e. ZZ
3		eupath2.5	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
4		nn0uz 10891	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
5		1m1e0 10386	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
6	5	fveq2i 5691	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
7	4, 6	eqtr4i 2464	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
8	3, 7	syl6eleq 2531	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
9		fzsuc2 11510	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ N e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
10	2, 8, 9	sylancr 658	. . . . . . . . . . . 12 |- ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... N ) u. { ( N + 1 ) } ) )
11	10	imaeq2d 5166	. . . . . . . . . . 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 23526	. . . . . . . . . . . . . . 15 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
15	12, 13, 14	syl2anc 656	. . . . . . . . . . . . . 14 |- ( ph -> F : ( 1 ... ( # ` F ) ) -1-1-onto-> A )
16		f1ofn 5639	. . . . . . . . . . . . . 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 10615	. . . . . . . . . . . . . . . . 17 |- ( N e. NN0 -> ( N + 1 ) e. NN )
20	3, 19	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
21		nnuz 10892	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
22	20, 21	syl6eleq 2531	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
23		eupacl 23525	. . . . . . . . . . . . . . . . 17 |- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )
24	12, 23	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( # ` F ) e. NN0 )
25	24	nn0zd 10741	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` F ) e. ZZ )
26		elfz5 11441	. . . . . . . . . . . . . . 15 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
27	22, 25, 26	syl2anc 656	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N + 1 ) e. ( 1 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
28	18, 27	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ( 1 ... ( # ` F ) ) )
29		fnsnfv 5748	. . . . . . . . . . . . 13 |- ( ( F Fn ( 1 ... ( # ` F ) ) /\ ( N + 1 ) e. ( 1 ... ( # ` F ) ) ) -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
30	17, 28, 29	syl2anc 656	. . . . . . . . . . . 12 |- ( ph -> { ( F ` ( N + 1 ) ) } = ( F " { ( N + 1 ) } ) )
31	30	uneq2d 3507	. . . . . . . . . . 11 |- ( ph -> ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) ) )
32	1, 11, 31	3eqtr4a 2499	. . . . . . . . . 10 |- ( ph -> ( F " ( 1 ... ( N + 1 ) ) ) = ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) )
33	32	reseq2d 5106	. . . . . . . . 9 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) )
34		resundi 5121	. . . . . . . . 9 |- ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) )
35	33, 34	syl6eq 2489	. . . . . . . 8 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) )
36		f1of 5638	. . . . . . . . . . . . 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 5841	. . . . . . . . . . 11 |- ( ph -> ( F ` ( N + 1 ) ) e. A )
39		fnressn 5891	. . . . . . . . . . 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 656	. . . . . . . . . 10 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } )
41		eupaseg 23529	. . . . . . . . . . . . . 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 656	. . . . . . . . . . . . 13 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } )
43	3	nn0cnd 10634	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
44		ax-1cn 9336	. . . . . . . . . . . . . . . 16 |- 1 e. CC
45		pncan 9612	. . . . . . . . . . . . . . . 16 |- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
46	43, 44, 45	sylancl 657	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N + 1 ) - 1 ) = N )
47	46	fveq2d 5692	. . . . . . . . . . . . . 14 |- ( ph -> ( P ` ( ( N + 1 ) - 1 ) ) = ( P ` N ) )
48	47	preq1d 3957	. . . . . . . . . . . . 13 |- ( ph -> { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
49	42, 48	eqtrd 2473	. . . . . . . . . . . 12 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
50	49	opeq2d 4063	. . . . . . . . . . 11 |- ( ph -> <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. = <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. )
51	50	sneqd 3886	. . . . . . . . . 10 |- ( ph -> { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
52	40, 51	eqtrd 2473	. . . . . . . . 9 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
53	52	uneq2d 3507	. . . . . . . 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 2473	. . . . . . 7 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
55	54	oveq2d 6106	. . . . . 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 5690	. . . . 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 5177	. . . . . . . 8 |- ( F " ( 1 ... N ) ) C_ ran F
58		f1ofo 5645	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -onto-> A )
59		forn 5620	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -onto-> A -> ran F = A )
60	15, 58, 59	3syl 20	. . . . . . . 8 |- ( ph -> ran F = A )
61	57, 60	syl5sseq 3401	. . . . . . 7 |- ( ph -> ( F " ( 1 ... N ) ) C_ A )
62		fnssres 5521	. . . . . . 7 |- ( ( E Fn A /\ ( F " ( 1 ... N ) ) C_ A ) -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
63	13, 61, 62	syl2anc 656	. . . . . 6 |- ( ph -> ( E |` ( F " ( 1 ... N ) ) ) Fn ( F " ( 1 ... N ) ) )
64		fvex 5698	. . . . . . . 8 |- ( F ` ( N + 1 ) ) e. _V
65		prex 4531	. . . . . . . 8 |- { ( P ` N ) , ( P ` ( N + 1 ) ) } e. _V
66	64, 65	fnsn 5468	. . . . . . 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 23527	. . . . . . . 8 |- ( ( F ( V EulPaths E ) P /\ E Fn A ) -> A e. Fin )
69	12, 13, 68	syl2anc 656	. . . . . . 7 |- ( ph -> A e. Fin )
70		ssfi 7529	. . . . . . 7 |- ( ( A e. Fin /\ ( F " ( 1 ... N ) ) C_ A ) -> ( F " ( 1 ... N ) ) e. Fin )
71	69, 61, 70	syl2anc 656	. . . . . 6 |- ( ph -> ( F " ( 1 ... N ) ) e. Fin )
72		snfi 7386	. . . . . . 7 |- { ( F ` ( N + 1 ) ) } e. Fin
73	72	a1i 11	. . . . . 6 |- ( ph -> { ( F ` ( N + 1 ) ) } e. Fin )
74	3	nn0red 10633	. . . . . . . . . 10 |- ( ph -> N e. RR )
75	74	ltp1d 10259	. . . . . . . . 9 |- ( ph -> N < ( N + 1 ) )
76		peano2re 9538	. . . . . . . . . . 11 |- ( N e. RR -> ( N + 1 ) e. RR )
77	74, 76	syl 16	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. RR )
78	74, 77	ltnled 9517	. . . . . . . . 9 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79	75, 78	mpbid 210	. . . . . . . 8 |- ( ph -> -. ( N + 1 ) <_ N )
80		f1of1 5637	. . . . . . . . . . 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 10741	. . . . . . . . . . . 12 |- ( ph -> N e. ZZ )
83	82	peano2zd 10746	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
84		eluz2 10863	. . . . . . . . . . . . 13 |- ( ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( N + 1 ) <_ ( # ` F ) ) )
85	83, 25, 18, 84	syl3anbrc 1167	. . . . . . . . . . . 12 |- ( ph -> ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) )
86		peano2uzr 10906	. . . . . . . . . . . 12 |- ( ( N e. ZZ /\ ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
87	82, 85, 86	syl2anc 656	. . . . . . . . . . 11 |- ( ph -> ( # ` F ) e. ( ZZ>= ` N ) )
88		fzss2 11494	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
89	87, 88	syl 16	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
90		f1elima 5973	. . . . . . . . . 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 1213	. . . . . . . . 9 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) e. ( 1 ... N ) ) )
92		elfz5 11441	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( N + 1 ) e. ( 1 ... N ) <-> ( N + 1 ) <_ N ) )
93	22, 82, 92	syl2anc 656	. . . . . . . . 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 3933	. . . . . . 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 23522	. . . . . . 7 |- ( F ( V EulPaths E ) P -> V UMGrph E )
99		umgrares 23193	. . . . . . 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 23183	. . . . . . . . 9 |- Rel UMGrph
102	101	brrelexi 4875	. . . . . . . 8 |- ( V UMGrph E -> V e. _V )
103	12, 98, 102	3syl 20	. . . . . . 7 |- ( ph -> V e. _V )
104		eupapf 23528	. . . . . . . . 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 2531	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` 0 ) )
107		elfzuzb 11443	. . . . . . . . 9 |- ( N e. ( 0 ... ( # ` F ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ( ZZ>= ` N ) ) )
108	106, 87, 107	sylanbrc 659	. . . . . . . 8 |- ( ph -> N e. ( 0 ... ( # ` F ) ) )
109	105, 108	ffvelrnd 5841	. . . . . . 7 |- ( ph -> ( P ` N ) e. V )
110		peano2nn0 10616	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
111	3, 110	syl 16	. . . . . . . . . . 11 |- ( ph -> ( N + 1 ) e. NN0 )
112	111, 4	syl6eleq 2531	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
113		elfz5 11441	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ZZ ) -> ( ( N + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( N + 1 ) <_ ( # ` F ) ) )
114	112, 25, 113	syl2anc 656	. . . . . . . . 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 5841	. . . . . . 7 |- ( ph -> ( P ` ( N + 1 ) ) e. V )
117		umgra1 23195	. . . . . . 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 1214	. . . . . 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 23507	. . . . 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 2473	. . . 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 4301	. . 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 5688	. . . . . . . . . 10 |- ( x = U -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
125	124	breq2d 4301	. . . . . . . . 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 3115	. . . . . . 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 2508	. . . . . 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 462	. . . 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 10674	. . . . . . . 8 |- 2 e. ZZ
134	133	a1i 11	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
135		vdgrfif 23504	. . . . . . . . . . 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 1213	. . . . . . . . . 10 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
137	136, 119	ffvelrnd 5841	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. NN0 )
138	137	nn0zd 10741	. . . . . . . 8 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
139	138	adantr 462	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. ZZ )
140		vdgrfif 23504	. . . . . . . . . . 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 1213	. . . . . . . . . 10 |- ( ph -> ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) : V --> NN0 )
142	141, 119	ffvelrnd 5841	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. NN0 )
143	142	nn0zd 10741	. . . . . . . 8 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
144	143	adantr 462	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. ZZ )
145		iddvds 13542	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 2 )
146	133, 145	ax-mp 5	. . . . . . . . 9 |- 2 || 2
147		simpr 458	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
148		simplr 749	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
149	148, 147	eqtr3d 2475	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) = U )
150	147, 149	preq12d 3959	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , U } )
151		dfsn2 3887	. . . . . . . . . . . . . . 15 |- { U } = { U , U }
152	150, 151	syl6eqr 2491	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U } )
153	152	opeq2d 4063	. . . . . . . . . . . . 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 3886	. . . . . . . . . . . 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 6106	. . . . . . . . . . 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 5690	. . . . . . . . . 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 720	. . . . . . . . . . 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 720	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
160	157, 158, 159	vdgr1d 23508	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U } >. } ) ` U ) = 2 )
161	156, 160	eqtrd 2473	. . . . . . . . 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 4325	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
163		dvds0 13544	. . . . . . . . . 10 |- ( 2 e. ZZ -> 2 || 0 )
164	133, 163	ax-mp 5	. . . . . . . . 9 |- 2 || 0
165	103	ad2antrr 720	. . . . . . . . . 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 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> U e. V )
168	109	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) e. V )
169		simpr 458	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) =/= U )
170	116	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) e. V )
171		simplr 749	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
172	171, 169	eqnetrrd 2626	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) =/= U )
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 23511	. . . . . . . . 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 4325	. . . . . . . 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 2687	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
176		dvdsadd2b 13571	. . . . . . 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 1217	. . . . . 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 10634	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. CC )
179	137	nn0cnd 10634	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. CC )
180	178, 179	addcomd 9567	. . . . . . . 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 4301	. . . . . . 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 462	. . . . . 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 458	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
186	185	eqeq2d 2452	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
187	185	preq2d 3958	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
188	186, 187	ifbieq2d 3811	. . . . 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 2508	. . . 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 458	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = U )
192	191	preq1d 3957	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
193	192	opeq2d 4063	. . . . . . . . . . . 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 3886	. . . . . . . . . . 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 6106	. . . . . . . . . 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 5690	. . . . . . . . 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 720	. . . . . . . . . 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 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U e. V )
200	116	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) e. V )
201		simplr 749	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
202	191, 201	eqnetrrd 2626	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
203	202	necomd 2693	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) =/= U )
204	197, 198, 199, 200, 203	vdgr1b 23509	. . . . . . . . 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 2473	. . . . . . . 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 6106	. . . . . . 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 4301	. . . . . 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 10475	. . . . . . . . . . . 12 |- 2 e. NN
210	209	a1i 11	. . . . . . . . . . 11 |- ( ph -> 2 e. NN )
211		1lt2 10484	. . . . . . . . . . . 12 |- 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 < 2 )
213		ndvdsp1 13609	. . . . . . . . . . 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 1213	. . . . . . . . . 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 13578	. . . . . . . . . . . 12 |- -. 2 || 1
217		opoe 13874	. . . . . . . . . . . 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 680	. . . . . . . . . . 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 720	. . . . 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 5698	. . . . . . 7 |- ( P ` N ) e. _V
226	225	eupath2lem2 23534	. . . . . 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 708	. . . . 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 458	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` ( N + 1 ) ) = U )
230	229	preq2d 3958	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
231	230	opeq2d 4063	. . . . . . . . . . . 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 3886	. . . . . . . . . . 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 6106	. . . . . . . . . 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 5690	. . . . . . . . 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 720	. . . . . . . . . 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 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> U e. V )
238	109	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) e. V )
239		simplr 749	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
240	239, 229	neeqtrd 2628	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
241	235, 236, 237, 238, 240	vdgr1c 23510	. . . . . . . . 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 2473	. . . . . . . 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 6106	. . . . . . 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 4301	. . . . . 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 720	. . . . 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 2691	. . . . . . . 8 |- ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` ( N + 1 ) ) =/= ( P ` N ) )
248		fvex 5698	. . . . . . . . 9 |- ( P ` ( N + 1 ) ) e. _V
249	248	eupath2lem2 23534	. . . . . . . 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 469	. . . . . . 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 708	. . . . 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 720	. . . . . . . . . 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 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U e. V )
257	109	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) e. V )
258		simprl 750	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` N ) =/= U )
259	116	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> ( P ` ( N + 1 ) ) e. V )
260		simprr 751	. . . . . . . . . 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 23511	. . . . . . . . 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 6106	. . . . . . . 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 9565	. . . . . . . . 9 |- ( ph -> ( ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) + 0 ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
264	263	ad2antrr 720	. . . . . . . 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 2473	. . . . . . 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 4301	. . . . . 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 720	. . . . 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 2693	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` N ) )
270	260	necomd 2693	. . . . . . . . . 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 2614	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
273		neeq1 2614	. . . . . . . . . 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 635	. . . . . . 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 2622	. . . . . . . . . 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 698	. . . . . . 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 2622	. . . . . . . . . 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 698	. . . . . . 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 23533	. . . . . . 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 23533	. . . . . . 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 2688	. . 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 2687	. 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 1364   e. wcel 1761   =/= wne 2604   {crab 2717   _Vcvv 2970   u. cun 3323   i^i cin 3324   C_ wss 3325   (/)c0 3634   ifcif 3788   {csn 3874   {cpr 3876   <.cop 3880   class class class wbr 4289   ran crn 4837   |` cres 4838   "cima 4839   Fn wfn 5410   -->wf 5411   -1-1->wf1 5412   -onto->wfo 5413   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   Fincfn 7306   CCcc 9276   RRcr 9277   0cc0 9278   1c1 9279   + caddc 9281   < clt 9414   <_ cle 9415   - cmin 9591   NNcn 10318   2c2 10367   NN0cn0 10575   ZZcz 10642   ZZ>=cuz 10857   ...cfz 11433   #chash 12099   || cdivides 13531   UMGrph cumg 23181   VDeg cvdg 23498   EulPaths ceup 23518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346 &nbs