Theorem vdgn1frgrv3

Description: Any vertex in a friendship graph does not have degree 1, see remark 2 in MertziosUnger p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018) (Revised by AV, 4-Apr-2021)

	Ref	Expression
Hypothesis	vdn1frgrv2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	vdgn1frgrv3	$$⊢\left(G\in \mathrm{FriendGraph}\wedge 1<\left|V\right|\right)\to \forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\ne 1$$

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	vdgn1frgrv2	$$⊢\left(G\in \mathrm{FriendGraph}\wedge v\in V\right)\to \left(1<\left|V\right|\to \mathrm{VtxDeg}\left(G\right)\left(v\right)\ne 1\right)$$
3	2	impancom	$$⊢\left(G\in \mathrm{FriendGraph}\wedge 1<\left|V\right|\right)\to \left(v\in V\to \mathrm{VtxDeg}\left(G\right)\left(v\right)\ne 1\right)$$
4	3	ralrimiv	$$⊢\left(G\in \mathrm{FriendGraph}\wedge 1<\left|V\right|\right)\to \forall v\in V\mathrm{VtxDeg}\left(G\right)\left(v\right)\ne 1$$