| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpl 486 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) → 𝐺 RegUSGraph 𝐾) |
| 2 | | simp1 1137 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑉 ∈
Fin) |
| 3 | | numclwwlk3.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 4 | 3 | finrusgrfusgr 27507 |
. . . 4
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) |
| 5 | 1, 2, 4 | syl2an 599 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 ∈
FinUSGraph) |
| 6 | | simpr2 1196 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑋 ∈ 𝑉) |
| 7 | | uzuzle23 12371 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
| 8 | 7 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑁 ∈
(ℤ≥‘2)) |
| 9 | 8 | adantl 485 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑁 ∈
(ℤ≥‘2)) |
| 10 | | eqid 2738 |
. . . 4
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣}) |
| 11 | | eqid 2738 |
. . . 4
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣}) = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣}) |
| 12 | 10, 11 | numclwwlk3lem2 28321 |
. . 3
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})𝑁)) + (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)))) |
| 13 | 5, 6, 9, 12 | syl21anc 837 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = ((♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})𝑁)) + (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)))) |
| 14 | | eqid 2738 |
. . . 4
⊢ (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)}) = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)}) |
| 15 | 3, 14, 11 | numclwwlk2 28318 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})𝑁)) = ((𝐾↑(𝑁 − 2)) − (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) |
| 16 | 1, 2 | anim12ci 617 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑉 ∈ Fin ∧
𝐺 RegUSGraph 𝐾)) |
| 17 | | 3simpc 1151 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘3))) |
| 18 | 17 | adantl 485 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘3))) |
| 19 | | eqid 2738 |
. . . . 5
⊢ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) |
| 20 | 3, 10, 19 | numclwwlk1 28298 |
. . . 4
⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) |
| 21 | 16, 18, 20 | syl2anc 587 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁)) = (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) |
| 22 | 15, 21 | oveq12d 7188 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})𝑁)) + (♯‘(𝑋(𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})𝑁))) = (((𝐾↑(𝑁 − 2)) − (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))))) |
| 23 | | simpll 767 |
. . . . 5
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐺 RegUSGraph 𝐾) |
| 24 | | ne0i 4223 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → 𝑉 ≠ ∅) |
| 25 | 24 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑉 ≠
∅) |
| 26 | 25 | adantl 485 |
. . . . 5
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝑉 ≠
∅) |
| 27 | 3 | frusgrnn0 27513 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈
ℕ0) |
| 28 | 5, 23, 26, 27 | syl3anc 1372 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℕ0) |
| 29 | 28 | nn0cnd 12038 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 𝐾 ∈
ℂ) |
| 30 | | uz3m2nn 12373 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈ ℕ) |
| 31 | 30 | 3anim3i 1155 |
. . . . 5
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑉 ∈ Fin ∧
𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
| 32 | 31 | adantl 485 |
. . . 4
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑉 ∈ Fin ∧
𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈
ℕ)) |
| 33 | 3 | clwwlknonfin 28031 |
. . . . 5
⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) |
| 34 | 33 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ (𝑁 − 2) ∈ ℕ) → (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin) |
| 35 | | hashcl 13809 |
. . . . 5
⊢ ((𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin →
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ∈
ℕ0) |
| 36 | 35 | nn0cnd 12038 |
. . . 4
⊢ ((𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)) ∈ Fin →
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ∈
ℂ) |
| 37 | 32, 34, 36 | 3syl 18 |
. . 3
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ∈
ℂ) |
| 38 | | numclwwlk3lem1 28319 |
. . 3
⊢ ((𝐾 ∈ ℂ ∧
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) ∈ ℂ ∧ 𝑁 ∈
(ℤ≥‘2)) → (((𝐾↑(𝑁 − 2)) − (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) = (((𝐾 − 1) · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |
| 39 | 29, 37, 9, 38 | syl3anc 1372 |
. 2
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((𝐾↑(𝑁 − 2)) −
(♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾 · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))))) = (((𝐾 − 1) · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |
| 40 | 13, 22, 39 | 3eqtrd 2777 |
1
⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁)) = (((𝐾 − 1) · (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))) + (𝐾↑(𝑁 − 2)))) |
