Step | Hyp | Ref
| Expression |
1 | | simpll 763 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐บ RegUSGraph ๐พ) |
2 | | simplr 765 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐บ โ FriendGraph
) |
3 | | simprr 769 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐ โ Fin) |
4 | 1, 2, 3 | 3jca 1126 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ (๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph โง ๐ โ Fin)) |
5 | | numclwwlk6.v |
. . . 4
โข ๐ = (Vtxโ๐บ) |
6 | 5 | numclwwlk6 29910 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = ((โฏโ๐) mod ๐)) |
7 | 4, 6 | stoic3 1776 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = ((โฏโ๐) mod ๐)) |
8 | | simp2 1135 |
. . . . 5
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ
โง ๐ โ Fin)) |
9 | 8 | ancomd 460 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐ โ Fin โง ๐ โ โ
)) |
10 | | simp1 1134 |
. . . . 5
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph )) |
11 | 10 | ancomd 460 |
. . . 4
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (๐บ โ FriendGraph โง ๐บ RegUSGraph ๐พ)) |
12 | 5 | frrusgrord 29861 |
. . . 4
โข ((๐ โ Fin โง ๐ โ โ
) โ ((๐บ โ FriendGraph โง ๐บ RegUSGraph ๐พ) โ (โฏโ๐) = ((๐พ ยท (๐พ โ 1)) + 1))) |
13 | 9, 11, 12 | sylc 65 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (โฏโ๐) = ((๐พ ยท (๐พ โ 1)) + 1)) |
14 | 13 | oveq1d 7426 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ๐) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
15 | 5 | numclwwlk7lem 29909 |
. . 3
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin)) โ ๐พ โ
โ0) |
16 | | nn0cn 12486 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ ๐พ โ
โ) |
17 | | peano2cnm 11530 |
. . . . . . . . . . 11
โข (๐พ โ โ โ (๐พ โ 1) โ
โ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โ) |
19 | 16, 18 | mulcomd 11239 |
. . . . . . . . 9
โข (๐พ โ โ0
โ (๐พ ยท (๐พ โ 1)) = ((๐พ โ 1) ยท ๐พ)) |
20 | 19 | oveq1d 7426 |
. . . . . . . 8
โข (๐พ โ โ0
โ ((๐พ ยท (๐พ โ 1)) mod ๐) = (((๐พ โ 1) ยท ๐พ) mod ๐)) |
21 | 20 | adantr 479 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((๐พ ยท (๐พ โ 1)) mod ๐) = (((๐พ โ 1) ยท ๐พ) mod ๐)) |
22 | | prmnn 16615 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
23 | 22 | ad2antrl 724 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โ
โ) |
24 | | nn0z 12587 |
. . . . . . . . . . 11
โข (๐พ โ โ0
โ ๐พ โ
โค) |
25 | | peano2zm 12609 |
. . . . . . . . . . 11
โข (๐พ โ โค โ (๐พ โ 1) โ
โค) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โค) |
27 | 26 | adantr 479 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐พ โ 1) โ
โค) |
28 | 24 | adantr 479 |
. . . . . . . . 9
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐พ โ
โค) |
29 | 23, 27, 28 | 3jca 1126 |
. . . . . . . 8
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ โง (๐พ โ 1) โ โค โง
๐พ โ
โค)) |
30 | | simprr 769 |
. . . . . . . 8
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โฅ (๐พ โ 1)) |
31 | | mulmoddvds 16277 |
. . . . . . . 8
โข ((๐ โ โ โง (๐พ โ 1) โ โค โง
๐พ โ โค) โ
(๐ โฅ (๐พ โ 1) โ (((๐พ โ 1) ยท ๐พ) mod ๐) = 0)) |
32 | 29, 30, 31 | sylc 65 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ โ 1) ยท ๐พ) mod ๐) = 0) |
33 | 21, 32 | eqtrd 2770 |
. . . . . 6
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((๐พ ยท (๐พ โ 1)) mod ๐) = 0) |
34 | 22 | nnred 12231 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
35 | | prmgt1 16638 |
. . . . . . . . 9
โข (๐ โ โ โ 1 <
๐) |
36 | 34, 35 | jca 510 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ โ โง 1 <
๐)) |
37 | 36 | ad2antrl 724 |
. . . . . . 7
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐ โ โ โง 1 <
๐)) |
38 | | 1mod 13872 |
. . . . . . 7
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
39 | 37, 38 | syl 17 |
. . . . . 6
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (1 mod
๐) = 1) |
40 | 33, 39 | oveq12d 7429 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) = (0 + 1)) |
41 | 40 | oveq1d 7426 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = ((0 + 1) mod ๐)) |
42 | | nn0re 12485 |
. . . . . . 7
โข (๐พ โ โ0
โ ๐พ โ
โ) |
43 | | peano2rem 11531 |
. . . . . . . 8
โข (๐พ โ โ โ (๐พ โ 1) โ
โ) |
44 | 42, 43 | syl 17 |
. . . . . . 7
โข (๐พ โ โ0
โ (๐พ โ 1) โ
โ) |
45 | 42, 44 | remulcld 11248 |
. . . . . 6
โข (๐พ โ โ0
โ (๐พ ยท (๐พ โ 1)) โ
โ) |
46 | 45 | adantr 479 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (๐พ ยท (๐พ โ 1)) โ
โ) |
47 | | 1red 11219 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ 1 โ
โ) |
48 | 22 | nnrpd 13018 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ+) |
49 | 48 | ad2antrl 724 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ๐ โ
โ+) |
50 | | modaddabs 13878 |
. . . . 5
โข (((๐พ ยท (๐พ โ 1)) โ โ โง 1 โ
โ โง ๐ โ
โ+) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
51 | 46, 47, 49, 50 | syl3anc 1369 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((((๐พ ยท (๐พ โ 1)) mod ๐) + (1 mod ๐)) mod ๐) = (((๐พ ยท (๐พ โ 1)) + 1) mod ๐)) |
52 | | 0p1e1 12338 |
. . . . . 6
โข (0 + 1) =
1 |
53 | 52 | oveq1i 7421 |
. . . . 5
โข ((0 + 1)
mod ๐) = (1 mod ๐) |
54 | 34, 35, 38 | syl2anc 582 |
. . . . . 6
โข (๐ โ โ โ (1 mod
๐) = 1) |
55 | 54 | ad2antrl 724 |
. . . . 5
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (1 mod
๐) = 1) |
56 | 53, 55 | eqtrid 2782 |
. . . 4
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ ((0 + 1)
mod ๐) =
1) |
57 | 41, 51, 56 | 3eqtr3d 2778 |
. . 3
โข ((๐พ โ โ0
โง (๐ โ โ
โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) + 1) mod ๐) = 1) |
58 | 15, 57 | stoic3 1776 |
. 2
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ (((๐พ ยท (๐พ โ 1)) + 1) mod ๐) = 1) |
59 | 7, 14, 58 | 3eqtrd 2774 |
1
โข (((๐บ RegUSGraph ๐พ โง ๐บ โ FriendGraph ) โง (๐ โ โ
โง ๐ โ Fin) โง (๐ โ โ โง ๐ โฅ (๐พ โ 1))) โ ((โฏโ(๐ ClWWalksN ๐บ)) mod ๐) = 1) |