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	⊢ 𝑉 = ( 0 ... 3 )
	konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
	konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	konigsberg	⊢ ( EulerPaths ‘ 𝐺 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	⊢ 𝑉 = ( 0 ... 3 )
2		konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
3		konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4	1 2 3	konigsberglem5	⊢ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )
5		elpri	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } → ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 0 ∨ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 2 ) )
6		2pos	⊢ 0 < 2
7		0re	⊢ 0 ∈ ℝ
8		2re	⊢ 2 ∈ ℝ
9	7 8	ltnsymi	⊢ ( 0 < 2 → ¬ 2 < 0 )
10	6 9	ax-mp	⊢ ¬ 2 < 0
11		breq2	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 0 → ( 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ 2 < 0 ) )
12	10 11	mtbiri	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 0 → ¬ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
13	8	ltnri	⊢ ¬ 2 < 2
14		breq2	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 2 → ( 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ 2 < 2 ) )
15	13 14	mtbiri	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 2 → ¬ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
16	12 15	jaoi	⊢ ( ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 0 ∨ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 2 ) → ¬ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
17	5 16	syl	⊢ ( ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } → ¬ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
18	4 17	mt2	⊢ ¬ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 }
19	1 2 3	konigsbergumgr	⊢ 𝐺 ∈ UMGraph
20		umgrupgr	⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )
21	19 20	ax-mp	⊢ 𝐺 ∈ UPGraph
22	3	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
23	1	ovexi	⊢ 𝑉 ∈ V
24		s7cli	⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
25	2 24	eqeltri	⊢ 𝐸 ∈ Word V
26		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
27	23 25 26	mp2an	⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉
28	22 27	eqtr2i	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
29	28	eulerpath	⊢ ( ( 𝐺 ∈ UPGraph ∧ ( EulerPaths ‘ 𝐺 ) ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )
30	21 29	mpan	⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } )
31	30	necon1bi	⊢ ( ¬ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } → ( EulerPaths ‘ 𝐺 ) = ∅ )
32	18 31	ax-mp	⊢ ( EulerPaths ‘ 𝐺 ) = ∅