Metamath Proof Explorer

Theorem konigsberglem5

Description: Lemma 5 for konigsberg : The set of vertices of odd degree is greater than 2. (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 konigsberglem5 ⊢ 2 < 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 1 2 3 konigsberglem4 ⊢ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
5 1 ovexi ⊢ V ∈ V
6 5 rabex ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ V
7 hashss ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ V ∧ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → 0 1 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
8 6 7 mpan ⊢ 0 1 3 ⊆ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → 0 1 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
9 0ne1 ⊢ 0 ≠ 1
10 1re ⊢ 1 ∈ ℝ
11 1lt3 ⊢ 1 < 3
12 10 11 ltneii ⊢ 1 ≠ 3
13 3ne0 ⊢ 3 ≠ 0
14 9 12 13 3pm3.2i ⊢ 0 ≠ 1 ∧ 1 ≠ 3 ∧ 3 ≠ 0
15 c0ex ⊢ 0 ∈ V
16 1ex ⊢ 1 ∈ V
17 3ex ⊢ 3 ∈ V
18 hashtpg ⊢ 0 ∈ V ∧ 1 ∈ V ∧ 3 ∈ V → 0 ≠ 1 ∧ 1 ≠ 3 ∧ 3 ≠ 0 ↔ 0 1 3 = 3
19 15 16 17 18 mp3an ⊢ 0 ≠ 1 ∧ 1 ≠ 3 ∧ 3 ≠ 0 ↔ 0 1 3 = 3
20 14 19 mpbi ⊢ 0 1 3 = 3
21 20 breq1i ⊢ 0 1 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ↔ 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
22 df-3 ⊢ 3 = 2 + 1
23 22 breq1i ⊢ 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ↔ 2 + 1 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
24 2z ⊢ 2 ∈ ℤ
25 fzfi ⊢ 0 … 3 ∈ Fin
26 1 25 eqeltri ⊢ V ∈ Fin
27 rabfi ⊢ V ∈ Fin → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ Fin
28 hashcl ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ Fin → x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ ℕ 0
29 26 27 28 mp2b ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ ℕ 0
30 29 nn0zi ⊢ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ ℤ
31 zltp1le ⊢ 2 ∈ ℤ ∧ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ∈ ℤ → 2 < x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ↔ 2 + 1 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
32 24 30 31 mp2an ⊢ 2 < x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x ↔ 2 + 1 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
33 23 32 sylbb2 ⊢ 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → 2 < x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
34 21 33 sylbi ⊢ 0 1 3 ≤ x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x → 2 < x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x
35 4 8 34 mp2b ⊢ 2 < x ∈ V | ¬ 2 ∥ VtxDeg ⁡ G ⁡ x