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