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 ) )