Metamath Proof Explorer

Theorem vdgn0frgrv2

Description: A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

		Ref	Expression
	Hypothesis	vdn1frgrv2.v	$⊢ V = Vtx (G)$
	Assertion	vdgn0frgrv2	$⊢ (G \in FriendGraph \land N \in V) \to (1 < \|V\| \to VtxDeg (G) (N) \neq 0)$

Proof

Step	Hyp	Ref	Expression
1		vdn1frgrv2.v	$⊢ V = Vtx (G)$
2		frgrconngr	$⊢ G \in FriendGraph \to G \in ConnGraph$
3		frgrusgr	$⊢ G \in FriendGraph \to G \in USGraph$
4		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
5	3 4	syl	$⊢ G \in FriendGraph \to G \in UMGraph$
6	1	vdn0conngrumgrv2	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to VtxDeg (G) (N) \neq 0$
7	6	ex	$⊢ (G \in ConnGraph \land G \in UMGraph) \to ((N \in V \land 1 < \|V\|) \to VtxDeg (G) (N) \neq 0)$
8	2 5 7	syl2anc	$⊢ G \in FriendGraph \to ((N \in V \land 1 < \|V\|) \to VtxDeg (G) (N) \neq 0)$
9	8	expdimp	$⊢ (G \in FriendGraph \land N \in V) \to (1 < \|V\| \to VtxDeg (G) (N) \neq 0)$