Step | Hyp | Ref
| Expression |
1 | | elfzelz 13450 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โค) |
2 | 1 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โค) |
3 | | peano2zm 12554 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ 1) โ โค) |
5 | 4 | zcnd 12616 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ 1) โ โ) |
6 | 2 | peano2zd 12618 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ + 1) โ โค) |
7 | 6 | zcnd 12616 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ + 1) โ โ) |
8 | 5, 7 | mulcomd 11184 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ โ 1) ยท (๐ + 1)) = ((๐ + 1) ยท (๐ โ 1))) |
9 | 2 | zcnd 12616 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
10 | | ax-1cn 11117 |
. . . . . . 7
โข 1 โ
โ |
11 | | subsq 14123 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ ((๐โ2)
โ (1โ2)) = ((๐ +
1) ยท (๐ โ
1))) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐โ2) โ (1โ2)) = ((๐ + 1) ยท (๐ โ 1))) |
13 | 9 | sqvald 14057 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐โ2) = (๐ ยท ๐)) |
14 | | sq1 14108 |
. . . . . . . 8
โข
(1โ2) = 1 |
15 | 14 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1โ2) =
1) |
16 | 13, 15 | oveq12d 7379 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐โ2) โ (1โ2)) = ((๐ ยท ๐) โ 1)) |
17 | 8, 12, 16 | 3eqtr2d 2779 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ โ 1) ยท (๐ + 1)) = ((๐ ยท ๐) โ 1)) |
18 | 17 | breq2d 5121 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ ((๐ โ 1) ยท (๐ + 1)) โ ๐ โฅ ((๐ ยท ๐) โ 1))) |
19 | | fz1ssfz0 13546 |
. . . . . 6
โข
(1...(๐ โ 1))
โ (0...(๐ โ
1)) |
20 | | simpr 486 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ (1...(๐ โ 1))) |
21 | 19, 20 | sselid 3946 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ (0...(๐ โ 1))) |
22 | 21 | biantrurd 534 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ ((๐ ยท ๐) โ 1) โ (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ ยท ๐) โ 1)))) |
23 | 18, 22 | bitrd 279 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ ((๐ โ 1) ยท (๐ + 1)) โ (๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ ยท ๐) โ 1)))) |
24 | | simpl 484 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
25 | | euclemma 16597 |
. . . 4
โข ((๐ โ โ โง (๐ โ 1) โ โค โง
(๐ + 1) โ โค)
โ (๐ โฅ ((๐ โ 1) ยท (๐ + 1)) โ (๐ โฅ (๐ โ 1) โจ ๐ โฅ (๐ + 1)))) |
26 | 24, 4, 6, 25 | syl3anc 1372 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ ((๐ โ 1) ยท (๐ + 1)) โ (๐ โฅ (๐ โ 1) โจ ๐ โฅ (๐ + 1)))) |
27 | | prmnn 16558 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
28 | | fzm1ndvds 16212 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐) |
29 | 27, 28 | sylan 581 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐) |
30 | | eqid 2733 |
. . . . 5
โข ((๐โ(๐ โ 2)) mod ๐) = ((๐โ(๐ โ 2)) mod ๐) |
31 | 30 | prmdiveq 16666 |
. . . 4
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ ((๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ ยท ๐) โ 1)) โ ๐ = ((๐โ(๐ โ 2)) mod ๐))) |
32 | 24, 2, 29, 31 | syl3anc 1372 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ โ (0...(๐ โ 1)) โง ๐ โฅ ((๐ ยท ๐) โ 1)) โ ๐ = ((๐โ(๐ โ 2)) mod ๐))) |
33 | 23, 26, 32 | 3bitr3rd 310 |
. 2
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (๐ โฅ (๐ โ 1) โจ ๐ โฅ (๐ + 1)))) |
34 | 24, 27 | syl 17 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
35 | | 1zzd 12542 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ 1 โ
โค) |
36 | | moddvds 16155 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค โง 1 โ
โค) โ ((๐ mod
๐) = (1 mod ๐) โ ๐ โฅ (๐ โ 1))) |
37 | 34, 2, 35, 36 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ mod ๐) = (1 mod ๐) โ ๐ โฅ (๐ โ 1))) |
38 | | elfznn 13479 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
39 | 38 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
40 | 39 | nnred 12176 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
41 | 34 | nnrpd 12963 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
โ+) |
42 | 39 | nnnn0d 12481 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
โ0) |
43 | 42 | nn0ge0d 12484 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ 0 โค ๐) |
44 | | elfzle2 13454 |
. . . . . . . 8
โข (๐ โ (1...(๐ โ 1)) โ ๐ โค (๐ โ 1)) |
45 | 44 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โค (๐ โ 1)) |
46 | | prmz 16559 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
47 | | zltlem1 12564 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
48 | 1, 46, 47 | syl2anr 598 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
49 | 45, 48 | mpbird 257 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ < ๐) |
50 | | modid 13810 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ+)
โง (0 โค ๐ โง ๐ < ๐)) โ (๐ mod ๐) = ๐) |
51 | 40, 41, 43, 49, 50 | syl22anc 838 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ mod ๐) = ๐) |
52 | 34 | nnred 12176 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
53 | | prmuz2 16580 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
54 | 24, 53 | syl 17 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ
(โคโฅโ2)) |
55 | | eluz2gt1 12853 |
. . . . . . 7
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
56 | 54, 55 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ 1 < ๐) |
57 | | 1mod 13817 |
. . . . . 6
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
58 | 52, 56, 57 | syl2anc 585 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1 mod ๐) = 1) |
59 | 51, 58 | eqeq12d 2749 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ mod ๐) = (1 mod ๐) โ ๐ = 1)) |
60 | 37, 59 | bitr3d 281 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ (๐ โ 1) โ ๐ = 1)) |
61 | 35 | znegcld 12617 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ -1 โ
โค) |
62 | | moddvds 16155 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค โง -1 โ
โค) โ ((๐ mod
๐) = (-1 mod ๐) โ ๐ โฅ (๐ โ -1))) |
63 | 34, 2, 61, 62 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ mod ๐) = (-1 mod ๐) โ ๐ โฅ (๐ โ -1))) |
64 | 34 | nncnd 12177 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ๐ โ โ) |
65 | 64 | mullidd 11181 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (1 ยท ๐) = ๐) |
66 | 65 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (-1 + (1 ยท ๐)) = (-1 + ๐)) |
67 | | neg1cn 12275 |
. . . . . . . . 9
โข -1 โ
โ |
68 | | addcom 11349 |
. . . . . . . . 9
โข ((-1
โ โ โง ๐
โ โ) โ (-1 + ๐) = (๐ + -1)) |
69 | 67, 64, 68 | sylancr 588 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (-1 + ๐) = (๐ + -1)) |
70 | | negsub 11457 |
. . . . . . . . 9
โข ((๐ โ โ โง 1 โ
โ) โ (๐ + -1) =
(๐ โ
1)) |
71 | 64, 10, 70 | sylancl 587 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ + -1) = (๐ โ 1)) |
72 | 66, 69, 71 | 3eqtrd 2777 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (-1 + (1 ยท ๐)) = (๐ โ 1)) |
73 | 72 | oveq1d 7376 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((-1 + (1 ยท
๐)) mod ๐) = ((๐ โ 1) mod ๐)) |
74 | | neg1rr 12276 |
. . . . . . . 8
โข -1 โ
โ |
75 | 74 | a1i 11 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ -1 โ
โ) |
76 | | modcyc 13820 |
. . . . . . 7
โข ((-1
โ โ โง ๐
โ โ+ โง 1 โ โค) โ ((-1 + (1 ยท
๐)) mod ๐) = (-1 mod ๐)) |
77 | 75, 41, 35, 76 | syl3anc 1372 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((-1 + (1 ยท
๐)) mod ๐) = (-1 mod ๐)) |
78 | | peano2rem 11476 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
79 | 52, 78 | syl 17 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ 1) โ โ) |
80 | | nnm1nn0 12462 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
81 | 34, 80 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ 1) โ
โ0) |
82 | 81 | nn0ge0d 12484 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ 0 โค (๐ โ 1)) |
83 | 52 | ltm1d 12095 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ 1) < ๐) |
84 | | modid 13810 |
. . . . . . 7
โข ((((๐ โ 1) โ โ โง
๐ โ
โ+) โง (0 โค (๐ โ 1) โง (๐ โ 1) < ๐)) โ ((๐ โ 1) mod ๐) = (๐ โ 1)) |
85 | 79, 41, 82, 83, 84 | syl22anc 838 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ โ 1) mod ๐) = (๐ โ 1)) |
86 | 73, 77, 85 | 3eqtr3d 2781 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (-1 mod ๐) = (๐ โ 1)) |
87 | 51, 86 | eqeq12d 2749 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ mod ๐) = (-1 mod ๐) โ ๐ = (๐ โ 1))) |
88 | | subneg 11458 |
. . . . . 6
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
-1) = (๐ +
1)) |
89 | 9, 10, 88 | sylancl 587 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โ -1) = (๐ + 1)) |
90 | 89 | breq2d 5121 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ (๐ โ -1) โ ๐ โฅ (๐ + 1))) |
91 | 63, 87, 90 | 3bitr3rd 310 |
. . 3
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ โฅ (๐ + 1) โ ๐ = (๐ โ 1))) |
92 | 60, 91 | orbi12d 918 |
. 2
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ((๐ โฅ (๐ โ 1) โจ ๐ โฅ (๐ + 1)) โ (๐ = 1 โจ ๐ = (๐ โ 1)))) |
93 | 33, 92 | bitrd 279 |
1
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (๐ = 1 โจ ๐ = (๐ โ 1)))) |