Proof of Theorem frgrogt3nreg
Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝐺 ∈ FriendGraph
) |
2 | | simp2 1062 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ∈ Fin) |
3 | | hashcl 13147 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
4 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℕ0 → 0 ∈ ℝ) |
5 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) ∈
ℕ0 → 3 ∈ ℝ) |
7 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) ∈
ℕ0 → (#‘𝑉) ∈ ℝ) |
8 | 4, 6, 7 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑉) ∈
ℕ0 → (0 ∈ ℝ ∧ 3 ∈ ℝ ∧
(#‘𝑉) ∈
ℝ)) |
9 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (0 ∈ ℝ ∧ 3 ∈
ℝ ∧ (#‘𝑉)
∈ ℝ)) |
10 | | 3pos 11114 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
3 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 0 < 3) |
12 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 3 < (#‘𝑉)) |
13 | | lttr 10114 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) → ((0 < 3 ∧ 3
< (#‘𝑉)) → 0
< (#‘𝑉))) |
14 | 13 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ (((0
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) ∧ (0 < 3 ∧ 3
< (#‘𝑉))) → 0
< (#‘𝑉)) |
15 | 9, 11, 12, 14 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 0 < (#‘𝑉)) |
16 | 15 | ex 450 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → 0 < (#‘𝑉))) |
17 | | ltne 10134 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 0 < (#‘𝑉)) → (#‘𝑉) ≠ 0) |
18 | 4, 16, 17 | syl6an 568 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (#‘𝑉) ≠ 0)) |
19 | | hasheq0 13154 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
20 | 19 | necon3bid 2838 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
21 | 20 | biimpcd 239 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ≠ 0
→ (𝑉 ∈ Fin →
𝑉 ≠
∅)) |
22 | 18, 21 | syl6 35 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (𝑉 ∈ Fin → 𝑉 ≠ ∅))) |
23 | 22 | com23 86 |
. . . . . . . . . . 11
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ∈ Fin → (3 < (#‘𝑉) → 𝑉 ≠ ∅))) |
24 | 3, 23 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → (3 <
(#‘𝑉) → 𝑉 ≠ ∅)) |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph →
(𝑉 ∈ Fin → (3
< (#‘𝑉) →
𝑉 ≠
∅))) |
26 | 25 | 3imp 1256 |
. . . . . . . 8
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → 𝑉 ≠ ∅) |
27 | 1, 2, 26 | 3jca 1242 |
. . . . . . 7
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) → (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) |
28 | 27 | ad2antrl 764 |
. . . . . 6
⊢ ((𝐺 RegUSGraph 𝑘 ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) → (𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) |
29 | | simpl 473 |
. . . . . 6
⊢ ((𝐺 RegUSGraph 𝑘 ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) → 𝐺 RegUSGraph 𝑘) |
30 | | frgrreggt1.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
31 | 30 | frgrregord13 27254 |
. . . . . 6
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 𝐺 RegUSGraph 𝑘) → ((#‘𝑉) = 1 ∨ (#‘𝑉) = 3)) |
32 | 28, 29, 31 | syl2anc 693 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝑘 ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) →
((#‘𝑉) = 1 ∨
(#‘𝑉) =
3)) |
33 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 ∈ ℝ) |
34 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 3 ∈ ℝ) |
35 | 7 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ∈ ℝ) |
36 | | 1lt3 11196 |
. . . . . . . . . . . . . . 15
⊢ 1 <
3 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 < 3) |
38 | 33, 34, 35, 37, 12 | lttrd 10198 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 < (#‘𝑉)) |
39 | 33, 38 | gtned 10172 |
. . . . . . . . . . . 12
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 1) |
40 | | eqneqall 2805 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) = 1
→ ((#‘𝑉) ≠ 1
→ ¬ 𝐺 RegUSGraph
𝑘)) |
41 | 39, 40 | syl5com 31 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → ((#‘𝑉) = 1 → ¬ 𝐺 RegUSGraph 𝑘)) |
42 | | ltne 10134 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℝ ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 3) |
43 | 6, 42 | sylan 488 |
. . . . . . . . . . . 12
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 3) |
44 | | eqneqall 2805 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) = 3
→ ((#‘𝑉) ≠ 3
→ ¬ 𝐺 RegUSGraph
𝑘)) |
45 | 43, 44 | syl5com 31 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → ((#‘𝑉) = 3 → ¬ 𝐺 RegUSGraph 𝑘)) |
46 | 41, 45 | jaod 395 |
. . . . . . . . . 10
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 𝐺 RegUSGraph 𝑘)) |
47 | 46 | ex 450 |
. . . . . . . . 9
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 𝐺 RegUSGraph 𝑘))) |
48 | 3, 47 | syl 17 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → (3 <
(#‘𝑉) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 𝐺 RegUSGraph 𝑘))) |
49 | 48 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph →
(𝑉 ∈ Fin → (3
< (#‘𝑉) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 𝐺 RegUSGraph 𝑘)))) |
50 | 49 | 3imp 1256 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 𝐺 RegUSGraph 𝑘)) |
51 | 50 | ad2antrl 764 |
. . . . 5
⊢ ((𝐺 RegUSGraph 𝑘 ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 𝐺 RegUSGraph 𝑘)) |
52 | 32, 51 | mpd 15 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝑘 ∧ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) → ¬
𝐺 RegUSGraph 𝑘) |
53 | 52 | ex 450 |
. . 3
⊢ (𝐺 RegUSGraph 𝑘 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0) → ¬
𝐺 RegUSGraph 𝑘)) |
54 | | ax-1 6 |
. . 3
⊢ (¬
𝐺 RegUSGraph 𝑘 → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0) → ¬
𝐺 RegUSGraph 𝑘)) |
55 | 53, 54 | pm2.61i 176 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) ∧ 𝑘 ∈ ℕ0)
→ ¬ 𝐺 RegUSGraph
𝑘) |
56 | 55 | ralrimiva 2966 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 <
(#‘𝑉)) →
∀𝑘 ∈
ℕ0 ¬ 𝐺
RegUSGraph 𝑘) |