Theorem konigsberg

Description: The Königsberg Bridge problem. If G is the Königsberg graph, i.e. a graph on four vertices 0 , 1 , 2 , 3 , with edges { 0 , 1 } , { 0 , 2 } , { 0 , 3 } , { 1 , 2 } , { 1 , 2 } , { 2 , 3 } , { 2 , 3 } , then vertices 0 , 1 , 3 each have degree three, and 2 has degree five, so there are four vertices of odd degree and thus by eulerpath the graph cannot have an Eulerian path. It is sufficient to show that there are 3 vertices of odd degree, since a graph having an Eulerian path can only have 0 or 2 vertices of odd degree. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 9-Mar-2021)

	Ref	Expression
Hypotheses	konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
	konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
	konigsberg.g	$$⊢G=⟨V,E⟩$$
Assertion	konigsberg	$$⊢\mathrm{EulerPaths}\left(G\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
2		konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
3		konigsberg.g	$$⊢G=⟨V,E⟩$$
4	1 2 3	konigsberglem5	$$⊢2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|$$
5		elpri	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}\to \left(\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=0\vee \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=2\right)$$
6		2pos	$$⊢0<2$$
7		0re	$$⊢0\in ℝ$$
8		2re	$$⊢2\in ℝ$$
9	7 8	ltnsymi	$$⊢0<2\to \neg 2<0$$
10	6 9	ax-mp	$$⊢\neg 2<0$$
11		breq2	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=0\to \left(2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\leftrightarrow 2<0\right)$$
12	10 11	mtbiri	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=0\to \neg 2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|$$
13	8	ltnri	$$⊢\neg 2<2$$
14		breq2	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=2\to \left(2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\leftrightarrow 2<2\right)$$
15	13 14	mtbiri	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=2\to \neg 2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|$$
16	12 15	jaoi	$$⊢\left(\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=0\vee \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|=2\right)\to \neg 2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|$$
17	5 16	syl	$$⊢\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}\to \neg 2<\left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|$$
18	4 17	mt2	$$⊢\neg \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}$$
19	1 2 3	konigsbergumgr	$$⊢G\in \mathrm{UMGraph}$$
20		umgrupgr	$$⊢G\in \mathrm{UMGraph}\to G\in \mathrm{UPGraph}$$
21	19 20	ax-mp	$$⊢G\in \mathrm{UPGraph}$$
22	3	fveq2i	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(⟨V,E⟩\right)$$
23	1	ovexi	$$⊢V\in \mathrm{V}$$
24		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
25	2 24	eqeltri	$$⊢E\in \mathrm{Word}\mathrm{V}$$
26		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{Word}\mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,E⟩\right)=V$$
27	23 25 26	mp2an	$$⊢\mathrm{Vtx}\left(⟨V,E⟩\right)=V$$
28	22 27	eqtr2i	$$⊢V=\mathrm{Vtx}\left(G\right)$$
29	28	eulerpath	$$⊢\left(G\in \mathrm{UPGraph}\wedge \mathrm{EulerPaths}\left(G\right)\ne \varnothing \right)\to \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}$$
30	21 29	mpan	$$⊢\mathrm{EulerPaths}\left(G\right)\ne \varnothing \to \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}$$
31	30	necon1bi	$$⊢\neg \left|\left\{x\in V|\neg 2\parallel \mathrm{VtxDeg}\left(G\right)\left(x\right)\right\}\right|\in \left\{0,2\right\}\to \mathrm{EulerPaths}\left(G\right)=\varnothing$$
32	18 31	ax-mp	$$⊢\mathrm{EulerPaths}\left(G\right)=\varnothing$$