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

Proof

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