Step | Hyp | Ref
| Expression |
1 | | neg1z 12540 |
. . . . . . . . 9
โข -1 โ
โค |
2 | | oddprm 16683 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
3 | 2 | nnnn0d 12474 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ0) |
4 | | zexpcl 13983 |
. . . . . . . . 9
โข ((-1
โ โค โง ((๐
โ 1) / 2) โ โ0) โ (-1โ((๐ โ 1) / 2)) โ
โค) |
5 | 1, 3, 4 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ (-1โ((๐ โ
1) / 2)) โ โค) |
6 | 5 | peano2zd 12611 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ((-1โ((๐
โ 1) / 2)) + 1) โ โค) |
7 | | eldifi 4087 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
8 | | prmnn 16551 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
10 | 6, 9 | zmodcld 13798 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ
โ0) |
11 | 10 | nn0cnd 12476 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ โ) |
12 | | 1cnd 11151 |
. . . . 5
โข (๐ โ (โ โ {2})
โ 1 โ โ) |
13 | 11, 12, 12 | subaddd 11531 |
. . . 4
โข (๐ โ (โ โ {2})
โ (((((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ 1) = 1 โ (1 + 1) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐))) |
14 | | 2re 12228 |
. . . . . . . 8
โข 2 โ
โ |
15 | 14 | a1i 11 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 โ โ) |
16 | 9 | nnrpd 12956 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ+) |
17 | | 0le2 12256 |
. . . . . . . 8
โข 0 โค
2 |
18 | 17 | a1i 11 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 0 โค 2) |
19 | | oddprmgt2 16576 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 < ๐) |
20 | | modid 13802 |
. . . . . . 7
โข (((2
โ โ โง ๐
โ โ+) โง (0 โค 2 โง 2 < ๐)) โ (2 mod ๐) = 2) |
21 | 15, 16, 18, 19, 20 | syl22anc 838 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (2 mod ๐) =
2) |
22 | | df-2 12217 |
. . . . . 6
โข 2 = (1 +
1) |
23 | 21, 22 | eqtrdi 2793 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (2 mod ๐) = (1 +
1)) |
24 | 23 | eqeq1d 2739 |
. . . 4
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ (1 +
1) = (((-1โ((๐ โ
1) / 2)) + 1) mod ๐))) |
25 | | eldifsni 4751 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
2) |
26 | 25 | neneqd 2949 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ ยฌ ๐ =
2) |
27 | | prmuz2 16573 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
28 | 7, 27 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
(โคโฅโ2)) |
29 | | 2prm 16569 |
. . . . . . . . . . . 12
โข 2 โ
โ |
30 | | dvdsprm 16580 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง 2 โ โ) โ (๐ โฅ 2 โ ๐ = 2)) |
31 | 28, 29, 30 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ (๐ โฅ 2 โ
๐ = 2)) |
32 | 26, 31 | mtbird 325 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ยฌ ๐ โฅ
2) |
33 | 32 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ ๐ โฅ 2) |
34 | | 1cnd 11151 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ 1 โ โ) |
35 | 2 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((๐
โ 1) / 2) โ โ) |
36 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ 2 โฅ ((๐ โ 1) / 2)) |
37 | | oexpneg 16228 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ((๐
โ 1) / 2) โ โ โง ยฌ 2 โฅ ((๐ โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) =
-(1โ((๐ โ 1) /
2))) |
38 | 34, 35, 36, 37 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) = -(1โ((๐ โ 1) /
2))) |
39 | 35 | nnzd 12527 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((๐
โ 1) / 2) โ โค) |
40 | | 1exp 13998 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ 1) / 2) โ โค
โ (1โ((๐ โ
1) / 2)) = 1) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (1โ((๐ โ 1) / 2)) = 1) |
42 | 41 | negeqd 11396 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ -(1โ((๐ โ 1) / 2)) = -1) |
43 | 38, 42 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) = -1) |
44 | 43 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((-1โ((๐ โ 1) / 2)) + 1) = (-1 +
1)) |
45 | | ax-1cn 11110 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
46 | | neg1cn 12268 |
. . . . . . . . . . . . . 14
โข -1 โ
โ |
47 | | 1pneg1e0 12273 |
. . . . . . . . . . . . . 14
โข (1 + -1)
= 0 |
48 | 45, 46, 47 | addcomli 11348 |
. . . . . . . . . . . . 13
โข (-1 + 1)
= 0 |
49 | 44, 48 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((-1โ((๐ โ 1) / 2)) + 1) = 0) |
50 | 49 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) = (2 โ
0)) |
51 | | 2cn 12229 |
. . . . . . . . . . . 12
โข 2 โ
โ |
52 | 51 | subid1i 11474 |
. . . . . . . . . . 11
โข (2
โ 0) = 2 |
53 | 50, 52 | eqtrdi 2793 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) =
2) |
54 | 53 | breq2d 5118 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (๐
โฅ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) โ ๐ โฅ 2)) |
55 | 33, 54 | mtbird 325 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1))) |
56 | 55 | ex 414 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (ยฌ 2 โฅ ((๐
โ 1) / 2) โ ยฌ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1)))) |
57 | 56 | con4d 115 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (๐ โฅ (2
โ ((-1โ((๐
โ 1) / 2)) + 1)) โ 2 โฅ ((๐ โ 1) / 2))) |
58 | | 2z 12536 |
. . . . . . . 8
โข 2 โ
โค |
59 | 58 | a1i 11 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 โ โค) |
60 | | moddvds 16148 |
. . . . . . 7
โข ((๐ โ โ โง 2 โ
โค โง ((-1โ((๐
โ 1) / 2)) + 1) โ โค) โ ((2 mod ๐) = (((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1)))) |
61 | 9, 59, 6, 60 | syl3anc 1372 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ
๐ โฅ (2 โ
((-1โ((๐ โ 1) /
2)) + 1)))) |
62 | | 4z 12538 |
. . . . . . . . 9
โข 4 โ
โค |
63 | | 4ne0 12262 |
. . . . . . . . 9
โข 4 โ
0 |
64 | | nnm1nn0 12455 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
65 | 9, 64 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โ0) |
66 | 65 | nn0zd 12526 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โค) |
67 | | dvdsval2 16140 |
. . . . . . . . 9
โข ((4
โ โค โง 4 โ 0 โง (๐ โ 1) โ โค) โ (4
โฅ (๐ โ 1)
โ ((๐ โ 1) / 4)
โ โค)) |
68 | 62, 63, 66, 67 | mp3an12i 1466 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ ((๐
โ 1) / 4) โ โค)) |
69 | 65 | nn0cnd 12476 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โ) |
70 | 51 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ 2 โ โ) |
71 | | 2ne0 12258 |
. . . . . . . . . . . 12
โข 2 โ
0 |
72 | 71 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ 2 โ 0) |
73 | 69, 70, 70, 72, 72 | divdiv1d 11963 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ (((๐ โ 1) / 2)
/ 2) = ((๐ โ 1) / (2
ยท 2))) |
74 | | 2t2e4 12318 |
. . . . . . . . . . 11
โข (2
ยท 2) = 4 |
75 | 74 | oveq2i 7369 |
. . . . . . . . . 10
โข ((๐ โ 1) / (2 ยท 2)) =
((๐ โ 1) /
4) |
76 | 73, 75 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (((๐ โ 1) / 2)
/ 2) = ((๐ โ 1) /
4)) |
77 | 76 | eleq1d 2823 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ((((๐ โ 1) /
2) / 2) โ โค โ ((๐ โ 1) / 4) โ
โค)) |
78 | 68, 77 | bitr4d 282 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ (((๐
โ 1) / 2) / 2) โ โค)) |
79 | 2 | nnzd 12527 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โค) |
80 | | dvdsval2 16140 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง ((๐ โ 1) / 2) โ โค) โ (2
โฅ ((๐ โ 1) / 2)
โ (((๐ โ 1) / 2)
/ 2) โ โค)) |
81 | 58, 71, 79, 80 | mp3an12i 1466 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (2 โฅ ((๐
โ 1) / 2) โ (((๐
โ 1) / 2) / 2) โ โค)) |
82 | 78, 81 | bitr4d 282 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ 2 โฅ ((๐ โ 1) / 2))) |
83 | 57, 61, 82 | 3imtr4d 294 |
. . . . 5
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ 4
โฅ (๐ โ
1))) |
84 | 46 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ -1 โ โ) |
85 | | neg1ne0 12270 |
. . . . . . . . . . . 12
โข -1 โ
0 |
86 | 85 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ -1 โ 0) |
87 | 58 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ 2 โ โค) |
88 | 78 | biimpa 478 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (((๐ โ 1)
/ 2) / 2) โ โค) |
89 | | expmulz 14015 |
. . . . . . . . . . 11
โข (((-1
โ โ โง -1 โ 0) โง (2 โ โค โง (((๐ โ 1) / 2) / 2) โ
โค)) โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) =
((-1โ2)โ(((๐
โ 1) / 2) / 2))) |
90 | 84, 86, 87, 88, 89 | syl22anc 838 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) =
((-1โ2)โ(((๐
โ 1) / 2) / 2))) |
91 | 2 | nncnd 12170 |
. . . . . . . . . . . . 13
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
92 | 91, 70, 72 | divcan2d 11934 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ (2 ยท (((๐
โ 1) / 2) / 2)) = ((๐
โ 1) / 2)) |
93 | 92 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (2 ยท (((๐
โ 1) / 2) / 2)) = ((๐
โ 1) / 2)) |
94 | 93 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) = (-1โ((๐ โ 1) /
2))) |
95 | | neg1sqe1 14101 |
. . . . . . . . . . . 12
โข
(-1โ2) = 1 |
96 | 95 | oveq1i 7368 |
. . . . . . . . . . 11
โข
((-1โ2)โ(((๐ โ 1) / 2) / 2)) = (1โ(((๐ โ 1) / 2) /
2)) |
97 | | 1exp 13998 |
. . . . . . . . . . . 12
โข ((((๐ โ 1) / 2) / 2) โ
โค โ (1โ(((๐
โ 1) / 2) / 2)) = 1) |
98 | 88, 97 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (1โ(((๐
โ 1) / 2) / 2)) = 1) |
99 | 96, 98 | eqtrid 2789 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ ((-1โ2)โ(((๐ โ 1) / 2) / 2)) = 1) |
100 | 90, 94, 99 | 3eqtr3d 2785 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ((๐
โ 1) / 2)) = 1) |
101 | 100 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ ((-1โ((๐
โ 1) / 2)) + 1) = (1 + 1)) |
102 | 22, 101 | eqtr4id 2796 |
. . . . . . 7
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ 2 = ((-1โ((๐ โ 1) / 2)) + 1)) |
103 | 102 | oveq1d 7373 |
. . . . . 6
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐)) |
104 | 103 | ex 414 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ (2 mod ๐)
= (((-1โ((๐ โ 1)
/ 2)) + 1) mod ๐))) |
105 | 83, 104 | impbid 211 |
. . . 4
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ 4
โฅ (๐ โ
1))) |
106 | 13, 24, 105 | 3bitr2d 307 |
. . 3
โข (๐ โ (โ โ {2})
โ (((((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ 1) = 1 โ 4 โฅ (๐ โ 1))) |
107 | | lgsval3 26666 |
. . . . 5
โข ((-1
โ โค โง ๐
โ (โ โ {2})) โ (-1 /L ๐) = ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
108 | 1, 107 | mpan 689 |
. . . 4
โข (๐ โ (โ โ {2})
โ (-1 /L ๐) = ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
109 | 108 | eqeq1d 2739 |
. . 3
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) = 1)) |
110 | | 4nn 12237 |
. . . . 5
โข 4 โ
โ |
111 | 110 | a1i 11 |
. . . 4
โข (๐ โ (โ โ {2})
โ 4 โ โ) |
112 | | prmz 16552 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โค) |
113 | 7, 112 | syl 17 |
. . . 4
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
114 | | 1zzd 12535 |
. . . 4
โข (๐ โ (โ โ {2})
โ 1 โ โค) |
115 | | moddvds 16148 |
. . . 4
โข ((4
โ โ โง ๐
โ โค โง 1 โ โค) โ ((๐ mod 4) = (1 mod 4) โ 4 โฅ (๐ โ 1))) |
116 | 111, 113,
114, 115 | syl3anc 1372 |
. . 3
โข (๐ โ (โ โ {2})
โ ((๐ mod 4) = (1 mod
4) โ 4 โฅ (๐
โ 1))) |
117 | 106, 109,
116 | 3bitr4d 311 |
. 2
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ (๐ mod 4) = (1 mod 4))) |
118 | | 1re 11156 |
. . . 4
โข 1 โ
โ |
119 | | nnrp 12927 |
. . . . 5
โข (4 โ
โ โ 4 โ โ+) |
120 | 110, 119 | ax-mp 5 |
. . . 4
โข 4 โ
โ+ |
121 | | 0le1 11679 |
. . . 4
โข 0 โค
1 |
122 | | 1lt4 12330 |
. . . 4
โข 1 <
4 |
123 | | modid 13802 |
. . . 4
โข (((1
โ โ โง 4 โ โ+) โง (0 โค 1 โง 1 <
4)) โ (1 mod 4) = 1) |
124 | 118, 120,
121, 122, 123 | mp4an 692 |
. . 3
โข (1 mod 4)
= 1 |
125 | 124 | eqeq2i 2750 |
. 2
โข ((๐ mod 4) = (1 mod 4) โ
(๐ mod 4) =
1) |
126 | 117, 125 | bitrdi 287 |
1
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ (๐ mod 4) = 1)) |