Step | Hyp | Ref
| Expression |
1 | | rusisusgra 26458 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
2 | 1 | ad2antrr 758 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 USGrph 𝐸) |
3 | | simp1 1054 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑉 ∈
Fin) |
4 | 3 | adantl 481 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 ∈
Fin) |
5 | | simp2 1055 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
6 | 5 | adantl 481 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
7 | | uzuzle23 11605 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
8 | 7 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘2)) |
9 | 8 | adantl 481 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑁 ∈
(ℤ≥‘2)) |
10 | | numclwwlk.c |
. . . 4
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
11 | | numclwwlk.f |
. . . 4
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
12 | | numclwwlk.g |
. . . 4
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
13 | | numclwwlk.q |
. . . 4
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
14 | | numclwwlk.h |
. . . 4
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))}) |
15 | 10, 11, 12, 13, 14 | numclwwlk3lem 26635 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (#‘(𝑋𝐹𝑁)) = ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐺𝑁)))) |
16 | 2, 4, 6, 9, 15 | syl31anc 1321 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹𝑁)) = ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐺𝑁)))) |
17 | 10, 11, 12, 13, 14 | numclwwlk2 26634 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐻𝑁)) = ((𝐾↑(𝑁 − 2)) − (#‘(𝑋𝐹(𝑁 − 2))))) |
18 | | simpl 472 |
. . . . 5
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → 〈𝑉, 𝐸〉 RegUSGrph 𝐾) |
19 | 18, 3 | anim12ci 589 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑉 ∈ Fin ∧
〈𝑉, 𝐸〉 RegUSGrph 𝐾)) |
20 | | 3simpc 1053 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘3))) |
21 | 20 | adantl 481 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘3))) |
22 | 10, 11, 12 | numclwwlk1 26625 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐺𝑁)) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
23 | 19, 21, 22 | syl2anc 691 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐺𝑁)) = (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) |
24 | 17, 23 | oveq12d 6567 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘(𝑋𝐻𝑁)) + (#‘(𝑋𝐺𝑁))) = (((𝐾↑(𝑁 − 2)) − (#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾 · (#‘(𝑋𝐹(𝑁 − 2)))))) |
25 | | rusgraprop 26456 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝐾)) |
26 | | nn0cn 11179 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
27 | 26 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑢 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑢) = 𝐾) → 𝐾 ∈ ℂ) |
28 | 25, 27 | syl 17 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐾 ∈ ℂ) |
29 | 28 | ad2antrr 758 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℂ) |
30 | | usgrav 25867 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
31 | 30 | simprd 478 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
32 | 1, 31 | syl 17 |
. . . . . . 7
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝐸 ∈ V) |
33 | 32 | adantr 480 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) → 𝐸 ∈ V) |
34 | 33, 3 | anim12ci 589 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑉 ∈ Fin ∧
𝐸 ∈
V)) |
35 | | uz3m2nn 11607 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
36 | 35 | nnnn0d 11228 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
37 | 36 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ0) |
38 | 5, 37 | jca 553 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ0)) |
39 | 38 | adantl 481 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ0)) |
40 | 10, 11 | numclwwlkffin 26609 |
. . . . 5
⊢ (((𝑉 ∈ Fin ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ0))
→ (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
41 | 34, 39, 40 | syl2anc 691 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋𝐹(𝑁 − 2)) ∈ Fin) |
42 | | hashcl 13009 |
. . . . 5
⊢ ((𝑋𝐹(𝑁 − 2)) ∈ Fin →
(#‘(𝑋𝐹(𝑁 − 2))) ∈
ℕ0) |
43 | 42 | nn0cnd 11230 |
. . . 4
⊢ ((𝑋𝐹(𝑁 − 2)) ∈ Fin →
(#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
44 | 41, 43 | syl 17 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹(𝑁 − 2))) ∈
ℂ) |
45 | | numclwlk3lem3 26600 |
. . 3
⊢ ((𝐾 ∈ ℂ ∧
(#‘(𝑋𝐹(𝑁 − 2))) ∈ ℂ ∧ 𝑁 ∈
(ℤ≥‘2)) → (((𝐾↑(𝑁 − 2)) − (#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) = (((𝐾 − 1) · (#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |
46 | 29, 44, 9, 45 | syl3anc 1318 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((𝐾↑(𝑁 − 2)) −
(#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾 · (#‘(𝑋𝐹(𝑁 − 2))))) = (((𝐾 − 1) · (#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |
47 | 16, 24, 46 | 3eqtrd 2648 |
1
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 FriendGrph 𝐸) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (#‘(𝑋𝐹𝑁)) = (((𝐾 − 1) · (#‘(𝑋𝐹(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |