Metamath Proof Explorer


Theorem frgrwopreglem2

Description: Lemma 2 for frgrwopreg . If the set A of vertices of degree K is not empty in a friendship graph with at least two vertices, then K must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 2-Jan-2022)

Ref Expression
Hypotheses frgrwopreg.v V = Vtx G
frgrwopreg.d D = VtxDeg G
frgrwopreg.a A = x V | D x = K
frgrwopreg.b B = V A
Assertion frgrwopreglem2 G FriendGraph 1 < V A 2 K

Proof

Step Hyp Ref Expression
1 frgrwopreg.v V = Vtx G
2 frgrwopreg.d D = VtxDeg G
3 frgrwopreg.a A = x V | D x = K
4 frgrwopreg.b B = V A
5 n0 A x x A
6 3 rabeq2i x A x V D x = K
7 1 vdgfrgrgt2 G FriendGraph x V 1 < V 2 VtxDeg G x
8 7 imp G FriendGraph x V 1 < V 2 VtxDeg G x
9 breq2 K = D x 2 K 2 D x
10 2 fveq1i D x = VtxDeg G x
11 10 breq2i 2 D x 2 VtxDeg G x
12 9 11 bitrdi K = D x 2 K 2 VtxDeg G x
13 12 eqcoms D x = K 2 K 2 VtxDeg G x
14 8 13 syl5ibrcom G FriendGraph x V 1 < V D x = K 2 K
15 14 exp31 G FriendGraph x V 1 < V D x = K 2 K
16 15 com14 D x = K x V 1 < V G FriendGraph 2 K
17 16 impcom x V D x = K 1 < V G FriendGraph 2 K
18 6 17 sylbi x A 1 < V G FriendGraph 2 K
19 18 exlimiv x x A 1 < V G FriendGraph 2 K
20 5 19 sylbi A 1 < V G FriendGraph 2 K
21 20 3imp31 G FriendGraph 1 < V A 2 K