Step | Hyp | Ref
| Expression |
1 | | 1zzd 12598 |
. . 3
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 1 โ
โค) |
2 | | lgseisen.1 |
. . . . . 6
โข (๐ โ ๐ โ (โ โ
{2})) |
3 | 2 | adantr 480 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ (โ โ
{2})) |
4 | | oddprm 16748 |
. . . . 5
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
5 | 3, 4 | syl 17 |
. . . 4
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) โ
โ) |
6 | 5 | nnzd 12590 |
. . 3
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ โ 1) / 2) โ
โค) |
7 | | neg1cn 12331 |
. . . . . . . . . . . . 13
โข -1 โ
โ |
8 | 7 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ -1 โ
โ) |
9 | | neg1ne0 12333 |
. . . . . . . . . . . . 13
โข -1 โ
0 |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ -1 โ
0) |
11 | | 2z 12599 |
. . . . . . . . . . . . 13
โข 2 โ
โค |
12 | 11 | a1i 11 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ 2 โ
โค) |
13 | | simpr 484 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (๐
/ 2) โ
โค) |
14 | | expmulz 14079 |
. . . . . . . . . . . 12
โข (((-1
โ โ โง -1 โ 0) โง (2 โ โค โง (๐
/ 2) โ โค)) โ
(-1โ(2 ยท (๐
/
2))) = ((-1โ2)โ(๐
/ 2))) |
15 | 8, 10, 12, 13, 14 | syl22anc 836 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (-1โ(2
ยท (๐
/ 2))) =
((-1โ2)โ(๐
/
2))) |
16 | | lgseisen.4 |
. . . . . . . . . . . . . . . . . 18
โข ๐
= ((๐ ยท (2 ยท ๐ฅ)) mod ๐) |
17 | | lgseisen.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ โ (โ โ
{2})) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ (โ โ
{2})) |
19 | 18 | eldifad 3961 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
20 | | prmz 16617 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ ๐ โ
โค) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โค) |
22 | | elfzelz 13506 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โ โค) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โ โค) |
24 | | zmulcl 12616 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((2
โ โค โง ๐ฅ
โ โค) โ (2 ยท ๐ฅ) โ โค) |
25 | 11, 23, 24 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 ยท ๐ฅ) โ
โค) |
26 | 21, 25 | zmulcld 12677 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ ยท (2 ยท ๐ฅ)) โ โค) |
27 | 3 | eldifad 3961 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
28 | | prmnn 16616 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
30 | | zmodfz 13863 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ ยท (2 ยท ๐ฅ)) โ โค โง ๐ โ โ) โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) โ (0...(๐ โ 1))) |
31 | 26, 29, 30 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) โ (0...(๐ โ 1))) |
32 | 16, 31 | eqeltrid 2836 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ (0...(๐ โ 1))) |
33 | | elfznn0 13599 |
. . . . . . . . . . . . . . . . 17
โข (๐
โ (0...(๐ โ 1)) โ ๐
โ
โ0) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ
โ0) |
35 | 34 | nn0zd 12589 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ โค) |
36 | 35 | zcnd 12672 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ โ) |
37 | 36 | adantr 480 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ ๐
โ
โ) |
38 | | 2cnd 12295 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ 2 โ
โ) |
39 | | 2ne0 12321 |
. . . . . . . . . . . . . 14
โข 2 โ
0 |
40 | 39 | a1i 11 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ 2 โ
0) |
41 | 37, 38, 40 | divcan2d 11997 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (2 ยท
(๐
/ 2)) = ๐
) |
42 | 41 | oveq2d 7428 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (-1โ(2
ยท (๐
/ 2))) =
(-1โ๐
)) |
43 | | neg1sqe1 14165 |
. . . . . . . . . . . . 13
โข
(-1โ2) = 1 |
44 | 43 | oveq1i 7422 |
. . . . . . . . . . . 12
โข
((-1โ2)โ(๐
/ 2)) = (1โ(๐
/
2)) |
45 | | 1exp 14062 |
. . . . . . . . . . . . 13
โข ((๐
/ 2) โ โค โ
(1โ(๐
/ 2)) =
1) |
46 | 45 | adantl 481 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (1โ(๐
/ 2)) = 1) |
47 | 44, 46 | eqtrid 2783 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ
((-1โ2)โ(๐
/ 2))
= 1) |
48 | 15, 42, 47 | 3eqtr3d 2779 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (-1โ๐
) = 1) |
49 | 48 | oveq1d 7427 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ ((-1โ๐
) ยท ๐
) = (1 ยท ๐
)) |
50 | 37 | mullidd 11237 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (1 ยท
๐
) = ๐
) |
51 | 49, 50 | eqtrd 2771 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ ((-1โ๐
) ยท ๐
) = ๐
) |
52 | 51 | oveq1d 7427 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ
(((-1โ๐
) ยท
๐
) mod ๐) = (๐
mod ๐)) |
53 | 34 | nn0red 12538 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ โ) |
54 | 29 | nnrpd 13019 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ
โ+) |
55 | 34 | nn0ge0d 12540 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 0 โค ๐
) |
56 | 26 | zred 12671 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ ยท (2 ยท ๐ฅ)) โ โ) |
57 | | modlt 13850 |
. . . . . . . . . . 11
โข (((๐ ยท (2 ยท ๐ฅ)) โ โ โง ๐ โ โ+)
โ ((๐ ยท (2
ยท ๐ฅ)) mod ๐) < ๐) |
58 | 56, 54, 57 | syl2anc 583 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) < ๐) |
59 | 16, 58 | eqbrtrid 5184 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
< ๐) |
60 | | modid 13866 |
. . . . . . . . 9
โข (((๐
โ โ โง ๐ โ โ+)
โง (0 โค ๐
โง ๐
< ๐)) โ (๐
mod ๐) = ๐
) |
61 | 53, 54, 55, 59, 60 | syl22anc 836 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐
mod ๐) = ๐
) |
62 | 61 | adantr 480 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ (๐
mod ๐) = ๐
) |
63 | 52, 62 | eqtrd 2771 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ
(((-1โ๐
) ยท
๐
) mod ๐) = ๐
) |
64 | 63 | oveq1d 7427 |
. . . . 5
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ
((((-1โ๐
) ยท
๐
) mod ๐) / 2) = (๐
/ 2)) |
65 | 64, 13 | eqeltrd 2832 |
. . . 4
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง (๐
/ 2) โ โค) โ
((((-1โ๐
) ยท
๐
) mod ๐) / 2) โ โค) |
66 | 29 | nncnd 12233 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
67 | 66 | mullidd 11237 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (1 ยท ๐) = ๐) |
68 | 67 | oveq2d 7428 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-๐
+ (1 ยท ๐)) = (-๐
+ ๐)) |
69 | 53 | renegcld 11646 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ -๐
โ โ) |
70 | 69 | recnd 11247 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ -๐
โ โ) |
71 | 66, 70 | addcomd 11421 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ + -๐
) = (-๐
+ ๐)) |
72 | 66, 36 | negsubd 11582 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ + -๐
) = (๐ โ ๐
)) |
73 | 68, 71, 72 | 3eqtr2d 2777 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-๐
+ (1 ยท ๐)) = (๐ โ ๐
)) |
74 | 73 | oveq1d 7427 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-๐
+ (1 ยท ๐)) mod ๐) = ((๐ โ ๐
) mod ๐)) |
75 | | modcyc 13876 |
. . . . . . . . . . 11
โข ((-๐
โ โ โง ๐ โ โ+
โง 1 โ โค) โ ((-๐
+ (1 ยท ๐)) mod ๐) = (-๐
mod ๐)) |
76 | 69, 54, 1, 75 | syl3anc 1370 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-๐
+ (1 ยท ๐)) mod ๐) = (-๐
mod ๐)) |
77 | 29 | nnred 12232 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โ) |
78 | 77, 53 | resubcld 11647 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ ๐
) โ โ) |
79 | 53, 77, 59 | ltled 11367 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โค ๐) |
80 | 77, 53 | subge0d 11809 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (0 โค (๐ โ ๐
) โ ๐
โค ๐)) |
81 | 79, 80 | mpbird 256 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 0 โค (๐ โ ๐
)) |
82 | | 2nn 12290 |
. . . . . . . . . . . . . . . . . . . . . 22
โข 2 โ
โ |
83 | | elfznn 13535 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โ โ) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โ โ) |
85 | | nnmulcl 12241 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยท ๐ฅ) โ โ) |
86 | 82, 84, 85 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 ยท ๐ฅ) โ
โ) |
87 | | elfzle2 13510 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ โ (1...((๐ โ 1) / 2)) โ ๐ฅ โค ((๐ โ 1) / 2)) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โค ((๐ โ 1) / 2)) |
89 | 84 | nnred 12232 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ฅ โ โ) |
90 | | prmuz2 16638 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
91 | | uz2m1nn 12912 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
92 | 27, 90, 91 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ 1) โ โ) |
93 | 92 | nnred 12232 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ 1) โ โ) |
94 | | 2re 12291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โ |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 2 โ
โ) |
96 | | 2pos 12320 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 0 <
2 |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 0 <
2) |
98 | | lemuldiv2 12100 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ โ โง (๐ โ 1) โ โ โง
(2 โ โ โง 0 < 2)) โ ((2 ยท ๐ฅ) โค (๐ โ 1) โ ๐ฅ โค ((๐ โ 1) / 2))) |
99 | 89, 93, 95, 97, 98 | syl112anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((2 ยท ๐ฅ) โค (๐ โ 1) โ ๐ฅ โค ((๐ โ 1) / 2))) |
100 | 88, 99 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 ยท ๐ฅ) โค (๐ โ 1)) |
101 | | prmz 16617 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โค) |
102 | 27, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ โค) |
103 | | peano2zm 12610 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
104 | | fznn 13574 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ 1) โ โค
โ ((2 ยท ๐ฅ)
โ (1...(๐ โ 1))
โ ((2 ยท ๐ฅ)
โ โ โง (2 ยท ๐ฅ) โค (๐ โ 1)))) |
105 | 102, 103,
104 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((2 ยท ๐ฅ) โ (1...(๐ โ 1)) โ ((2 ยท ๐ฅ) โ โ โง (2
ยท ๐ฅ) โค (๐ โ 1)))) |
106 | 86, 100, 105 | mpbir2and 710 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 ยท ๐ฅ) โ (1...(๐ โ 1))) |
107 | | fzm1ndvds 16270 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (2
ยท ๐ฅ) โ
(1...(๐ โ 1))) โ
ยฌ ๐ โฅ (2 ยท
๐ฅ)) |
108 | 29, 106, 107 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ (2 ยท ๐ฅ)) |
109 | | lgseisen.3 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ โ ๐) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐ โ ๐) |
111 | | prmrp 16654 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
112 | 27, 19, 111 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
113 | 110, 112 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ gcd ๐) = 1) |
114 | | coprmdvds 16595 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โค โง ๐ โ โค โง (2
ยท ๐ฅ) โ โค)
โ ((๐ โฅ (๐ ยท (2 ยท ๐ฅ)) โง (๐ gcd ๐) = 1) โ ๐ โฅ (2 ยท ๐ฅ))) |
115 | 102, 21, 25, 114 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ โฅ (๐ ยท (2 ยท ๐ฅ)) โง (๐ gcd ๐) = 1) โ ๐ โฅ (2 ยท ๐ฅ))) |
116 | 113, 115 | mpan2d 691 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ (๐ ยท (2 ยท ๐ฅ)) โ ๐ โฅ (2 ยท ๐ฅ))) |
117 | 108, 116 | mtod 197 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ (๐ ยท (2 ยท ๐ฅ))) |
118 | | dvdsval3 16206 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (๐ ยท (2 ยท ๐ฅ)) โ โค) โ (๐ โฅ (๐ ยท (2 ยท ๐ฅ)) โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) = 0)) |
119 | 29, 26, 118 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ (๐ ยท (2 ยท ๐ฅ)) โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) = 0)) |
120 | 117, 119 | mtbid 323 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) = 0) |
121 | 16 | eqeq1i 2736 |
. . . . . . . . . . . . . . . . 17
โข (๐
= 0 โ ((๐ ยท (2 ยท ๐ฅ)) mod ๐) = 0) |
122 | 120, 121 | sylnibr 328 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐
= 0) |
123 | 92 | nnnn0d 12537 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ 1) โ
โ0) |
124 | | nn0uz 12869 |
. . . . . . . . . . . . . . . . . . . 20
โข
โ0 = (โคโฅโ0) |
125 | 123, 124 | eleqtrdi 2842 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ 1) โ
(โคโฅโ0)) |
126 | | elfzp12 13585 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ 1) โ
(โคโฅโ0) โ (๐
โ (0...(๐ โ 1)) โ (๐
= 0 โจ ๐
โ ((0 + 1)...(๐ โ 1))))) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐
โ (0...(๐ โ 1)) โ (๐
= 0 โจ ๐
โ ((0 + 1)...(๐ โ 1))))) |
128 | 32, 127 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐
= 0 โจ ๐
โ ((0 + 1)...(๐ โ 1)))) |
129 | 128 | ord 861 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (ยฌ ๐
= 0 โ ๐
โ ((0 + 1)...(๐ โ 1)))) |
130 | 122, 129 | mpd 15 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ ((0 + 1)...(๐ โ 1))) |
131 | | 1e0p1 12724 |
. . . . . . . . . . . . . . . 16
โข 1 = (0 +
1) |
132 | 131 | oveq1i 7422 |
. . . . . . . . . . . . . . 15
โข
(1...(๐ โ 1))
= ((0 + 1)...(๐ โ
1)) |
133 | 130, 132 | eleqtrrdi 2843 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ (1...(๐ โ 1))) |
134 | | elfznn 13535 |
. . . . . . . . . . . . . 14
โข (๐
โ (1...(๐ โ 1)) โ ๐
โ โ) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ โ) |
136 | 135 | nnrpd 13019 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ๐
โ
โ+) |
137 | 77, 136 | ltsubrpd 13053 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ ๐
) < ๐) |
138 | | modid 13866 |
. . . . . . . . . . 11
โข ((((๐ โ ๐
) โ โ โง ๐ โ โ+) โง (0 โค
(๐ โ ๐
) โง (๐ โ ๐
) < ๐)) โ ((๐ โ ๐
) mod ๐) = (๐ โ ๐
)) |
139 | 78, 54, 81, 137, 138 | syl22anc 836 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐ โ ๐
) mod ๐) = (๐ โ ๐
)) |
140 | 74, 76, 139 | 3eqtr3d 2779 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-๐
mod ๐) = (๐ โ ๐
)) |
141 | 140 | adantr 480 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (-๐
mod ๐) = (๐ โ ๐
)) |
142 | | ax-1cn 11171 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
143 | 142 | a1i 11 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 1 โ
โ) |
144 | 135 | adantr 480 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ๐
โ
โ) |
145 | 35 | peano2zd 12674 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐
+ 1) โ โค) |
146 | | dvdsval2 16205 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โค โง 2 โ 0 โง (๐
+ 1) โ โค) โ (2 โฅ
(๐
+ 1) โ ((๐
+ 1) / 2) โ
โค)) |
147 | 11, 39, 145, 146 | mp3an12i 1464 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (2 โฅ (๐
+ 1) โ ((๐
+ 1) / 2) โ โค)) |
148 | 147 | biimpar 477 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 2 โฅ
(๐
+ 1)) |
149 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ๐
โ
โค) |
150 | 82 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 2 โ
โ) |
151 | | 1lt2 12388 |
. . . . . . . . . . . . . . . 16
โข 1 <
2 |
152 | 151 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 1 <
2) |
153 | | ndvdsp1 16359 |
. . . . . . . . . . . . . . 15
โข ((๐
โ โค โง 2 โ
โ โง 1 < 2) โ (2 โฅ ๐
โ ยฌ 2 โฅ (๐
+ 1))) |
154 | 149, 150,
152, 153 | syl3anc 1370 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (2 โฅ
๐
โ ยฌ 2 โฅ
(๐
+ 1))) |
155 | 148, 154 | mt2d 136 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ยฌ 2
โฅ ๐
) |
156 | | oexpneg 16293 |
. . . . . . . . . . . . 13
โข ((1
โ โ โง ๐
โ โ โง ยฌ 2 โฅ ๐
) โ (-1โ๐
) = -(1โ๐
)) |
157 | 143, 144,
155, 156 | syl3anc 1370 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
(-1โ๐
) =
-(1โ๐
)) |
158 | | 1exp 14062 |
. . . . . . . . . . . . . 14
โข (๐
โ โค โ
(1โ๐
) =
1) |
159 | 149, 158 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
(1โ๐
) =
1) |
160 | 159 | negeqd 11459 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
-(1โ๐
) =
-1) |
161 | 157, 160 | eqtrd 2771 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
(-1โ๐
) =
-1) |
162 | 161 | oveq1d 7427 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
((-1โ๐
) ยท ๐
) = (-1 ยท ๐
)) |
163 | 36 | adantr 480 |
. . . . . . . . . . 11
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ๐
โ
โ) |
164 | 163 | mulm1d 11671 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (-1
ยท ๐
) = -๐
) |
165 | 162, 164 | eqtrd 2771 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
((-1โ๐
) ยท ๐
) = -๐
) |
166 | 165 | oveq1d 7427 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
(((-1โ๐
) ยท
๐
) mod ๐) = (-๐
mod ๐)) |
167 | 66 | adantr 480 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ๐ โ
โ) |
168 | 167, 163,
143 | pnpcan2d 11614 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ + 1) โ (๐
+ 1)) = (๐ โ ๐
)) |
169 | 141, 166,
168 | 3eqtr4d 2781 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
(((-1โ๐
) ยท
๐
) mod ๐) = ((๐ + 1) โ (๐
+ 1))) |
170 | 169 | oveq1d 7427 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
((((-1โ๐
) ยท
๐
) mod ๐) / 2) = (((๐ + 1) โ (๐
+ 1)) / 2)) |
171 | | peano2cn 11391 |
. . . . . . . 8
โข (๐ โ โ โ (๐ + 1) โ
โ) |
172 | 167, 171 | syl 17 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (๐ + 1) โ
โ) |
173 | | peano2cn 11391 |
. . . . . . . 8
โข (๐
โ โ โ (๐
+ 1) โ
โ) |
174 | 163, 173 | syl 17 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (๐
+ 1) โ
โ) |
175 | | 2cnd 12295 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 2 โ
โ) |
176 | 39 | a1i 11 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ 2 โ
0) |
177 | 172, 174,
175, 176 | divsubdird 12034 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (((๐ + 1) โ (๐
+ 1)) / 2) = (((๐ + 1) / 2) โ ((๐
+ 1) / 2))) |
178 | 170, 177 | eqtrd 2771 |
. . . . 5
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
((((-1โ๐
) ยท
๐
) mod ๐) / 2) = (((๐ + 1) / 2) โ ((๐
+ 1) / 2))) |
179 | 167, 143,
175 | subadd23d 11598 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ โ 1) + 2) = (๐ + (2 โ
1))) |
180 | | 2m1e1 12343 |
. . . . . . . . . . 11
โข (2
โ 1) = 1 |
181 | 180 | oveq2i 7423 |
. . . . . . . . . 10
โข (๐ + (2 โ 1)) = (๐ + 1) |
182 | 179, 181 | eqtr2di 2788 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (๐ + 1) = ((๐ โ 1) + 2)) |
183 | 182 | oveq1d 7427 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ + 1) / 2) = (((๐ โ 1) + 2) /
2)) |
184 | 92 | nncnd 12233 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โ 1) โ โ) |
185 | 184 | adantr 480 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (๐ โ 1) โ
โ) |
186 | 185, 175,
175, 176 | divdird 12033 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (((๐ โ 1) + 2) / 2) = (((๐ โ 1) / 2) + (2 /
2))) |
187 | | 2div2e1 12358 |
. . . . . . . . . 10
โข (2 / 2) =
1 |
188 | 187 | oveq2i 7423 |
. . . . . . . . 9
โข (((๐ โ 1) / 2) + (2 / 2)) =
(((๐ โ 1) / 2) +
1) |
189 | 186, 188 | eqtrdi 2787 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (((๐ โ 1) + 2) / 2) = (((๐ โ 1) / 2) +
1)) |
190 | 183, 189 | eqtrd 2771 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ + 1) / 2) = (((๐ โ 1) / 2) +
1)) |
191 | 6 | adantr 480 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ โ 1) / 2) โ
โค) |
192 | 191 | peano2zd 12674 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (((๐ โ 1) / 2) + 1) โ
โค) |
193 | 190, 192 | eqeltrd 2832 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐ + 1) / 2) โ
โค) |
194 | | simpr 484 |
. . . . . 6
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ ((๐
+ 1) / 2) โ
โค) |
195 | 193, 194 | zsubcld 12676 |
. . . . 5
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ (((๐ + 1) / 2) โ ((๐
+ 1) / 2)) โ
โค) |
196 | 178, 195 | eqeltrd 2832 |
. . . 4
โข (((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โง ((๐
+ 1) / 2) โ โค) โ
((((-1โ๐
) ยท
๐
) mod ๐) / 2) โ โค) |
197 | | zeo 12653 |
. . . . 5
โข (๐
โ โค โ ((๐
/ 2) โ โค โจ
((๐
+ 1) / 2) โ
โค)) |
198 | 35, 197 | syl 17 |
. . . 4
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((๐
/ 2) โ โค โจ
((๐
+ 1) / 2) โ
โค)) |
199 | 65, 196, 198 | mpjaodan 956 |
. . 3
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โ โค) |
200 | | m1expcl 14057 |
. . . . . . . . . 10
โข (๐
โ โค โ
(-1โ๐
) โ
โค) |
201 | 35, 200 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-1โ๐
) โ
โค) |
202 | 201, 35 | zmulcld 12677 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-1โ๐
) ยท ๐
) โ โค) |
203 | 202, 29 | zmodcld 13862 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท ๐
) mod ๐) โ
โ0) |
204 | 203 | nn0red 12538 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท ๐
) mod ๐) โ โ) |
205 | | fzm1ndvds 16270 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐
โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐
) |
206 | 29, 133, 205 | syl2anc 583 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ ๐
) |
207 | | ax-1ne0 11182 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
0 |
208 | | divneg2 11943 |
. . . . . . . . . . . . . . . . . . . 20
โข ((1
โ โ โง 1 โ โ โง 1 โ 0) โ -(1 / 1) = (1 /
-1)) |
209 | 142, 142,
207, 208 | mp3an 1460 |
. . . . . . . . . . . . . . . . . . 19
โข -(1 / 1)
= (1 / -1) |
210 | | 1div1e1 11909 |
. . . . . . . . . . . . . . . . . . . 20
โข (1 / 1) =
1 |
211 | 210 | negeqi 11458 |
. . . . . . . . . . . . . . . . . . 19
โข -(1 / 1)
= -1 |
212 | 209, 211 | eqtr3i 2761 |
. . . . . . . . . . . . . . . . . 18
โข (1 / -1)
= -1 |
213 | 212 | oveq1i 7422 |
. . . . . . . . . . . . . . . . 17
โข ((1 /
-1)โ๐
) =
(-1โ๐
) |
214 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ -1 โ
โ) |
215 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ -1 โ
0) |
216 | 214, 215,
35 | exprecd 14124 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((1 /
-1)โ๐
) = (1 /
(-1โ๐
))) |
217 | 213, 216 | eqtr3id 2785 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-1โ๐
) = (1 / (-1โ๐
))) |
218 | 217 | oveq2d 7428 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-1โ๐
) ยท (-1โ๐
)) = ((-1โ๐
) ยท (1 / (-1โ๐
)))) |
219 | 201 | zcnd 12672 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-1โ๐
) โ
โ) |
220 | 214, 215,
35 | expne0d 14122 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (-1โ๐
) โ 0) |
221 | 219, 220 | recidd 11990 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-1โ๐
) ยท (1 / (-1โ๐
))) = 1) |
222 | 218, 221 | eqtrd 2771 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-1โ๐
) ยท (-1โ๐
)) = 1) |
223 | 222 | oveq1d 7427 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท (-1โ๐
)) ยท ๐
) = (1 ยท ๐
)) |
224 | 219, 219,
36 | mulassd 11242 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท (-1โ๐
)) ยท ๐
) = ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
))) |
225 | 36 | mullidd 11237 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (1 ยท ๐
) = ๐
) |
226 | 223, 224,
225 | 3eqtr3d 2779 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
)) = ๐
) |
227 | 226 | breq2d 5161 |
. . . . . . . . . . 11
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
)) โ ๐ โฅ ๐
)) |
228 | 206, 227 | mtbird 324 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
))) |
229 | | dvdsmultr2 16246 |
. . . . . . . . . . 11
โข ((๐ โ โค โง
(-1โ๐
) โ โค
โง ((-1โ๐
) ยท
๐
) โ โค) โ
(๐ โฅ ((-1โ๐
) ยท ๐
) โ ๐ โฅ ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
)))) |
230 | 102, 201,
202, 229 | syl3anc 1370 |
. . . . . . . . . 10
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ ((-1โ๐
) ยท ๐
) โ ๐ โฅ ((-1โ๐
) ยท ((-1โ๐
) ยท ๐
)))) |
231 | 228, 230 | mtod 197 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ ๐ โฅ ((-1โ๐
) ยท ๐
)) |
232 | | dvdsval3 16206 |
. . . . . . . . . 10
โข ((๐ โ โ โง
((-1โ๐
) ยท ๐
) โ โค) โ (๐ โฅ ((-1โ๐
) ยท ๐
) โ (((-1โ๐
) ยท ๐
) mod ๐) = 0)) |
233 | 29, 202, 232 | syl2anc 583 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (๐ โฅ ((-1โ๐
) ยท ๐
) โ (((-1โ๐
) ยท ๐
) mod ๐) = 0)) |
234 | 231, 233 | mtbid 323 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ยฌ
(((-1โ๐
) ยท
๐
) mod ๐) = 0) |
235 | | elnn0 12479 |
. . . . . . . . . 10
โข
((((-1โ๐
)
ยท ๐
) mod ๐) โ โ0
โ ((((-1โ๐
)
ยท ๐
) mod ๐) โ โ โจ
(((-1โ๐
) ยท
๐
) mod ๐) = 0)) |
236 | 203, 235 | sylib 217 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) โ โ โจ (((-1โ๐
) ยท ๐
) mod ๐) = 0)) |
237 | 236 | ord 861 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (ยฌ
(((-1โ๐
) ยท
๐
) mod ๐) โ โ โ (((-1โ๐
) ยท ๐
) mod ๐) = 0)) |
238 | 234, 237 | mt3d 148 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท ๐
) mod ๐) โ โ) |
239 | 238 | nngt0d 12266 |
. . . . . 6
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 0 <
(((-1โ๐
) ยท
๐
) mod ๐)) |
240 | 204, 95, 239, 97 | divgt0d 12154 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 0 <
((((-1โ๐
) ยท
๐
) mod ๐) / 2)) |
241 | | elnnz 12573 |
. . . . 5
โข
(((((-1โ๐
)
ยท ๐
) mod ๐) / 2) โ โ โ
(((((-1โ๐
) ยท
๐
) mod ๐) / 2) โ โค โง 0 <
((((-1โ๐
) ยท
๐
) mod ๐) / 2))) |
242 | 199, 240,
241 | sylanbrc 582 |
. . . 4
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โ โ) |
243 | 242 | nnge1d 12265 |
. . 3
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ 1 โค
((((-1โ๐
) ยท
๐
) mod ๐) / 2)) |
244 | | zmodfz 13863 |
. . . . . 6
โข
((((-1โ๐
)
ยท ๐
) โ โค
โง ๐ โ โ)
โ (((-1โ๐
)
ยท ๐
) mod ๐) โ (0...(๐ โ 1))) |
245 | 202, 29, 244 | syl2anc 583 |
. . . . 5
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท ๐
) mod ๐) โ (0...(๐ โ 1))) |
246 | | elfzle2 13510 |
. . . . 5
โข
((((-1โ๐
)
ยท ๐
) mod ๐) โ (0...(๐ โ 1)) โ (((-1โ๐
) ยท ๐
) mod ๐) โค (๐ โ 1)) |
247 | 245, 246 | syl 17 |
. . . 4
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ (((-1โ๐
) ยท ๐
) mod ๐) โค (๐ โ 1)) |
248 | | lediv1 12084 |
. . . . 5
โข
(((((-1โ๐
)
ยท ๐
) mod ๐) โ โ โง (๐ โ 1) โ โ โง
(2 โ โ โง 0 < 2)) โ ((((-1โ๐
) ยท ๐
) mod ๐) โค (๐ โ 1) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โค ((๐ โ 1) / 2))) |
249 | 204, 93, 95, 97, 248 | syl112anc 1373 |
. . . 4
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) โค (๐ โ 1) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โค ((๐ โ 1) / 2))) |
250 | 247, 249 | mpbid 231 |
. . 3
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โค ((๐ โ 1) / 2)) |
251 | 1, 6, 199, 243, 250 | elfzd 13497 |
. 2
โข ((๐ โง ๐ฅ โ (1...((๐ โ 1) / 2))) โ ((((-1โ๐
) ยท ๐
) mod ๐) / 2) โ (1...((๐ โ 1) / 2))) |
252 | | lgseisen.5 |
. 2
โข ๐ = (๐ฅ โ (1...((๐ โ 1) / 2)) โฆ ((((-1โ๐
) ยท ๐
) mod ๐) / 2)) |
253 | 251, 252 | fmptd 7116 |
1
โข (๐ โ ๐:(1...((๐ โ 1) / 2))โถ(1...((๐ โ 1) /
2))) |