Theorem eupath2lem3 25105

Description: Lemma for eupath2 25106. (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 5425	. . . . . . . . . . 11 |- ( F " ( ( 1 ... N ) u. { ( N + 1 ) } ) ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) )
2		1z 10915	. . . . . . . . . . . . 13 |- 1 e. ZZ
3		eupath2.5	. . . . . . . . . . . . . 14 |- ( ph -> N e. NN0 )
4		nn0uz 11140	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
5		1m1e0 10625	. . . . . . . . . . . . . . . 16 |- ( 1 - 1 ) = 0
6	5	fveq2i 5875	. . . . . . . . . . . . . . 15 |- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
7	4, 6	eqtr4i 2489	. . . . . . . . . . . . . 14 |- NN0 = ( ZZ>= ` ( 1 - 1 ) )
8	3, 7	syl6eleq 2555	. . . . . . . . . . . . 13 |- ( ph -> N e. ( ZZ>= ` ( 1 - 1 ) ) )
9		fzsuc2 11762	. . . . . . . . . . . . 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 5347	. . . . . . . . . . 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 25096	. . . . . . . . . . . . . . 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 5823	. . . . . . . . . . . . . 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 10856	. . . . . . . . . . . . . . . . 17 |- ( N e. NN0 -> ( N + 1 ) e. NN )
20	3, 19	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. NN )
21		nnuz 11141	. . . . . . . . . . . . . . . 16 |- NN = ( ZZ>= ` 1 )
22	20, 21	syl6eleq 2555	. . . . . . . . . . . . . . 15 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
23		eupacl 25095	. . . . . . . . . . . . . . . . 17 |- ( F ( V EulPaths E ) P -> ( # ` F ) e. NN0 )
24	12, 23	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( # ` F ) e. NN0 )
25	24	nn0zd 10988	. . . . . . . . . . . . . . 15 |- ( ph -> ( # ` F ) e. ZZ )
26		elfz5 11705	. . . . . . . . . . . . . . 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 5933	. . . . . . . . . . . . 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 3654	. . . . . . . . . . 11 |- ( ph -> ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) = ( ( F " ( 1 ... N ) ) u. ( F " { ( N + 1 ) } ) ) )
32	1, 11, 31	3eqtr4a 2524	. . . . . . . . . 10 |- ( ph -> ( F " ( 1 ... ( N + 1 ) ) ) = ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) )
33	32	reseq2d 5283	. . . . . . . . 9 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) )
34		resundi 5297	. . . . . . . . 9 |- ( E |` ( ( F " ( 1 ... N ) ) u. { ( F ` ( N + 1 ) ) } ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) )
35	33, 34	syl6eq 2514	. . . . . . . 8 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. ( E |` { ( F ` ( N + 1 ) ) } ) ) )
36		f1of 5822	. . . . . . . . . . . . 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 6033	. . . . . . . . . . 11 |- ( ph -> ( F ` ( N + 1 ) ) e. A )
39		fnressn 6084	. . . . . . . . . . 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 25099	. . . . . . . . . . . . . 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 10875	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. CC )
44		ax-1cn 9567	. . . . . . . . . . . . . . . 16 |- 1 e. CC
45		pncan 9845	. . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . 14 |- ( ph -> ( P ` ( ( N + 1 ) - 1 ) ) = ( P ` N ) )
48	47	preq1d 4117	. . . . . . . . . . . . 13 |- ( ph -> { ( P ` ( ( N + 1 ) - 1 ) ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
49	42, 48	eqtrd 2498	. . . . . . . . . . . 12 |- ( ph -> ( E ` ( F ` ( N + 1 ) ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )
50	49	opeq2d 4226	. . . . . . . . . . 11 |- ( ph -> <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. = <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. )
51	50	sneqd 4044	. . . . . . . . . 10 |- ( ph -> { <. ( F ` ( N + 1 ) ) , ( E ` ( F ` ( N + 1 ) ) ) >. } = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
52	40, 51	eqtrd 2498	. . . . . . . . 9 |- ( ph -> ( E |` { ( F ` ( N + 1 ) ) } ) = { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } )
53	52	uneq2d 3654	. . . . . . . 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 2498	. . . . . . 7 |- ( ph -> ( E |` ( F " ( 1 ... ( N + 1 ) ) ) ) = ( ( E |` ( F " ( 1 ... N ) ) ) u. { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) )
55	54	oveq2d 6312	. . . . . 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 5874	. . . . 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 5358	. . . . . . . 8 |- ( F " ( 1 ... N ) ) C_ ran F
58		f1ofo 5829	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -1-1-onto-> A -> F : ( 1 ... ( # ` F ) ) -onto-> A )
59		forn 5804	. . . . . . . . 9 |- ( F : ( 1 ... ( # ` F ) ) -onto-> A -> ran F = A )
60	15, 58, 59	3syl 20	. . . . . . . 8 |- ( ph -> ran F = A )
61	57, 60	syl5sseq 3547	. . . . . . 7 |- ( ph -> ( F " ( 1 ... N ) ) C_ A )
62		fnssres 5700	. . . . . . 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 5882	. . . . . . . 8 |- ( F ` ( N + 1 ) ) e. _V
65		prex 4698	. . . . . . . 8 |- { ( P ` N ) , ( P ` ( N + 1 ) ) } e. _V
66	64, 65	fnsn 5647	. . . . . . 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 25097	. . . . . . . 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 7759	. . . . . . 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 7615	. . . . . . 7 |- { ( F ` ( N + 1 ) ) } e. Fin
73	72	a1i 11	. . . . . 6 |- ( ph -> { ( F ` ( N + 1 ) ) } e. Fin )
74	3	nn0red 10874	. . . . . . . . . 10 |- ( ph -> N e. RR )
75	74	ltp1d 10496	. . . . . . . . 9 |- ( ph -> N < ( N + 1 ) )
76		peano2re 9770	. . . . . . . . . . 11 |- ( N e. RR -> ( N + 1 ) e. RR )
77	74, 76	syl 16	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. RR )
78	74, 77	ltnled 9749	. . . . . . . . 9 |- ( ph -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79	75, 78	mpbid 210	. . . . . . . 8 |- ( ph -> -. ( N + 1 ) <_ N )
80		f1of1 5821	. . . . . . . . . . 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 10988	. . . . . . . . . . . 12 |- ( ph -> N e. ZZ )
83	82	peano2zd 10993	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
84		eluz2 11112	. . . . . . . . . . . . 13 |- ( ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) <-> ( ( N + 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( N + 1 ) <_ ( # ` F ) ) )
85	83, 25, 18, 84	syl3anbrc 1180	. . . . . . . . . . . 12 |- ( ph -> ( # ` F ) e. ( ZZ>= ` ( N + 1 ) ) )
86		peano2uzr 11161	. . . . . . . . . . . 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 11748	. . . . . . . . . . 11 |- ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
89	87, 88	syl 16	. . . . . . . . . 10 |- ( ph -> ( 1 ... N ) C_ ( 1 ... ( # ` F ) ) )
90		f1elima 6172	. . . . . . . . . 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 1228	. . . . . . . . 9 |- ( ph -> ( ( F ` ( N + 1 ) ) e. ( F " ( 1 ... N ) ) <-> ( N + 1 ) e. ( 1 ... N ) ) )
92		elfz5 11705	. . . . . . . . . 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 4092	. . . . . . 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 25092	. . . . . . 7 |- ( F ( V EulPaths E ) P -> V UMGrph E )
99		umgrares 24450	. . . . . . 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 24440	. . . . . . . . 9 |- Rel UMGrph
102	101	brrelexi 5049	. . . . . . . 8 |- ( V UMGrph E -> V e. _V )
103	12, 98, 102	3syl 20	. . . . . . 7 |- ( ph -> V e. _V )
104		eupapf 25098	. . . . . . . . 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 2555	. . . . . . . . 9 |- ( ph -> N e. ( ZZ>= ` 0 ) )
107		elfzuzb 11707	. . . . . . . . 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 6033	. . . . . . 7 |- ( ph -> ( P ` N ) e. V )
110		peano2nn0 10857	. . . . . . . . . . . 12 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
111	3, 110	syl 16	. . . . . . . . . . 11 |- ( ph -> ( N + 1 ) e. NN0 )
112	111, 4	syl6eleq 2555	. . . . . . . . . 10 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
113		elfz5 11705	. . . . . . . . . 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 6033	. . . . . . 7 |- ( ph -> ( P ` ( N + 1 ) ) e. V )
117		umgra1 24452	. . . . . . 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 1229	. . . . . 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 25028	. . . . 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 2498	. . . 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 4468	. . 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 5872	. . . . . . . . . 10 |- ( x = U -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` x ) = ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) )
125	124	breq2d 4468	. . . . . . . . 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 3258	. . . . . . 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 2527	. . . . . 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 10917	. . . . . . . 8 |- 2 e. ZZ
134	133	a1i 11	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 e. ZZ )
135		vdgrfif 25025	. . . . . . . . . . 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 1228	. . . . . . . . . 10 |- ( ph -> ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) : V --> NN0 )
137	136, 119	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. NN0 )
138	137	nn0zd 10988	. . . . . . . 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 25025	. . . . . . . . . . 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 1228	. . . . . . . . . 10 |- ( ph -> ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) : V --> NN0 )
142	141, 119	ffvelrnd 6033	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. NN0 )
143	142	nn0zd 10988	. . . . . . . 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 14008	. . . . . . . . . 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 755	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
149	148, 147	eqtr3d 2500	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) = U )
150	147, 149	preq12d 4119	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , U } )
151		dfsn2 4045	. . . . . . . . . . . . . . 15 |- { U } = { U , U }
152	150, 151	syl6eqr 2516	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U } )
153	152	opeq2d 4226	. . . . . . . . . . . . 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 4044	. . . . . . . . . . . 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 6312	. . . . . . . . . . 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 5874	. . . . . . . . . 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 25029	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { U } >. } ) ` U ) = 2 )
161	156, 160	eqtrd 2498	. . . . . . . . 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 4492	. . . . . . . 8 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
163		dvds0 14010	. . . . . . . . . 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 755	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` N ) = ( P ` ( N + 1 ) ) )
172	171, 169	eqnetrrd 2751	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) /\ ( P ` N ) =/= U ) -> ( P ` ( N + 1 ) ) =/= U )
173	165, 166, 167, 168, 169, 170, 172	vdgr1a 25032	. . . . . . . . 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 4492	. . . . . . . 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 2775	. . . . . . 7 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> 2 || ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) )
176		dvdsadd2b 14039	. . . . . . 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 1232	. . . . . 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 10875	. . . . . . . . 9 |- ( ph -> ( ( V VDeg { <. ( F ` ( N + 1 ) ) , { ( P ` N ) , ( P ` ( N + 1 ) ) } >. } ) ` U ) e. CC )
179	137	nn0cnd 10875	. . . . . . . . 9 |- ( ph -> ( ( V VDeg ( E |` ( F " ( 1 ... N ) ) ) ) ` U ) e. CC )
180	178, 179	addcomd 9799	. . . . . . . 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 4468	. . . . . . 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 2471	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( ( P ` 0 ) = ( P ` N ) <-> ( P ` 0 ) = ( P ` ( N + 1 ) ) ) )
187	185	preq2d 4118	. . . . . 6 |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> { ( P ` 0 ) , ( P ` N ) } = { ( P ` 0 ) , ( P ` ( N + 1 ) ) } )
188	186, 187	ifbieq2d 3969	. . . . 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 2527	. . . 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 4117	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { U , ( P ` ( N + 1 ) ) } )
193	192	opeq2d 4226	. . . . . . . . . . . 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 4044	. . . . . . . . . . 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 6312	. . . . . . . . . 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 5874	. . . . . . . . 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 755	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
202	191, 201	eqnetrrd 2751	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> U =/= ( P ` ( N + 1 ) ) )
203	202	necomd 2728	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` N ) = U ) -> ( P ` ( N + 1 ) ) =/= U )
204	197, 198, 199, 200, 203	vdgr1b 25030	. . . . . . . . 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 2498	. . . . . . . 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 6312	. . . . . . 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 4468	. . . . . 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 10714	. . . . . . . . . . . 12 |- 2 e. NN
210	209	a1i 11	. . . . . . . . . . 11 |- ( ph -> 2 e. NN )
211		1lt2 10723	. . . . . . . . . . . 12 |- 1 < 2
212	211	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 < 2 )
213		ndvdsp1 14078	. . . . . . . . . . 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 1228	. . . . . . . . . 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 14046	. . . . . . . . . . . 12 |- -. 2 || 1
217		opoe 14346	. . . . . . . . . . . 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 5882	. . . . . . 7 |- ( P ` N ) e. _V
226	225	eupath2lem2 25104	. . . . . 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 4118	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } = { ( P ` N ) , U } )
231	230	opeq2d 4226	. . . . . . . . . . . 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 4044	. . . . . . . . . . 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 6312	. . . . . . . . . 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 5874	. . . . . . . . 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 755	. . . . . . . . . . 11 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= ( P ` ( N + 1 ) ) )
240	239, 229	neeqtrd 2752	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( P ` ( N + 1 ) ) = U ) -> ( P ` N ) =/= U )
241	235, 236, 237, 238, 240	vdgr1c 25031	. . . . . . . . 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 2498	. . . . . . . 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 6312	. . . . . . 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 4468	. . . . . 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 2726	. . . . . . . 8 |- ( ( P ` N ) =/= ( P ` ( N + 1 ) ) <-> ( P ` ( N + 1 ) ) =/= ( P ` N ) )
248		fvex 5882	. . . . . . . . 9 |- ( P ` ( N + 1 ) ) e. _V
249	248	eupath2lem2 25104	. . . . . . . 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 756	. . . . . . . . . 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 757	. . . . . . . . . 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 25032	. . . . . . . . 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 6312	. . . . . . . 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 9797	. . . . . . . . 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 2498	. . . . . . 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 4468	. . . . . 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 2728	. . . . . . . . . 10 |- ( ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) ) /\ ( ( P ` N ) =/= U /\ ( P ` ( N + 1 ) ) =/= U ) ) -> U =/= ( P ` N ) )
270	260	necomd 2728	. . . . . . . . . 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 2738	. . . . . . . . . 10 |- ( U = ( P ` 0 ) -> ( U =/= ( P ` N ) <-> ( P ` 0 ) =/= ( P ` N ) ) )
273		neeq1 2738	. . . . . . . . . 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 2659	. . . . . . . . . 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 2659	. . . . . . . . . 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 25103	. . . . . . 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 25103	. . . . . . 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 2776	. . 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 2775	. 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 1395   e. wcel 1819   =/= wne 2652   {crab 2811   _Vcvv 3109   u. cun 3469   i^i cin 3470   C_ wss 3471   (/)c0 3793   ifcif 3944   {csn 4032   {cpr 4034   <.cop 4038   class class class wbr 4456   ran crn 5009   |` cres 5010   "cima 5011   Fn wfn 5589   -->wf 5590   -1-1->wf1 5591   -onto->wfo 5592   -1-1-onto->wf1o 5593   ` cfv 5594  (class class class)co 6296   Fincfn 7535   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510   + caddc 9512   < clt 9645   <_ cle 9646   - cmin 9824   NNcn 10556   2c2 10606   NN0cn0 10816   ZZcz 10885   ZZ>=cuz 11106   ...cfz 11697   #chash 12407   || cdvds 13997   UMGrph cumg 24438   VDeg cvdg 25019   EulPaths ceup 25088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576