Metamath Proof Explorer

Theorem vdgfrgrgt2

Description: Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in MertziosUnger p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 5-Apr-2021)

Ref Expression
Hypothesis vdn1frgrv2.v ⊢ V = Vtx ⁡ G
Assertion vdgfrgrgt2 ⊢ G ∈ FriendGraph ∧ N ∈ V → 1 < V → 2 ≤ VtxDeg ⁡ G ⁡ N

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v ⊢ V = Vtx ⁡ G
2 1 vdgn0frgrv2 ⊢ G ∈ FriendGraph ∧ N ∈ V → 1 < V → VtxDeg ⁡ G ⁡ N ≠ 0
3 2 imp ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N ≠ 0
4 1 vdgn1frgrv2 ⊢ G ∈ FriendGraph ∧ N ∈ V → 1 < V → VtxDeg ⁡ G ⁡ N ≠ 1
5 4 imp ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N ≠ 1
6 1 vtxdgelxnn0 ⊢ N ∈ V → VtxDeg ⁡ G ⁡ N ∈ ℕ 0 *
7 xnn0n0n1ge2b ⊢ VtxDeg ⁡ G ⁡ N ∈ ℕ 0 * → VtxDeg ⁡ G ⁡ N ≠ 0 ∧ VtxDeg ⁡ G ⁡ N ≠ 1 ↔ 2 ≤ VtxDeg ⁡ G ⁡ N
8 6 7 syl ⊢ N ∈ V → VtxDeg ⁡ G ⁡ N ≠ 0 ∧ VtxDeg ⁡ G ⁡ N ≠ 1 ↔ 2 ≤ VtxDeg ⁡ G ⁡ N
9 8 ad2antlr ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → VtxDeg ⁡ G ⁡ N ≠ 0 ∧ VtxDeg ⁡ G ⁡ N ≠ 1 ↔ 2 ≤ VtxDeg ⁡ G ⁡ N
10 3 5 9 mpbi2and ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → 2 ≤ VtxDeg ⁡ G ⁡ N
11 10 ex ⊢ G ∈ FriendGraph ∧ N ∈ V → 1 < V → 2 ≤ VtxDeg ⁡ G ⁡ N