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 ∈ FriendGraph ∧ V ∈ Fin ∧ 3 < V → ∀ k ∈ ℕ 0 ¬ G RegUSGraph k

Proof

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