Proof of Theorem frgregordn0
Step | Hyp | Ref
| Expression |
1 | | frisusgra 26519 |
. . . . 5
⊢ (𝑉 FriendGrph 𝐸 → 𝑉 USGrph 𝐸) |
2 | | usgreghash2spot 26596 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |
3 | 1, 2 | syl3an1 1351 |
. . . 4
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |
4 | 3 | imp 444 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
5 | | frghash2spot 26590 |
. . . . . 6
⊢ ((𝑉 FriendGrph 𝐸 ∧ (𝑉 ∈ Fin ∧ 𝑉 ≠ ∅)) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
6 | 5 | 3impb 1252 |
. . . . 5
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
7 | 6 | adantr 480 |
. . . 4
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
8 | | eqeq1 2614 |
. . . . . 6
⊢
((#‘(𝑉
2SPathsOt 𝐸)) =
((#‘𝑉) ·
((#‘𝑉) − 1))
→ ((#‘(𝑉
2SPathsOt 𝐸)) =
((#‘𝑉) ·
(𝐾 · (𝐾 − 1))) ↔
((#‘𝑉) ·
((#‘𝑉) − 1)) =
((#‘𝑉) ·
(𝐾 · (𝐾 − 1))))) |
9 | | hashcl 13009 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
10 | 9 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℂ) |
11 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin → 1 ∈
ℂ) |
12 | 10, 11 | subcld 10271 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin →
((#‘𝑉) − 1)
∈ ℂ) |
13 | 12 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((#‘𝑉) − 1) ∈
ℂ) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ((#‘𝑉) − 1) ∈
ℂ) |
15 | | usgfiregdegfi 26438 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
16 | 1, 15 | syl3an1 1351 |
. . . . . . . . . . 11
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
17 | 16 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
18 | | nn0cn 11179 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
19 | | kcnktkm1cn 10340 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
21 | 10 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (#‘𝑉) ∈
ℂ) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘𝑉) ∈ ℂ) |
23 | | hasheq0 13015 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
24 | 23 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 →
𝑉 =
∅)) |
25 | 24 | necon3d 2803 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
(#‘𝑉) ≠
0)) |
26 | 25 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘𝑉) ≠
0) |
27 | 26 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (#‘𝑉) ≠ 0) |
28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘𝑉) ≠ 0) |
29 | 14, 20, 22, 28 | mulcand 10539 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (((#‘𝑉) · ((#‘𝑉) − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) ↔ ((#‘𝑉) − 1) = (𝐾 · (𝐾 − 1)))) |
30 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → 1 ∈ ℂ) |
31 | | subadd2 10164 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) ↔ ((𝐾 · (𝐾 − 1)) + 1) = (#‘𝑉))) |
32 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (((𝐾 · (𝐾 − 1)) + 1) = (#‘𝑉) ↔ (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
33 | 31, 32 | syl6bb 275 |
. . . . . . . . . 10
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) ↔
(#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
34 | 33 | biimpd 218 |
. . . . . . . . 9
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) →
(#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
35 | 22, 30, 20, 34 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (((#‘𝑉) − 1) = (𝐾 · (𝐾 − 1)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
36 | 29, 35 | sylbid 229 |
. . . . . . 7
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (((#‘𝑉) · ((#‘𝑉) − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
37 | 36 | com12 32 |
. . . . . 6
⊢
(((#‘𝑉)
· ((#‘𝑉)
− 1)) = ((#‘𝑉)
· (𝐾 · (𝐾 − 1))) → (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
38 | 8, 37 | syl6bi 242 |
. . . . 5
⊢
((#‘(𝑉
2SPathsOt 𝐸)) =
((#‘𝑉) ·
((#‘𝑉) − 1))
→ ((#‘(𝑉
2SPathsOt 𝐸)) =
((#‘𝑉) ·
(𝐾 · (𝐾 − 1))) → (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))) |
39 | 38 | com23 84 |
. . . 4
⊢
((#‘(𝑉
2SPathsOt 𝐸)) =
((#‘𝑉) ·
((#‘𝑉) − 1))
→ (((𝑉 FriendGrph
𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ((#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))) |
40 | 7, 39 | mpcom 37 |
. . 3
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → ((#‘(𝑉 2SPathsOt 𝐸)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
41 | 4, 40 | mpd 15 |
. 2
⊢ (((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
42 | 41 | ex 449 |
1
⊢ ((𝑉 FriendGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑣) = 𝐾 → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |