Proof of Theorem frrusgrord0
Step | Hyp | Ref
| Expression |
1 | | frgrusgr 41432 |
. . . . . . 7
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph
) |
2 | 1 | anim1i 590 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
3 | | frrusgrord0.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
4 | 3 | isfusgr 40537 |
. . . . . 6
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) |
5 | 2, 4 | sylibr 223 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph
) |
6 | 3 | fusgreghash2wsp 41502 |
. . . . 5
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |
7 | 5, 6 | stoic3 1692 |
. . . 4
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |
8 | 7 | imp 444 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1)))) |
9 | 3 | frgrhash2wsp 41497 |
. . . . 5
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘(2 WSPathsN 𝐺)) =
((#‘𝑉) ·
((#‘𝑉) −
1))) |
10 | 9 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · ((#‘𝑉) − 1))) |
11 | | eqeq1 2614 |
. . . . . 6
⊢
((#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · ((#‘𝑉) − 1)) → ((#‘(2 WSPathsN
𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) ↔ ((#‘𝑉) · ((#‘𝑉) − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))))) |
12 | | hashcl 13009 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℕ0) |
13 | 12 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin →
(#‘𝑉) ∈
ℂ) |
14 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin → 1 ∈
ℂ) |
15 | 13, 14 | subcld 10271 |
. . . . . . . . . . 11
⊢ (𝑉 ∈ Fin →
((#‘𝑉) − 1)
∈ ℂ) |
16 | 15 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
((#‘𝑉) − 1)
∈ ℂ) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ((#‘𝑉) − 1) ∈
ℂ) |
18 | 4 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph
) |
19 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
20 | 3, 19 | fusgrregdegfi 40769 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
21 | 18, 20 | stoic3 1692 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
22 | 1, 21 | syl3an1 1351 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → 𝐾 ∈
ℕ0)) |
23 | 22 | imp 444 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 𝐾 ∈
ℕ0) |
24 | | nn0cn 11179 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
25 | | kcnktkm1cn 10340 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℂ → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 · (𝐾 − 1)) ∈
ℂ) |
27 | 13 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘𝑉) ∈
ℂ) |
28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘𝑉) ∈ ℂ) |
29 | | hasheq0 13015 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 ↔
𝑉 =
∅)) |
30 | 29 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ Fin →
((#‘𝑉) = 0 →
𝑉 =
∅)) |
31 | 30 | necon3d 2803 |
. . . . . . . . . . . 12
⊢ (𝑉 ∈ Fin → (𝑉 ≠ ∅ →
(#‘𝑉) ≠
0)) |
32 | 31 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘𝑉) ≠
0) |
33 | 32 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(#‘𝑉) ≠
0) |
34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘𝑉) ≠ 0) |
35 | 17, 26, 28, 34 | mulcand 10539 |
. . . . . . . 8
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (((#‘𝑉) · ((#‘𝑉) − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) ↔ ((#‘𝑉) − 1) = (𝐾 · (𝐾 − 1)))) |
36 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → 1 ∈ ℂ) |
37 | | subadd2 10164 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) ↔ ((𝐾 · (𝐾 − 1)) + 1) = (#‘𝑉))) |
38 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (((𝐾 · (𝐾 − 1)) + 1) = (#‘𝑉) ↔ (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
39 | 37, 38 | syl6bb 275 |
. . . . . . . . . 10
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) ↔
(#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
40 | 39 | biimpd 218 |
. . . . . . . . 9
⊢
(((#‘𝑉) ∈
ℂ ∧ 1 ∈ ℂ ∧ (𝐾 · (𝐾 − 1)) ∈ ℂ) →
(((#‘𝑉) − 1) =
(𝐾 · (𝐾 − 1)) →
(#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
41 | 28, 36, 26, 40 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (((#‘𝑉) − 1) = (𝐾 · (𝐾 − 1)) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
42 | 35, 41 | sylbid 229 |
. . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (((#‘𝑉) · ((#‘𝑉) − 1)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
43 | 42 | com12 32 |
. . . . . 6
⊢
(((#‘𝑉)
· ((#‘𝑉)
− 1)) = ((#‘𝑉)
· (𝐾 · (𝐾 − 1))) → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
44 | 11, 43 | syl6bi 242 |
. . . . 5
⊢
((#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · ((#‘𝑉) − 1)) → ((#‘(2 WSPathsN
𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))) |
45 | 44 | com23 84 |
. . . 4
⊢
((#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · ((#‘𝑉) − 1)) → (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ((#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))) |
46 | 10, 45 | mpcom 37 |
. . 3
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → ((#‘(2 WSPathsN 𝐺)) = ((#‘𝑉) · (𝐾 · (𝐾 − 1))) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |
47 | 8, 46 | mpd 15 |
. 2
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧
∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)) |
48 | 47 | ex 449 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
(∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (#‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1))) |