Step | Hyp | Ref
| Expression |
1 | | rusgraprop 26456 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾)) |
2 | | nn0re 11178 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
3 | | 1re 9918 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
4 | | lenlt 9995 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐾 ≤ 1
↔ ¬ 1 < 𝐾)) |
5 | 4 | bicomd 212 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℝ ∧ 1 ∈
ℝ) → (¬ 1 < 𝐾 ↔ 𝐾 ≤ 1)) |
6 | 2, 3, 5 | sylancl 693 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (¬ 1 < 𝐾
↔ 𝐾 ≤
1)) |
7 | | ioran 510 |
. . . . . . . . . . 11
⊢ (¬
(𝐾 = 0 ∨ 𝐾 = 2) ↔ (¬ 𝐾 = 0 ∧ ¬ 𝐾 = 2)) |
8 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ (𝐾 ≠ 0 ↔ ¬ 𝐾 = 0) |
9 | | elnnne0 11183 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) |
10 | | nnle1eq1 10925 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 ↔ 𝐾 = 1)) |
11 | | rusgrasn 26472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((#‘𝑉) = 1
∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 𝐾 = 0) |
12 | 11 | orcd 406 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝑉) = 1
∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)) |
13 | 12 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
14 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → ((#‘𝑉) = 1 → (𝐾 = 0 ∨ 𝐾 = 2))) |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑉) = 1
→ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))) |
16 | 15 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑉) = 1
→ ((𝑉 ∈ Fin ∧
𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
17 | 16 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝑉) = 1
→ (𝐾 = 1 →
((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
18 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
19 | | rusisusgra 26458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
20 | | usgrav 25867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
22 | | hasheq0 13015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑉 ∈ V → ((#‘𝑉) = 0 ↔ 𝑉 = ∅)) |
23 | 22 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑉 ∈ V → (𝑉 = ∅ ↔ (#‘𝑉) = 0)) |
24 | 23 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑉 ∈ V → (𝑉 ≠ ∅ ↔
(#‘𝑉) ≠
0)) |
25 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝑉) ∈
ℕ ↔ ((#‘𝑉)
∈ ℕ0 ∧ (#‘𝑉) ≠ 0)) |
26 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑉) ≠ 1
↔ ¬ (#‘𝑉) =
1) |
27 | | eluz2b3 11638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝑉) ∈
(ℤ≥‘2) ↔ ((#‘𝑉) ∈ ℕ ∧ (#‘𝑉) ≠ 1)) |
28 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
((#‘𝑉) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝑉) ∈ ℤ ∧ 2 ≤
(#‘𝑉))) |
29 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 1 ∈ ℝ) |
30 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ 2 ∈
ℝ |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 2 ∈ ℝ) |
32 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
((#‘𝑉) ∈
ℤ → (#‘𝑉)
∈ ℝ) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → (#‘𝑉) ∈ ℝ) |
34 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 1 <
2 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
((#‘𝑉) ∈
ℤ → 1 < 2) |
36 | 35 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → (1 < 2 ∧ 2 ≤
(#‘𝑉))) |
37 | | ltletr 10008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) → ((1 < 2 ∧ 2
≤ (#‘𝑉)) → 1
< (#‘𝑉))) |
38 | 37 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (#‘𝑉) ∈ ℝ) ∧ (1 < 2 ∧ 2
≤ (#‘𝑉))) → 1
< (#‘𝑉)) |
39 | 29, 31, 33, 36, 38 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → 1 < (#‘𝑉)) |
40 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (𝐾 = 1 → (((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
41 | 40 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢ (𝐾 = 1 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
42 | 41 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑉 FriendGrph 𝐸 ∧ (((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1)) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
43 | | vdgn1frgrav3 26555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . 59
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 1) |
44 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . 61
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
45 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
⊢ (((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ↔ ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 1) |
46 | 45 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ (¬ ((𝑉 VDeg 𝐸)‘𝑣) = 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
47 | | ancom 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
⊢ ((¬
((𝑉 VDeg 𝐸)‘𝑣) = 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ (((𝑉 VDeg 𝐸)‘𝑣) = 1 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 1)) |
48 | | pm3.24 922 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
⊢ ¬
(((𝑉 VDeg 𝐸)‘𝑣) = 1 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 1) |
49 | 48 | bifal 1488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) = 1 ∧ ¬ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ ⊥) |
50 | 46, 47, 49 | 3bitri 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
⊢ ((((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ ⊥) |
51 | 50 | ralbii 2963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) ↔ ∀𝑣 ∈ 𝑉 ⊥) |
52 | | r19.3rzv 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
⊢ (𝑉 ≠ ∅ → (⊥
↔ ∀𝑣 ∈
𝑉 ⊥)) |
53 | | falim 1489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
⊢ (⊥
→ (𝐾 = 0 ∨ 𝐾 = 2)) |
54 | 52, 53 | syl6bir 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
⊢ (𝑉 ≠ ∅ →
(∀𝑣 ∈ 𝑉 ⊥ → (𝐾 = 0 ∨ 𝐾 = 2))) |
55 | 54 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
⊢
(∀𝑣 ∈
𝑉 ⊥ → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2))) |
56 | 51, 55 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . 61
⊢
(∀𝑣 ∈
𝑉 (((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ((𝑉 VDeg 𝐸)‘𝑣) = 1) → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2))) |
57 | 44, 56 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . 60
⊢
((∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1) → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2))) |
58 | 57 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . 59
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) ≠ 1 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2)))) |
59 | 43, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
⊢ ((𝑉 FriendGrph 𝐸 ∧ 1 < (#‘𝑉)) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2)))) |
60 | 59 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
⊢ (1 <
(#‘𝑉) → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2))))) |
61 | 60 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
⊢
((((#‘𝑉)
∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1) → (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2))))) |
62 | 61 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
⊢ ((𝑉 FriendGrph 𝐸 ∧ (((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1)) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 1 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2)))) |
63 | 42, 62 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑉 FriendGrph 𝐸 ∧ (((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1)) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 ≠ ∅ → (𝐾 = 0 ∨ 𝐾 = 2)))) |
64 | 63 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ ((𝑉 FriendGrph 𝐸 ∧ (((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1)) → (𝑉 ≠ ∅ → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))) |
65 | 64 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ (𝑉 FriendGrph 𝐸 → ((((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1) → (𝑉 ≠ ∅ → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
66 | 65 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝑉 FriendGrph 𝐸 → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 ≠ ∅ → ((((#‘𝑉) ∈ ℤ ∧ 1 <
(#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
67 | 66 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢
(∀𝑣 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((((#‘𝑉) ∈ ℤ ∧ 1 <
(#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
68 | 67 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((((#‘𝑉) ∈ ℤ ∧ 1 <
(#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
69 | 1, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → ((((#‘𝑉) ∈ ℤ ∧ 1 <
(#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
70 | 69 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝑉 ≠ ∅ → ((((#‘𝑉) ∈ ℤ ∧ 1 <
(#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
71 | 70 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → ((((#‘𝑉) ∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1) → (𝐾 = 0 ∨ 𝐾 = 2))) |
72 | 71 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
((((#‘𝑉)
∈ ℤ ∧ 1 < (#‘𝑉)) ∧ 𝐾 = 1) → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))) |
73 | 72 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((#‘𝑉) ∈
ℤ ∧ 1 < (#‘𝑉)) → (𝐾 = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
74 | 39, 73 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝑉) ∈
ℤ ∧ 2 ≤ (#‘𝑉)) → (𝐾 = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
75 | 74 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((2
∈ ℤ ∧ (#‘𝑉) ∈ ℤ ∧ 2 ≤ (#‘𝑉)) → (𝐾 = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
76 | 28, 75 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝑉) ∈
(ℤ≥‘2) → (𝐾 = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
77 | 27, 76 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((#‘𝑉) ∈
ℕ ∧ (#‘𝑉)
≠ 1) → (𝐾 = 1
→ ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
78 | 77 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝑉) ≠ 1
→ ((#‘𝑉) ∈
ℕ → (𝐾 = 1
→ ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
79 | 78 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝑉) ≠ 1
→ (𝐾 = 1 →
((#‘𝑉) ∈ ℕ
→ ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
80 | 26, 79 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (¬
(#‘𝑉) = 1 →
(𝐾 = 1 →
((#‘𝑉) ∈ ℕ
→ ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
81 | 80 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝑉) ∈
ℕ → (𝐾 = 1
→ (¬ (#‘𝑉) =
1 → ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
82 | 25, 81 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝑉) ∈
ℕ0 ∧ (#‘𝑉) ≠ 0) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
83 | 82 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝑉) ≠ 0
→ ((#‘𝑉) ∈
ℕ0 → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((𝑉 ≠ ∅ ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
84 | 83 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝑉) ≠ 0
→ ((𝑉 ≠ ∅
∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
85 | 84 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝑉) ≠ 0
→ (𝑉 ≠ ∅
→ ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2))))))) |
86 | 24, 85 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑉 ∈ V → (𝑉 ≠ ∅ → (𝑉 ≠ ∅ → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))))) |
87 | 86 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑉 ≠ ∅ → (𝑉 ≠ ∅ → (𝑉 ∈ V → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))))) |
88 | 87 | pm2.43i 50 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑉 ≠ ∅ → (𝑉 ∈ V → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2))))))) |
89 | 88 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑉 ≠ ∅ ∧ 𝑉 ∈ V) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
90 | 89 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 ≠ ∅ ∧ 𝑉 ∈ V) → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2))))))) |
91 | 90 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑉 ∈ V → (𝑉 ≠ ∅ → (𝑉 FriendGrph 𝐸 → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))))) |
92 | 91 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑉 ∈ V → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))))) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))))) |
94 | 21, 93 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2))))))) |
95 | 94 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((#‘𝑉) ∈ ℕ0
→ (𝐾 = 0 ∨ 𝐾 = 2)))))) |
96 | 95 | com15 99 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑉) ∈
ℕ0 → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬ (#‘𝑉) = 1 → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
97 | 18, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ → (𝐾 = 1 → (¬
(#‘𝑉) = 1 →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
98 | 97 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (𝐾 = 1 → (¬
(#‘𝑉) = 1 →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
99 | 98 | com13 86 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(#‘𝑉) = 1 →
(𝐾 = 1 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
100 | 17, 99 | pm2.61i 175 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 1 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
101 | 10, 100 | syl6bi 242 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → (𝐾 ≤ 1 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
102 | 9, 101 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) →
(𝐾 ≤ 1 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
103 | 102 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ≠ 0 → (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 →
((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
104 | 103 | com23 84 |
. . . . . . . . . . . . 13
⊢ (𝐾 ≠ 0 → (𝐾 ≤ 1 → (𝐾 ∈ ℕ0
→ ((𝑉 ∈ Fin ∧
𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
105 | 8, 104 | sylbir 224 |
. . . . . . . . . . . 12
⊢ (¬
𝐾 = 0 → (𝐾 ≤ 1 → (𝐾 ∈ ℕ0
→ ((𝑉 ∈ Fin ∧
𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
106 | 105 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝐾 = 0 ∧ ¬ 𝐾 = 2) → (𝐾 ≤ 1 → (𝐾 ∈ ℕ0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
107 | 7, 106 | sylbi 206 |
. . . . . . . . . 10
⊢ (¬
(𝐾 = 0 ∨ 𝐾 = 2) → (𝐾 ≤ 1 → (𝐾 ∈ ℕ0 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
108 | 107 | com13 86 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝐾 ≤ 1 →
(¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
109 | 6, 108 | sylbid 229 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ (¬ 1 < 𝐾
→ (¬ (𝐾 = 0 ∨
𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
110 | 109 | com25 97 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ0
→ ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ 1 < 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
111 | 110 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ 1 < 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
112 | 111 | expd 451 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ 1 < 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))))) |
113 | 1, 112 | mpcom 37 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 FriendGrph 𝐸 → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ 1 < 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2)))))) |
114 | 113 | impcom 445 |
. . 3
⊢ ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (¬ 1 < 𝐾 → (𝐾 = 0 ∨ 𝐾 = 2))))) |
115 | 114 | com14 94 |
. 2
⊢ (¬ 1
< 𝐾 → (¬ (𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))))) |
116 | | simprl 790 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → 𝑉 FriendGrph 𝐸) |
117 | | simpl 472 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ∈ Fin) |
118 | 117 | ad2antlr 759 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → 𝑉 ∈ Fin) |
119 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝑉 ≠ ∅) |
120 | 119 | ad2antlr 759 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → 𝑉 ≠ ∅) |
121 | | simpl 472 |
. . . . . 6
⊢ ((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → 1 < 𝐾) |
122 | | simpr 476 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 〈𝑉, 𝐸〉 RegUSGrph 𝐾) |
123 | 121, 122 | anim12ci 589 |
. . . . 5
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾)) |
124 | | frgrareggt1 26643 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾) → 𝐾 = 2)) |
125 | 124 | imp 444 |
. . . . 5
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 1 < 𝐾)) → 𝐾 = 2) |
126 | 116, 118,
120, 123, 125 | syl31anc 1321 |
. . . 4
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → 𝐾 = 2) |
127 | 126 | olcd 407 |
. . 3
⊢ (((1 <
𝐾 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) ∧ (𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾)) → (𝐾 = 0 ∨ 𝐾 = 2)) |
128 | 127 | exp31 628 |
. 2
⊢ (1 <
𝐾 → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
129 | | 2a1 28 |
. 2
⊢ ((𝐾 = 0 ∨ 𝐾 = 2) → ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2)))) |
130 | 115, 128,
129 | pm2.61ii 176 |
1
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝑉 FriendGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → (𝐾 = 0 ∨ 𝐾 = 2))) |