Metamath Proof Explorer

Theorem cusgrsizeindb1

Description: Base case of the induction in cusgrsize . The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/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	cusgrsizeindb1	$⊢ (G \in USGraph \land \|V\| = 1) \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	usgr1v0e	$⊢ (G \in USGraph \land \|V\| = 1) \to \|E\| = 0$
4		oveq1	$⊢ \|V\| = 1 \to (\binom{\|V\|}{2}) = (\binom{1}{2})$
5		1nn0	$⊢ 1 \in ℕ_{0}$
6		2z	$⊢ 2 \in ℤ$
7		1lt2	$⊢ 1 < 2$
8	7	olci	$⊢ (2 < 0 \lor 1 < 2)$
9		bcval4	$⊢ (1 \in ℕ_{0} \land 2 \in ℤ \land (2 < 0 \lor 1 < 2)) \to (\binom{1}{2}) = 0$
10	5 6 8 9	mp3an	$⊢ (\binom{1}{2}) = 0$
11	4 10	eqtrdi	$⊢ \|V\| = 1 \to (\binom{\|V\|}{2}) = 0$
12	11	eqeq2d	$⊢ \|V\| = 1 \to (\|E\| = (\binom{\|V\|}{2}) \leftrightarrow \|E\| = 0)$
13	12	adantl	$⊢ (G \in USGraph \land \|V\| = 1) \to (\|E\| = (\binom{\|V\|}{2}) \leftrightarrow \|E\| = 0)$
14	3 13	mpbird	$⊢ (G \in USGraph \land \|V\| = 1) \to \|E\| = (\binom{\|V\|}{2})$