Metamath Proof Explorer

Theorem vdgfrgrgt2

Description: Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in MertziosUnger p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017) (Revised by AV, 5-Apr-2021)

Ref Expression
Hypothesis vdn1frgrv2.v 
|- V = ( Vtx ` G )
Assertion vdgfrgrgt2 
|- ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> 2 <_ ( ( VtxDeg ` G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v 
 |-  V = ( Vtx ` G )
2 1 vdgn0frgrv2 
 |-  ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 ) )
3 2 imp 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 0 )
4 1 vdgn1frgrv2 
 |-  ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` N ) =/= 1 ) )
5 4 imp 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( VtxDeg ` G ) ` N ) =/= 1 )
6 1 vtxdgelxnn0 
 |-  ( N e. V -> ( ( VtxDeg ` G ) ` N ) e. NN0* )
7 xnn0n0n1ge2b 
 |-  ( ( ( VtxDeg ` G ) ` N ) e. NN0* -> ( ( ( ( VtxDeg ` G ) ` N ) =/= 0 /\ ( ( VtxDeg ` G ) ` N ) =/= 1 ) <-> 2 <_ ( ( VtxDeg ` G ) ` N ) ) )
8 6 7 syl 
 |-  ( N e. V -> ( ( ( ( VtxDeg ` G ) ` N ) =/= 0 /\ ( ( VtxDeg ` G ) ` N ) =/= 1 ) <-> 2 <_ ( ( VtxDeg ` G ) ` N ) ) )
9 8 ad2antlr 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> ( ( ( ( VtxDeg ` G ) ` N ) =/= 0 /\ ( ( VtxDeg ` G ) ` N ) =/= 1 ) <-> 2 <_ ( ( VtxDeg ` G ) ` N ) ) )
10 3 5 9 mpbi2and 
 |-  ( ( ( G e. FriendGraph /\ N e. V ) /\ 1 < ( # ` V ) ) -> 2 <_ ( ( VtxDeg ` G ) ` N ) )
11 10 ex 
 |-  ( ( G e. FriendGraph /\ N e. V ) -> ( 1 < ( # ` V ) -> 2 <_ ( ( VtxDeg ` G ) ` N ) ) )