Step | Hyp | Ref
| Expression |
1 | | numclwwlk6.v |
. . . . . 6
β’ π = (VtxβπΊ) |
2 | 1 | finrusgrfusgr 29089 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) |
3 | 2 | 3adant2 1129 |
. . . 4
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β πΊ β FinUSGraph) |
4 | | prmnn 16615 |
. . . . 5
β’ (π β β β π β
β) |
5 | 4 | adantr 479 |
. . . 4
β’ ((π β β β§ π β₯ (πΎ β 1)) β π β β) |
6 | 1 | numclwwlk4 29906 |
. . . 4
β’ ((πΊ β FinUSGraph β§ π β β) β
(β―β(π ClWWalksN
πΊ)) = Ξ£π₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π))) |
7 | 3, 5, 6 | syl2an 594 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (β―β(π ClWWalksN πΊ)) = Ξ£π₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π))) |
8 | 7 | oveq1d 7426 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β ((β―β(π ClWWalksN πΊ)) mod π) = (Ξ£π₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π)) mod π)) |
9 | 5 | adantl 480 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β π β β) |
10 | | simp3 1136 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β π β Fin) |
11 | 10 | adantr 479 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β π β Fin) |
12 | 11 | adantr 479 |
. . . . . . 7
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β π β Fin) |
13 | 1 | clwwlknonfin 29614 |
. . . . . . 7
β’ (π β Fin β (π₯(ClWWalksNOnβπΊ)π) β Fin) |
14 | | hashcl 14320 |
. . . . . . 7
β’ ((π₯(ClWWalksNOnβπΊ)π) β Fin β (β―β(π₯(ClWWalksNOnβπΊ)π)) β
β0) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . 6
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β (β―β(π₯(ClWWalksNOnβπΊ)π)) β
β0) |
16 | 15 | nn0zd 12588 |
. . . . 5
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β (β―β(π₯(ClWWalksNOnβπΊ)π)) β β€) |
17 | 16 | ralrimiva 3144 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β βπ₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π)) β β€) |
18 | 9, 11, 17 | modfsummod 15744 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (Ξ£π₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) = (Ξ£π₯ β π ((β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) mod π)) |
19 | | simpl 481 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin)) |
20 | | simpr 483 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (π β β β§ π β₯ (πΎ β 1))) |
21 | 20 | anim1ci 614 |
. . . . . . 7
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β (π₯ β π β§ (π β β β§ π β₯ (πΎ β 1)))) |
22 | | 3anass 1093 |
. . . . . . 7
β’ ((π₯ β π β§ π β β β§ π β₯ (πΎ β 1)) β (π₯ β π β§ (π β β β§ π β₯ (πΎ β 1)))) |
23 | 21, 22 | sylibr 233 |
. . . . . 6
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β (π₯ β π β§ π β β β§ π β₯ (πΎ β 1))) |
24 | 1 | numclwwlk5 29908 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π₯ β π β§ π β β β§ π β₯ (πΎ β 1))) β ((β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) = 1) |
25 | 19, 23, 24 | syl2an2r 681 |
. . . . 5
β’ ((((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β§ π₯ β π) β ((β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) = 1) |
26 | 25 | sumeq2dv 15653 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β Ξ£π₯ β π ((β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) = Ξ£π₯ β π 1) |
27 | 26 | oveq1d 7426 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (Ξ£π₯ β π ((β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) mod π) = (Ξ£π₯ β π 1 mod π)) |
28 | 18, 27 | eqtrd 2770 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (Ξ£π₯ β π (β―β(π₯(ClWWalksNOnβπΊ)π)) mod π) = (Ξ£π₯ β π 1 mod π)) |
29 | | 1cnd 11213 |
. . . . 5
β’ ((π β β β§ π β₯ (πΎ β 1)) β 1 β
β) |
30 | | fsumconst 15740 |
. . . . 5
β’ ((π β Fin β§ 1 β
β) β Ξ£π₯
β π 1 =
((β―βπ) Β·
1)) |
31 | 10, 29, 30 | syl2an 594 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β Ξ£π₯ β π 1 = ((β―βπ) Β· 1)) |
32 | | hashcl 14320 |
. . . . . . . 8
β’ (π β Fin β
(β―βπ) β
β0) |
33 | 32 | nn0red 12537 |
. . . . . . 7
β’ (π β Fin β
(β―βπ) β
β) |
34 | | ax-1rid 11182 |
. . . . . . 7
β’
((β―βπ)
β β β ((β―βπ) Β· 1) = (β―βπ)) |
35 | 33, 34 | syl 17 |
. . . . . 6
β’ (π β Fin β
((β―βπ) Β·
1) = (β―βπ)) |
36 | 35 | 3ad2ant3 1133 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β ((β―βπ) Β· 1) =
(β―βπ)) |
37 | 36 | adantr 479 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β ((β―βπ) Β· 1) =
(β―βπ)) |
38 | 31, 37 | eqtrd 2770 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β Ξ£π₯ β π 1 = (β―βπ)) |
39 | 38 | oveq1d 7426 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β (Ξ£π₯ β π 1 mod π) = ((β―βπ) mod π)) |
40 | 8, 28, 39 | 3eqtrd 2774 |
1
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β β β§ π β₯ (πΎ β 1))) β ((β―β(π ClWWalksN πΊ)) mod π) = ((β―βπ) mod π)) |