Metamath Proof Explorer

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 = ( 0 ... 3 )
konigsberg.e 
|- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
konigsberg.g 
|- G = <. V , E >.
Assertion konigsberg 
|- ( EulerPaths ` G ) = (/)

Proof

Step Hyp Ref Expression
1 konigsberg.v 
 |-  V = ( 0 ... 3 )
2 konigsberg.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
3 konigsberg.g 
 |-  G = <. V , E >.
4 1 2 3 konigsberglem5 
 |-  2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } )
5 elpri 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } -> ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 0 \/ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 2 ) )
6 2pos 
 |-  0 < 2
7 0re 
 |-  0 e. RR
8 2re 
 |-  2 e. RR
9 7 8 ltnsymi 
 |-  ( 0 < 2 -> -. 2 < 0 )
10 6 9 ax-mp 
 |-  -. 2 < 0
11 breq2 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 0 -> ( 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> 2 < 0 ) )
12 10 11 mtbiri 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 0 -> -. 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
13 8 ltnri 
 |-  -. 2 < 2
14 breq2 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 2 -> ( 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) <-> 2 < 2 ) )
15 13 14 mtbiri 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 2 -> -. 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
16 12 15 jaoi 
 |-  ( ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 0 \/ ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = 2 ) -> -. 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
17 5 16 syl 
 |-  ( ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } -> -. 2 < ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) )
18 4 17 mt2 
 |-  -. ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 }
19 1 2 3 konigsbergumgr 
 |-  G e. UMGraph
20 umgrupgr 
 |-  ( G e. UMGraph -> G e. UPGraph )
21 19 20 ax-mp 
 |-  G e. UPGraph
22 3 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` <. V , E >. )
23 1 ovexi 
 |-  V e. _V
24 s7cli 
 |-  <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> e. Word _V
25 2 24 eqeltri 
 |-  E e. Word _V
26 opvtxfv 
 |-  ( ( V e. _V /\ E e. Word _V ) -> ( Vtx ` <. V , E >. ) = V )
27 23 25 26 mp2an 
 |-  ( Vtx ` <. V , E >. ) = V
28 22 27 eqtr2i 
 |-  V = ( Vtx ` G )
29 28 eulerpath 
 |-  ( ( G e. UPGraph /\ ( EulerPaths ` G ) =/= (/) ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )
30 21 29 mpan 
 |-  ( ( EulerPaths ` G ) =/= (/) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )
31 30 necon1bi 
 |-  ( -. ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } -> ( EulerPaths ` G ) = (/) )
32 18 31 ax-mp 
 |-  ( EulerPaths ` G ) = (/)