Metamath Proof Explorer

Theorem frgrogt3nreg

Description: If a finite friendship graph has an order greater than 3, it cannot be k-regular for any k . (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v 
|- V = ( Vtx ` G )
Assertion frgrogt3nreg 
|- ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> A. k e. NN0 -. G RegUSGraph k )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 simp1 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> G e. FriendGraph )
3 simp2 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> V e. Fin )
4 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
5 0red 
 |-  ( ( # ` V ) e. NN0 -> 0 e. RR )
6 3re 
 |-  3 e. RR
7 6 a1i 
 |-  ( ( # ` V ) e. NN0 -> 3 e. RR )
8 nn0re 
 |-  ( ( # ` V ) e. NN0 -> ( # ` V ) e. RR )
9 5 7 8 3jca 
 |-  ( ( # ` V ) e. NN0 -> ( 0 e. RR /\ 3 e. RR /\ ( # ` V ) e. RR ) )
10 9 adantr 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( 0 e. RR /\ 3 e. RR /\ ( # ` V ) e. RR ) )
11 3pos 
 |-  0 < 3
12 11 a1i 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 0 < 3 )
13 simpr 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 3 < ( # ` V ) )
14 lttr 
 |-  ( ( 0 e. RR /\ 3 e. RR /\ ( # ` V ) e. RR ) -> ( ( 0 < 3 /\ 3 < ( # ` V ) ) -> 0 < ( # ` V ) ) )
15 14 imp 
 |-  ( ( ( 0 e. RR /\ 3 e. RR /\ ( # ` V ) e. RR ) /\ ( 0 < 3 /\ 3 < ( # ` V ) ) ) -> 0 < ( # ` V ) )
16 10 12 13 15 syl12anc 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 0 < ( # ` V ) )
17 16 ex 
 |-  ( ( # ` V ) e. NN0 -> ( 3 < ( # ` V ) -> 0 < ( # ` V ) ) )
18 ltne 
 |-  ( ( 0 e. RR /\ 0 < ( # ` V ) ) -> ( # ` V ) =/= 0 )
19 5 17 18 syl6an 
 |-  ( ( # ` V ) e. NN0 -> ( 3 < ( # ` V ) -> ( # ` V ) =/= 0 ) )
20 hasheq0 
 |-  ( V e. Fin -> ( ( # ` V ) = 0 <-> V = (/) ) )
21 20 necon3bid 
 |-  ( V e. Fin -> ( ( # ` V ) =/= 0 <-> V =/= (/) ) )
22 21 biimpcd 
 |-  ( ( # ` V ) =/= 0 -> ( V e. Fin -> V =/= (/) ) )
23 19 22 syl6 
 |-  ( ( # ` V ) e. NN0 -> ( 3 < ( # ` V ) -> ( V e. Fin -> V =/= (/) ) ) )
24 23 com23 
 |-  ( ( # ` V ) e. NN0 -> ( V e. Fin -> ( 3 < ( # ` V ) -> V =/= (/) ) ) )
25 4 24 mpcom 
 |-  ( V e. Fin -> ( 3 < ( # ` V ) -> V =/= (/) ) )
26 25 a1i 
 |-  ( G e. FriendGraph -> ( V e. Fin -> ( 3 < ( # ` V ) -> V =/= (/) ) ) )
27 26 3imp 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> V =/= (/) )
28 2 3 27 3jca 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) )
29 28 ad2antrl 
 |-  ( ( G RegUSGraph k /\ ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) ) -> ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) )
30 simpl 
 |-  ( ( G RegUSGraph k /\ ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) ) -> G RegUSGraph k )
31 1 frgrregord13 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph k ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
32 29 30 31 syl2anc 
 |-  ( ( G RegUSGraph k /\ ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
33 1red 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 1 e. RR )
34 6 a1i 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 3 e. RR )
35 8 adantr 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( # ` V ) e. RR )
36 1lt3 
 |-  1 < 3
37 36 a1i 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 1 < 3 )
38 33 34 35 37 13 lttrd 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> 1 < ( # ` V ) )
39 33 38 gtned 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( # ` V ) =/= 1 )
40 eqneqall 
 |-  ( ( # ` V ) = 1 -> ( ( # ` V ) =/= 1 -> -. G RegUSGraph k ) )
41 39 40 syl5com 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( ( # ` V ) = 1 -> -. G RegUSGraph k ) )
42 ltne 
 |-  ( ( 3 e. RR /\ 3 < ( # ` V ) ) -> ( # ` V ) =/= 3 )
43 7 42 sylan 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( # ` V ) =/= 3 )
44 eqneqall 
 |-  ( ( # ` V ) = 3 -> ( ( # ` V ) =/= 3 -> -. G RegUSGraph k ) )
45 43 44 syl5com 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( ( # ` V ) = 3 -> -. G RegUSGraph k ) )
46 41 45 jaod 
 |-  ( ( ( # ` V ) e. NN0 /\ 3 < ( # ` V ) ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) )
47 46 ex 
 |-  ( ( # ` V ) e. NN0 -> ( 3 < ( # ` V ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) ) )
48 4 47 syl 
 |-  ( V e. Fin -> ( 3 < ( # ` V ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) ) )
49 48 a1i 
 |-  ( G e. FriendGraph -> ( V e. Fin -> ( 3 < ( # ` V ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) ) ) )
50 49 3imp 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) )
51 50 ad2antrl 
 |-  ( ( G RegUSGraph k /\ ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) ) -> ( ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> -. G RegUSGraph k ) )
52 32 51 mpd 
 |-  ( ( G RegUSGraph k /\ ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) ) -> -. G RegUSGraph k )
53 52 ex 
 |-  ( G RegUSGraph k -> ( ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) -> -. G RegUSGraph k ) )
54 ax-1 
 |-  ( -. G RegUSGraph k -> ( ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) -> -. G RegUSGraph k ) )
55 53 54 pm2.61i 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) /\ k e. NN0 ) -> -. G RegUSGraph k )
56 55 ralrimiva 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ 3 < ( # ` V ) ) -> A. k e. NN0 -. G RegUSGraph k )