Step |
Hyp |
Ref |
Expression |
1 |
|
frrusgrord0.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
frgrusgr |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph ) |
3 |
2
|
anim1i |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
4 |
1
|
isfusgr |
⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin ) ) |
5 |
3 4
|
sylibr |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph ) |
6 |
1
|
fusgreghash2wsp |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |
7 |
5 6
|
stoic3 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |
8 |
7
|
imp |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
9 |
1
|
frgrhash2wsp |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) |
10 |
9
|
eqcomd |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) ) |
11 |
10
|
eqeq1d |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ↔ ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |
12 |
11
|
3adant3 |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ↔ ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |
13 |
12
|
adantr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ↔ ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ) ) |
14 |
1
|
frrusgrord0lem |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) ) |
15 |
|
peano2cnm |
⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℂ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℂ ) |
16 |
15
|
3ad2ant2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℂ ) |
17 |
|
kcnktkm1cn |
⊢ ( 𝐾 ∈ ℂ → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |
18 |
17
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( 𝐾 · ( 𝐾 − 1 ) ) ∈ ℂ ) |
19 |
|
simp2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ♯ ‘ 𝑉 ) ∈ ℂ ) |
20 |
|
simp3 |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ♯ ‘ 𝑉 ) ≠ 0 ) |
21 |
16 18 19 20
|
mulcand |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) ↔ ( ( ♯ ‘ 𝑉 ) − 1 ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) ) |
22 |
|
npcan1 |
⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑉 ) ) |
23 |
|
oveq1 |
⊢ ( ( ( ♯ ‘ 𝑉 ) − 1 ) = ( 𝐾 · ( 𝐾 − 1 ) ) → ( ( ( ♯ ‘ 𝑉 ) − 1 ) + 1 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) |
24 |
22 23
|
sylan9req |
⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) = ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) |
25 |
24
|
ex |
⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑉 ) − 1 ) = ( 𝐾 · ( 𝐾 − 1 ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |
26 |
25
|
3ad2ant2 |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ( ( ♯ ‘ 𝑉 ) − 1 ) = ( 𝐾 · ( 𝐾 − 1 ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |
27 |
21 26
|
sylbid |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ∈ ℂ ∧ ( ♯ ‘ 𝑉 ) ≠ 0 ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |
28 |
14 27
|
syl |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ( ( ♯ ‘ 𝑉 ) · ( ( ♯ ‘ 𝑉 ) − 1 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |
29 |
13 28
|
sylbird |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ( ♯ ‘ ( 2 WSPathsN 𝐺 ) ) = ( ( ♯ ‘ 𝑉 ) · ( 𝐾 · ( 𝐾 − 1 ) ) ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |
30 |
8 29
|
mpd |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) |
31 |
30
|
ex |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) |