Metamath Proof Explorer

Theorem konigsberglem4

Description: Lemma 4 for konigsberg : Vertices 0 , 1 , 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 28-Feb-2021)

Ref Expression
Hypotheses konigsberg.v ⊢V=0…3
konigsberg.e ⊢E=⟨“01020312122323”⟩
konigsberg.g ⊢G=VE
Assertion konigsberglem4 ⊢013⊆x∈V|¬2∥VtxDeg⁡G⁡x

Proof

Step Hyp Ref Expression
1 konigsberg.v ⊢V=0…3
2 konigsberg.e ⊢E=⟨“01020312122323”⟩
3 konigsberg.g ⊢G=VE
4 3nn0 ⊢3∈ℕ0
5 0elfz ⊢3∈ℕ0→0∈0…3
6 4 5 ax-mp ⊢0∈0…3
7 6 1 eleqtrri ⊢0∈V
8 n2dvds3 ⊢¬2∥3
9 1 2 3 konigsberglem1 ⊢VtxDeg⁡G⁡0=3
10 9 breq2i ⊢2∥VtxDeg⁡G⁡0↔2∥3
11 8 10 mtbir ⊢¬2∥VtxDeg⁡G⁡0
12 fveq2 ⊢x=0→VtxDeg⁡G⁡x=VtxDeg⁡G⁡0
13 12 breq2d ⊢x=0→2∥VtxDeg⁡G⁡x↔2∥VtxDeg⁡G⁡0
14 13 notbid ⊢x=0→¬2∥VtxDeg⁡G⁡x↔¬2∥VtxDeg⁡G⁡0
15 14 elrab ⊢0∈x∈V|¬2∥VtxDeg⁡G⁡x↔0∈V∧¬2∥VtxDeg⁡G⁡0
16 7 11 15 mpbir2an ⊢0∈x∈V|¬2∥VtxDeg⁡G⁡x
17 1nn0 ⊢1∈ℕ0
18 1le3 ⊢1≤3
19 elfz2nn0 ⊢1∈0…3↔1∈ℕ0∧3∈ℕ0∧1≤3
20 17 4 18 19 mpbir3an ⊢1∈0…3
21 20 1 eleqtrri ⊢1∈V
22 1 2 3 konigsberglem2 ⊢VtxDeg⁡G⁡1=3
23 22 breq2i ⊢2∥VtxDeg⁡G⁡1↔2∥3
24 8 23 mtbir ⊢¬2∥VtxDeg⁡G⁡1
25 fveq2 ⊢x=1→VtxDeg⁡G⁡x=VtxDeg⁡G⁡1
26 25 breq2d ⊢x=1→2∥VtxDeg⁡G⁡x↔2∥VtxDeg⁡G⁡1
27 26 notbid ⊢x=1→¬2∥VtxDeg⁡G⁡x↔¬2∥VtxDeg⁡G⁡1
28 27 elrab ⊢1∈x∈V|¬2∥VtxDeg⁡G⁡x↔1∈V∧¬2∥VtxDeg⁡G⁡1
29 21 24 28 mpbir2an ⊢1∈x∈V|¬2∥VtxDeg⁡G⁡x
30 3re ⊢3∈ℝ
31 30 leidi ⊢3≤3
32 elfz2nn0 ⊢3∈0…3↔3∈ℕ0∧3∈ℕ0∧3≤3
33 4 4 31 32 mpbir3an ⊢3∈0…3
34 33 1 eleqtrri ⊢3∈V
35 1 2 3 konigsberglem3 ⊢VtxDeg⁡G⁡3=3
36 35 breq2i ⊢2∥VtxDeg⁡G⁡3↔2∥3
37 8 36 mtbir ⊢¬2∥VtxDeg⁡G⁡3
38 fveq2 ⊢x=3→VtxDeg⁡G⁡x=VtxDeg⁡G⁡3
39 38 breq2d ⊢x=3→2∥VtxDeg⁡G⁡x↔2∥VtxDeg⁡G⁡3
40 39 notbid ⊢x=3→¬2∥VtxDeg⁡G⁡x↔¬2∥VtxDeg⁡G⁡3
41 40 elrab ⊢3∈x∈V|¬2∥VtxDeg⁡G⁡x↔3∈V∧¬2∥VtxDeg⁡G⁡3
42 34 37 41 mpbir2an ⊢3∈x∈V|¬2∥VtxDeg⁡G⁡x
43 16 29 42 3pm3.2i ⊢0∈x∈V|¬2∥VtxDeg⁡G⁡x∧1∈x∈V|¬2∥VtxDeg⁡G⁡x∧3∈x∈V|¬2∥VtxDeg⁡G⁡x
44 c0ex ⊢0∈V
45 1ex ⊢1∈V
46 3ex ⊢3∈V
47 44 45 46 tpss ⊢0∈x∈V|¬2∥VtxDeg⁡G⁡x∧1∈x∈V|¬2∥VtxDeg⁡G⁡x∧3∈x∈V|¬2∥VtxDeg⁡G⁡x↔013⊆x∈V|¬2∥VtxDeg⁡G⁡x
48 43 47 mpbi ⊢013⊆x∈V|¬2∥VtxDeg⁡G⁡x