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=VtxG
cusgrsizeindb0.e E=EdgG
Assertion cusgrsizeindb1 GUSGraphV=1E=(V2)

Proof

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