Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐บ RegUSGraph ๐พ) |
2 | | simplr 768 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐บ โ FriendGraph
) |
3 | | simprr 772 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐ โ Fin) |
4 | 1, 2, 3 | 3jca 1129 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ (๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph โง ๐ โ Fin)) |
5 | | numclwwlk6.v |
. . . 4
โข ๐ = (Vtxโ๐บ) |
6 | 5 | numclwwlk6 29643 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = ((โฏโ๐) mod ๐)) |
7 | 4, 6 | stoic3 1779 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = ((โฏโ๐) mod ๐)) |
8 | | simp2 1138 |
. . . . 5
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ
โง ๐ โ Fin)) |
9 | 8 | ancomd 463 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐ โ Fin โง ๐ โ โ
)) |
10 | | simp1 1137 |
. . . . 5
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph )) |
11 | 10 | ancomd 463 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐บ โ FriendGraph โง ๐บ RegUSGraph ๐พ)) |
12 | 5 | frrusgrord 29594 |
. . . 4
โข ((๐ โ Fin โง ๐ โ โ
) โ ((๐บ โ FriendGraph โง ๐บ RegUSGraph ๐พ) โ (โฏโ๐) = ((๐พ ยท (๐พ โ 1)) + 1))) |
13 | 9, 11, 12 | sylc 65 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (โฏโ๐) = ((๐พ ยท (๐พ โ 1)) + 1)) |
14 | 13 | oveq1d 7424 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ๐) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
15 | 5 | numclwwlk7lem 29642 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐พ โ
โ0) |
16 | | nn0cn 12482 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ ๐พ โ
โ) |
17 | | peano2cnm 11526 |
. . . . . . . . . . 11
โข (๐พ โ โ โ (๐พ โ 1) โ
โ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โ) |
19 | 16, 18 | mulcomd 11235 |
. . . . . . . . 9
โข (๐พ โ โ0
โ (๐พ ยท (๐พ โ 1)) = ((๐พ โ 1) ยท ๐พ)) |
20 | 19 | oveq1d 7424 |
. . . . . . . 8
โข (๐พ โ โ0
โ ((๐พ ยท (๐พ โ 1)) mod ๐) = (((๐พ โ 1) ยท ๐พ) mod ๐)) |
21 | 20 | adantr 482 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((๐พ ยท (๐พ โ 1)) mod ๐) = (((๐พ โ 1) ยท ๐พ) mod ๐)) |
22 | | prmnn 16611 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
23 | 22 | ad2antrl 727 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โ
โ) |
24 | | nn0z 12583 |
. . . . . . . . . . 11
โข (๐พ โ โ0
โ ๐พ โ
โค) |
25 | | peano2zm 12605 |
. . . . . . . . . . 11
โข (๐พ โ โค โ (๐พ โ 1) โ
โค) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โค) |
27 | 26 | adantr 482 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐พ โ 1) โ
โค) |
28 | 24 | adantr 482 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐พ โ
โค) |
29 | 23, 27, 28 | 3jca 1129 |
. . . . . . . 8
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ โง (๐พ โ 1) โ โค โง
๐พ โ
โค)) |
30 | | simprr 772 |
. . . . . . . 8
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โฅ (๐พ โ 1)) |
31 | | mulmoddvds 16273 |
. . . . . . . 8
โข ((๐ โ โ โง (๐พ โ 1) โ โค โง
๐พ โ โค) โ
(๐ โฅ (๐พ โ 1) โ (((๐พ โ 1) ยท ๐พ) mod ๐) = 0)) |
32 | 29, 30, 31 | sylc 65 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ โ 1) ยท ๐พ) mod ๐) = 0) |
33 | 21, 32 | eqtrd 2773 |
. . . . . 6
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((๐พ ยท (๐พ โ 1)) mod ๐) = 0) |
34 | 22 | nnred 12227 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
35 | | prmgt1 16634 |
. . . . . . . . 9
โข (๐ โ โ โ 1 <
๐) |
36 | 34, 35 | jca 513 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ โ โง 1 <
๐)) |
37 | 36 | ad2antrl 727 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ โง 1 <
๐)) |
38 | | 1mod 13868 |
. . . . . . 7
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
39 | 37, 38 | syl 17 |
. . . . . 6
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (1 mod
๐) = 1) |
40 | 33, 39 | oveq12d 7427 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) = (0 + 1)) |
41 | 40 | oveq1d 7424 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = ((0 + 1) mod ๐)) |
42 | | nn0re 12481 |
. . . . . . 7
โข (๐พ โ โ0
โ ๐พ โ
โ) |
43 | | peano2rem 11527 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ) |
44 | 42, 43 | syl 17 |
. . . . . . 7
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โ) |
45 | 42, 44 | remulcld 11244 |
. . . . . 6
โข (๐พ โ โ0
โ (๐พ ยท (๐พ โ 1)) โ
โ) |
46 | 45 | adantr 482 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐พ ยท (๐พ โ 1)) โ
โ) |
47 | | 1red 11215 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ 1 โ
โ) |
48 | 22 | nnrpd 13014 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ+) |
49 | 48 | ad2antrl 727 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โ
โ+) |
50 | | modaddabs 13874 |
. . . . 5
โข (((๐พ ยท (๐พ โ 1)) โ โ โง 1 โ
โ โง ๐ โ
โ+) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
51 | 46, 47, 49, 50 | syl3anc 1372 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
52 | | 0p1e1 12334 |
. . . . . 6
โข (0 + 1) =
1 |
53 | 52 | oveq1i 7419 |
. . . . 5
โข ((0 + 1)
mod ๐) = (1 mod ๐) |
54 | 34, 35, 38 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ โ (1 mod
๐) = 1) |
55 | 54 | ad2antrl 727 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (1 mod
๐) = 1) |
56 | 53, 55 | eqtrid 2785 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((0 + 1)
mod ๐) =
1) |
57 | 41, 51, 56 | 3eqtr3d 2781 |
. . 3
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) + 1) mod ๐) = 1) |
58 | 15, 57 | stoic3 1779 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) + 1) mod ๐) = 1) |
59 | 7, 14, 58 | 3eqtrd 2777 |
1
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = 1) |