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 = ⟨“ 0 1 0 2 0 3 1 2 1 2 2 3 2 3 ”⟩
konigsberg.g ⊢ G = V E
Assertion konigsberglem4 ⊢ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x

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 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 ↔ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
48 43 47 mpbi ⊢ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x