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 ⊢ 𝑉 = ( 0 ... 3 )
konigsberg.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
konigsberg.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion konigsberglem5 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )

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 konigsberglem4 ⊢ { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) }
5 1 ovexi ⊢ 𝑉 ∈ V
6 5 rabex ⊢ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V
7 hashss ⊢ ( ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V ∧ { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) → ( ♯ ‘ { 0 , 1 , 3 } ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
8 6 7 mpan ⊢ ( { 0 , 1 , 3 } ⊆ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } → ( ♯ ‘ { 0 , 1 , 3 } ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
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 } ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ 3 ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
22 df-3 ⊢ 3 = ( 2 + 1 )
23 22 breq1i ⊢ ( 3 ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ ( 2 + 1 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
24 2z ⊢ 2 ∈ ℤ
25 fzfi ⊢ ( 0 ... 3 ) ∈ Fin
26 1 25 eqeltri ⊢ 𝑉 ∈ Fin
27 rabfi ⊢ ( 𝑉 ∈ Fin → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ Fin )
28 hashcl ⊢ ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℕ0 )
29 26 27 28 mp2b ⊢ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℕ0
30 29 nn0zi ⊢ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℤ
31 zltp1le ⊢ ( ( 2 ∈ ℤ ∧ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ ℤ ) → ( 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ ( 2 + 1 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ) )
32 24 30 31 mp2an ⊢ ( 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ↔ ( 2 + 1 ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
33 23 32 sylbb2 ⊢ ( 3 ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) → 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
34 21 33 sylbi ⊢ ( ( ♯ ‘ { 0 , 1 , 3 } ) ≤ ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) → 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
35 4 8 34 mp2b ⊢ 2 < ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } )