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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frgrogt3nreg ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑘 ∈ ℕ0 ¬ 𝐺 RegUSGraph 𝑘 )

Proof

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