Theorem 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	cusgrsizeindb0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	cusgrsizeindb0	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )

Proof

Step	Hyp	Ref	Expression
1		cusgrsizeindb0.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		cusgrsizeindb0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	uhgr0vsize0	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = 0 )
4		oveq1	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ( ( ♯ ‘ 𝑉 ) C 2 ) = ( 0 C 2 ) )
5		2nn	⊢ 2 ∈ ℕ
6		bc0k	⊢ ( 2 ∈ ℕ → ( 0 C 2 ) = 0 )
7	5 6	ax-mp	⊢ ( 0 C 2 ) = 0
8	4 7	eqtr2di	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → 0 = ( ( ♯ ‘ 𝑉 ) C 2 ) )
9	8	adantl	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → 0 = ( ( ♯ ‘ 𝑉 ) C 2 ) )
10	3 9	eqtrd	⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 0 ) → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝑉 ) C 2 ) )