Metamath Proof Explorer

Theorem numclwwlk7lem

Description: Lemma for numclwwlk7 , frgrreggt1 and frgrreg : If a finite, nonempty friendship graph is K-regular, the K is a nonnegative integer. (Contributed by AV, 3-Jun-2021)

		Ref	Expression
	Hypothesis	numclwwlk7lem.v	$⊢ V = Vtx (G)$
	Assertion	numclwwlk7lem	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to K \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk7lem.v	$⊢ V = Vtx (G)$
2	1	finrusgrfusgr	$⊢ (G RegUSGraph K \land V \in Fin) \to G \in FinUSGraph$
3	2	ad2ant2rl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to G \in FinUSGraph$
4		simpll	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to G RegUSGraph K$
5		simprl	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to V \neq \emptyset$
6	1	frusgrnn0	$⊢ (G \in FinUSGraph \land G RegUSGraph K \land V \neq \emptyset) \to K \in ℕ_{0}$
7	3 4 5 6	syl3anc	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to K \in ℕ_{0}$