Metamath Proof Explorer


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 V = Vtx G
cusgrsizeindb0.e E = Edg G
Assertion cusgrsizeindb0 G UHGraph V = 0 E = ( V 2 )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v V = Vtx G
2 cusgrsizeindb0.e E = Edg G
3 1 2 uhgr0vsize0 G UHGraph V = 0 E = 0
4 oveq1 V = 0 ( V 2 ) = ( 0 2 )
5 2nn 2
6 bc0k 2 ( 0 2 ) = 0
7 5 6 ax-mp ( 0 2 ) = 0
8 4 7 eqtr2di V = 0 0 = ( V 2 )
9 8 adantl G UHGraph V = 0 0 = ( V 2 )
10 3 9 eqtrd G UHGraph V = 0 E = ( V 2 )