cusgrsizeindb0

Description: Base case of the induction in cusgrsize . The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 7-Nov-2020)

	Ref	Expression
Hypotheses	cusgrsizeindb0.v	$⊢ V = Vtx (G)$
	cusgrsizeindb0.e	$⊢ E = Edg (G)$
Assertion	cusgrsizeindb0	$⊢ (G \in UHGraph \land \|V\| = 0) \to \|E\| = (\binom{\|V\|}{2})$

Proof

Step	Hyp	Ref	Expression
1		cusgrsizeindb0.v	$⊢ V = Vtx (G)$
2		cusgrsizeindb0.e	$⊢ E = Edg (G)$
3	1 2	uhgr0vsize0	$⊢ (G \in UHGraph \land \|V\| = 0) \to \|E\| = 0$
4		oveq1	$⊢ \|V\| = 0 \to (\binom{\|V\|}{2}) = (\binom{0}{2})$
5		2nn	$⊢ 2 \in ℕ$
6		bc0k	$⊢ 2 \in ℕ \to (\binom{0}{2}) = 0$
7	5 6	ax-mp	$⊢ (\binom{0}{2}) = 0$
8	4 7	syl6req	$⊢ \|V\| = 0 \to 0 = (\binom{\|V\|}{2})$
9	8	adantl	$⊢ (G \in UHGraph \land \|V\| = 0) \to 0 = (\binom{\|V\|}{2})$
10	3 9	eqtrd	$⊢ (G \in UHGraph \land \|V\| = 0) \to \|E\| = (\binom{\|V\|}{2})$

Metamath Proof Explorer

Theorem cusgrsizeindb0

Proof