Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
πΊ RegUSGraph πΎ) |
2 | | simpr1 1195 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
π β π) |
3 | | numclwwlk3.v |
. . . . . . . . . . . . 13
β’ π = (VtxβπΊ) |
4 | 3 | finrusgrfusgr 28555 |
. . . . . . . . . . . 12
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) |
5 | 4 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β πΊ β FinUSGraph) |
6 | 5 | adantl 483 |
. . . . . . . . . 10
β’ ((π β π β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin)) β πΊ β FinUSGraph) |
7 | | simpr1 1195 |
. . . . . . . . . 10
β’ ((π β π β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin)) β πΊ RegUSGraph πΎ) |
8 | | ne0i 4299 |
. . . . . . . . . . 11
β’ (π β π β π β β
) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β π β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin)) β π β β
) |
10 | 3 | frusgrnn0 28561 |
. . . . . . . . . 10
β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β
) β πΎ β
β0) |
11 | 6, 7, 9, 10 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β π β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin)) β πΎ β
β0) |
12 | 11 | ex 414 |
. . . . . . . 8
β’ (π β π β ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β πΎ β
β0)) |
13 | 12 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β π β§ 2 β β β§ 2 β₯
(πΎ β 1)) β
((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β πΎ β
β0)) |
14 | 13 | impcom 409 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
πΎ β
β0) |
15 | 1, 2, 14 | 3jca 1129 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
(πΊ RegUSGraph πΎ β§ π β π β§ πΎ β
β0)) |
16 | | simpr3 1197 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β 2
β₯ (πΎ β
1)) |
17 | 3 | numclwwlk5lem 29373 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ π β π β§ πΎ β β0) β (2
β₯ (πΎ β 1)
β ((β―β(π(ClWWalksNOnβπΊ)2)) mod 2) = 1)) |
18 | 15, 16, 17 | sylc 65 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
((β―β(π(ClWWalksNOnβπΊ)2)) mod 2) = 1) |
19 | 18 | a1i 11 |
. . 3
β’ (π = 2 β (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β 1))) β
((β―β(π(ClWWalksNOnβπΊ)2)) mod 2) = 1)) |
20 | | eleq1 2826 |
. . . . 5
β’ (π = 2 β (π β β β 2 β
β)) |
21 | | breq1 5113 |
. . . . 5
β’ (π = 2 β (π β₯ (πΎ β 1) β 2 β₯ (πΎ β 1))) |
22 | 20, 21 | 3anbi23d 1440 |
. . . 4
β’ (π = 2 β ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β (π β π β§ 2 β β β§ 2 β₯
(πΎ β
1)))) |
23 | 22 | anbi2d 630 |
. . 3
β’ (π = 2 β (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ 2 β β β§ 2 β₯
(πΎ β
1))))) |
24 | | oveq2 7370 |
. . . . . 6
β’ (π = 2 β (π(ClWWalksNOnβπΊ)π) = (π(ClWWalksNOnβπΊ)2)) |
25 | 24 | fveq2d 6851 |
. . . . 5
β’ (π = 2 β
(β―β(π(ClWWalksNOnβπΊ)π)) = (β―β(π(ClWWalksNOnβπΊ)2))) |
26 | | id 22 |
. . . . 5
β’ (π = 2 β π = 2) |
27 | 25, 26 | oveq12d 7380 |
. . . 4
β’ (π = 2 β
((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = ((β―β(π(ClWWalksNOnβπΊ)2)) mod 2)) |
28 | 27 | eqeq1d 2739 |
. . 3
β’ (π = 2 β
(((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = 1 β ((β―β(π(ClWWalksNOnβπΊ)2)) mod 2) =
1)) |
29 | 19, 23, 28 | 3imtr4d 294 |
. 2
β’ (π = 2 β (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = 1)) |
30 | | 3simpa 1149 |
. . . . . . . 8
β’ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph )) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph )) |
32 | 31 | adantl 483 |
. . . . . 6
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph )) |
33 | | simprl3 1221 |
. . . . . 6
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β π β Fin) |
34 | | simprr1 1222 |
. . . . . 6
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β π β π) |
35 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ (π β (β β {2})
β (π β β
β§ π β
2)) |
36 | | oddprmge3 16583 |
. . . . . . . . . . 11
β’ (π β (β β {2})
β π β
(β€β₯β3)) |
37 | 35, 36 | sylbir 234 |
. . . . . . . . . 10
β’ ((π β β β§ π β 2) β π β
(β€β₯β3)) |
38 | 37 | ex 414 |
. . . . . . . . 9
β’ (π β β β (π β 2 β π β
(β€β₯β3))) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β (π β 2 β π β
(β€β₯β3))) |
40 | 39 | adantl 483 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (π β 2 β π β
(β€β₯β3))) |
41 | 40 | impcom 409 |
. . . . . 6
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β π β
(β€β₯β3)) |
42 | 3 | numclwwlk3 29371 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β Fin β§ π β π β§ π β (β€β₯β3)))
β (β―β(π(ClWWalksNOnβπΊ)π)) = (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2)))) |
43 | 32, 33, 34, 41, 42 | syl13anc 1373 |
. . . . 5
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β (β―β(π(ClWWalksNOnβπΊ)π)) = (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2)))) |
44 | 43 | oveq1d 7377 |
. . . 4
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β ((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = ((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2))) mod π)) |
45 | 12 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β πΎ β
β0)) |
46 | 45 | impcom 409 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β πΎ β
β0) |
47 | 46 | nn0zd 12532 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β πΎ β β€) |
48 | | peano2zm 12553 |
. . . . . . . . 9
β’ (πΎ β β€ β (πΎ β 1) β
β€) |
49 | | zre 12510 |
. . . . . . . . 9
β’ ((πΎ β 1) β β€
β (πΎ β 1) β
β) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (πΎ β 1) β β) |
51 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β π β Fin) |
52 | 3 | clwwlknonfin 29080 |
. . . . . . . . . 10
β’ (π β Fin β (π(ClWWalksNOnβπΊ)(π β 2)) β Fin) |
53 | | hashcl 14263 |
. . . . . . . . . 10
β’ ((π(ClWWalksNOnβπΊ)(π β 2)) β Fin β
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β0) |
54 | 51, 52, 53 | 3syl 18 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β0) |
55 | 54 | nn0red 12481 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β) |
56 | 50, 55 | remulcld 11192 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) β
β) |
57 | 46 | nn0red 12481 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β πΎ β β) |
58 | | prmm2nn0 16581 |
. . . . . . . . . 10
β’ (π β β β (π β 2) β
β0) |
59 | 58 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β (π β 2) β
β0) |
60 | 59 | adantl 483 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (π β 2) β
β0) |
61 | 57, 60 | reexpcld 14075 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (πΎβ(π β 2)) β
β) |
62 | | prmnn 16557 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
63 | 62 | nnrpd 12962 |
. . . . . . . . 9
β’ (π β β β π β
β+) |
64 | 63 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β π β
β+) |
65 | 64 | adantl 483 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β π β
β+) |
66 | 56, 61, 65 | 3jca 1129 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) β β β§ (πΎβ(π β 2)) β β β§ π β
β+)) |
67 | 66 | adantl 483 |
. . . . 5
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) β β β§ (πΎβ(π β 2)) β β β§ π β
β+)) |
68 | | modaddabs 13821 |
. . . . . 6
β’ ((((πΎ β 1) Β·
(β―β(π(ClWWalksNOnβπΊ)(π β 2)))) β β β§ (πΎβ(π β 2)) β β β§ π β β+)
β (((((πΎ β 1)
Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π) = ((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2))) mod π)) |
69 | 68 | eqcomd 2743 |
. . . . 5
β’ ((((πΎ β 1) Β·
(β―β(π(ClWWalksNOnβπΊ)(π β 2)))) β β β§ (πΎβ(π β 2)) β β β§ π β β+)
β ((((πΎ β 1)
Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2))) mod π) = (((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π)) |
70 | 67, 69 | syl 17 |
. . . 4
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β ((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) + (πΎβ(π β 2))) mod π) = (((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π)) |
71 | 62 | 3ad2ant2 1135 |
. . . . . . . . . . 11
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β π β β) |
72 | 71 | adantl 483 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β π β β) |
73 | | nn0z 12531 |
. . . . . . . . . . 11
β’ (πΎ β β0
β πΎ β
β€) |
74 | 46, 73, 48 | 3syl 18 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (πΎ β 1) β β€) |
75 | 54 | nn0zd 12532 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β€) |
76 | 72, 74, 75 | 3jca 1129 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (π β β β§ (πΎ β 1) β β€ β§
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β
β€)) |
77 | | simpr3 1197 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β π β₯ (πΎ β 1)) |
78 | | mulmoddvds 16219 |
. . . . . . . . 9
β’ ((π β β β§ (πΎ β 1) β β€ β§
(β―β(π(ClWWalksNOnβπΊ)(π β 2))) β β€) β (π β₯ (πΎ β 1) β (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) = 0)) |
79 | 76, 77, 78 | sylc 65 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) = 0) |
80 | | simpr2 1196 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β π β β) |
81 | 80, 47 | jca 513 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (π β β β§ πΎ β β€)) |
82 | | powm2modprm 16682 |
. . . . . . . . 9
β’ ((π β β β§ πΎ β β€) β (π β₯ (πΎ β 1) β ((πΎβ(π β 2)) mod π) = 1)) |
83 | 81, 77, 82 | sylc 65 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((πΎβ(π β 2)) mod π) = 1) |
84 | 79, 83 | oveq12d 7380 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) = (0 + 1)) |
85 | 84 | oveq1d 7377 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π) = ((0 + 1) mod π)) |
86 | | 0p1e1 12282 |
. . . . . . . . . 10
β’ (0 + 1) =
1 |
87 | 86 | oveq1i 7372 |
. . . . . . . . 9
β’ ((0 + 1)
mod π) = (1 mod π) |
88 | 62 | nnred 12175 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
89 | | prmgt1 16580 |
. . . . . . . . . 10
β’ (π β β β 1 <
π) |
90 | | 1mod 13815 |
. . . . . . . . . 10
β’ ((π β β β§ 1 <
π) β (1 mod π) = 1) |
91 | 88, 89, 90 | syl2anc 585 |
. . . . . . . . 9
β’ (π β β β (1 mod
π) = 1) |
92 | 87, 91 | eqtrid 2789 |
. . . . . . . 8
β’ (π β β β ((0 + 1)
mod π) =
1) |
93 | 92 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β π β§ π β β β§ π β₯ (πΎ β 1)) β ((0 + 1) mod π) = 1) |
94 | 93 | adantl 483 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((0 + 1) mod π) = 1) |
95 | 85, 94 | eqtrd 2777 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β (((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π) = 1) |
96 | 95 | adantl 483 |
. . . 4
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β (((((πΎ β 1) Β· (β―β(π(ClWWalksNOnβπΊ)(π β 2)))) mod π) + ((πΎβ(π β 2)) mod π)) mod π) = 1) |
97 | 44, 70, 96 | 3eqtrd 2781 |
. . 3
β’ ((π β 2 β§ ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1)))) β ((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = 1) |
98 | 97 | ex 414 |
. 2
β’ (π β 2 β (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = 1)) |
99 | 29, 98 | pm2.61ine 3029 |
1
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph β§ π β Fin) β§ (π β π β§ π β β β§ π β₯ (πΎ β 1))) β ((β―β(π(ClWWalksNOnβπΊ)π)) mod π) = 1) |