This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. UHGraph /\ ( # ` V ) = 0 ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )

Proof

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