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 USGraph V = 1 E = ( V 2 )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v V = Vtx G
2 cusgrsizeindb0.e E = Edg G
3 1 2 usgr1v0e G USGraph V = 1 E = 0
4 oveq1 V = 1 ( V 2 ) = ( 1 2 )
5 1nn0 1 0
6 2z 2
7 1lt2 1 < 2
8 7 olci 2 < 0 1 < 2
9 bcval4 1 0 2 2 < 0 1 < 2 ( 1 2 ) = 0
10 5 6 8 9 mp3an ( 1 2 ) = 0
11 4 10 eqtrdi V = 1 ( V 2 ) = 0
12 11 eqeq2d V = 1 E = ( V 2 ) E = 0
13 12 adantl G USGraph V = 1 E = ( V 2 ) E = 0
14 3 13 mpbird G USGraph V = 1 E = ( V 2 )