Proof of Theorem frgraogt3nreg
Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 FriendGrph 𝐸) |
2 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 ∈ Fin) |
3 | | hashcl 13009 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
4 | | 0red 9920 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℕ0 → 0 ∈ ℝ) |
5 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) ∈
ℕ0 → 3 ∈ ℝ) |
7 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) ∈
ℕ0 → (#‘𝑉) ∈ ℝ) |
8 | 4, 6, 7 | 3jca 1235 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝑉) ∈
ℕ0 → (0 ∈ ℝ ∧ 3 ∈ ℝ ∧
(#‘𝑉) ∈
ℝ)) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (0 ∈ ℝ ∧ 3 ∈
ℝ ∧ (#‘𝑉)
∈ ℝ)) |
10 | | 3pos 10991 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
3 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 0 < 3) |
12 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 3 < (#‘𝑉)) |
13 | | lttr 9993 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) → ((0 < 3 ∧ 3
< (#‘𝑉)) → 0
< (#‘𝑉))) |
14 | 13 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ (((0
∈ ℝ ∧ 3 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) ∧ (0 < 3 ∧ 3
< (#‘𝑉))) → 0
< (#‘𝑉)) |
15 | 9, 11, 12, 14 | syl12anc 1316 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 0 < (#‘𝑉)) |
16 | 15 | ex 449 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → 0 < (#‘𝑉))) |
17 | | ltne 10013 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 0 < (#‘𝑉)) → (#‘𝑉) ≠ 0) |
18 | 4, 16, 17 | syl6an 566 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (#‘𝑉) ≠ 0)) |
19 | | hasheq0 13015 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
20 | 19 | necon3bid 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((#‘𝑉) ≠ 0 ↔
𝑉 ≠
∅)) |
21 | 20 | biimpcd 238 |
. . . . . . . . . . . . 13
⊢
((#‘𝑉) ≠ 0
→ (𝑉 ∈ Fin →
𝑉 ≠
∅)) |
22 | 18, 21 | syl6 34 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (𝑉 ∈ Fin → 𝑉 ≠ ∅))) |
23 | 22 | com23 84 |
. . . . . . . . . . 11
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ∈ Fin → (3 < (#‘𝑉) → 𝑉 ≠ ∅))) |
24 | 3, 23 | mpcom 37 |
. . . . . . . . . 10
⊢ (𝑉 ∈ Fin → (3 <
(#‘𝑉) → 𝑉 ≠ ∅)) |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ Fin → (3 < (#‘𝑉) → 𝑉 ≠ ∅))) |
26 | 25 | 3imp 1249 |
. . . . . . . 8
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → 𝑉 ≠ ∅) |
27 | 1, 2, 26 | 3jca 1235 |
. . . . . . 7
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) |
28 | 27 | ad2antrl 760 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∧ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) → (𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) |
29 | | simpl 472 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∧ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) →
〈𝑉, 𝐸〉 RegUSGrph 𝑘) |
30 | | frgraregord13 26646 |
. . . . . 6
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝑘) → ((#‘𝑉) = 1 ∨ (#‘𝑉) = 3)) |
31 | 28, 29, 30 | syl2anc 691 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∧ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) →
((#‘𝑉) = 1 ∨
(#‘𝑉) =
3)) |
32 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 ∈ ℝ) |
33 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 3 ∈ ℝ) |
34 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ∈ ℝ) |
35 | | 1lt3 11073 |
. . . . . . . . . . . . . . 15
⊢ 1 <
3 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 < 3) |
37 | 32, 33, 34, 36, 12 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → 1 < (#‘𝑉)) |
38 | 32, 37 | gtned 10051 |
. . . . . . . . . . . 12
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 1) |
39 | | eqneqall 2793 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) = 1
→ ((#‘𝑉) ≠ 1
→ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
40 | 38, 39 | syl5com 31 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → ((#‘𝑉) = 1 → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
41 | | ltne 10013 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℝ ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 3) |
42 | 6, 41 | sylan 487 |
. . . . . . . . . . . 12
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (#‘𝑉) ≠ 3) |
43 | | eqneqall 2793 |
. . . . . . . . . . . 12
⊢
((#‘𝑉) = 3
→ ((#‘𝑉) ≠ 3
→ ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
44 | 42, 43 | syl5com 31 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → ((#‘𝑉) = 3 → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
45 | 40, 44 | jaod 394 |
. . . . . . . . . 10
⊢
(((#‘𝑉) ∈
ℕ0 ∧ 3 < (#‘𝑉)) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
46 | 45 | ex 449 |
. . . . . . . . 9
⊢
((#‘𝑉) ∈
ℕ0 → (3 < (#‘𝑉) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘))) |
47 | 3, 46 | syl 17 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → (3 <
(#‘𝑉) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘))) |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝑉 FriendGrph 𝐸 → (𝑉 ∈ Fin → (3 < (#‘𝑉) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)))) |
49 | 48 | 3imp 1249 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → (((#‘𝑉) = 1 ∨ (#‘𝑉) = 3) → ¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
50 | 49 | ad2antrl 760 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∧ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) →
(((#‘𝑉) = 1 ∨
(#‘𝑉) = 3) →
¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
51 | 31, 50 | mpd 15 |
. . . 4
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝑘 ∧ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0)) → ¬
〈𝑉, 𝐸〉 RegUSGrph 𝑘) |
52 | 51 | ex 449 |
. . 3
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝑘 → (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0) → ¬
〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
53 | | ax-1 6 |
. . 3
⊢ (¬
〈𝑉, 𝐸〉 RegUSGrph 𝑘 → (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0) → ¬
〈𝑉, 𝐸〉 RegUSGrph 𝑘)) |
54 | 52, 53 | pm2.61i 175 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) ∧ 𝑘 ∈ ℕ0) → ¬
〈𝑉, 𝐸〉 RegUSGrph 𝑘) |
55 | 54 | ralrimiva 2949 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 3 < (#‘𝑉)) → ∀𝑘 ∈ ℕ0
¬ 〈𝑉, 𝐸〉 RegUSGrph 𝑘) |