Step | Hyp | Ref
| Expression |
1 | | neg1z 9284 |
. . . . . . . . 9
โข -1 โ
โค |
2 | | oddprm 12258 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
3 | 2 | nnnn0d 9228 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ0) |
4 | | zexpcl 10534 |
. . . . . . . . 9
โข ((-1
โ โค โง ((๐
โ 1) / 2) โ โ0) โ (-1โ((๐ โ 1) / 2)) โ
โค) |
5 | 1, 3, 4 | sylancr 414 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ (-1โ((๐ โ
1) / 2)) โ โค) |
6 | 5 | peano2zd 9377 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ((-1โ((๐
โ 1) / 2)) + 1) โ โค) |
7 | | eldifi 3257 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
8 | | prmnn 12109 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โ) |
9 | 7, 8 | syl 14 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
10 | 6, 9 | zmodcld 10344 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ
โ0) |
11 | 10 | nn0cnd 9230 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ โ) |
12 | | 1cnd 7972 |
. . . . 5
โข (๐ โ (โ โ {2})
โ 1 โ โ) |
13 | 11, 12, 12 | subaddd 8285 |
. . . 4
โข (๐ โ (โ โ {2})
โ (((((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ 1) = 1 โ (1 + 1) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐))) |
14 | | 2z 9280 |
. . . . . . . . 9
โข 2 โ
โค |
15 | | zq 9625 |
. . . . . . . . 9
โข (2 โ
โค โ 2 โ โ) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
โข 2 โ
โ |
17 | 16 | a1i 9 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 โ โ) |
18 | | prmz 12110 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
19 | | zq 9625 |
. . . . . . . 8
โข (๐ โ โค โ ๐ โ
โ) |
20 | 7, 18, 19 | 3syl 17 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
21 | | 0le2 9008 |
. . . . . . . 8
โข 0 โค
2 |
22 | 21 | a1i 9 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 0 โค 2) |
23 | | oddprmgt2 12133 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 < ๐) |
24 | | modqid 10348 |
. . . . . . 7
โข (((2
โ โ โง ๐
โ โ) โง (0 โค 2 โง 2 < ๐)) โ (2 mod ๐) = 2) |
25 | 17, 20, 22, 23, 24 | syl22anc 1239 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (2 mod ๐) =
2) |
26 | | df-2 8977 |
. . . . . 6
โข 2 = (1 +
1) |
27 | 25, 26 | eqtrdi 2226 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (2 mod ๐) = (1 +
1)) |
28 | 27 | eqeq1d 2186 |
. . . 4
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ (1 +
1) = (((-1โ((๐ โ
1) / 2)) + 1) mod ๐))) |
29 | | 2nn 9079 |
. . . . . . . 8
โข 2 โ
โ |
30 | 2 | nnzd 9373 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โค) |
31 | | dvdsdc 11804 |
. . . . . . . 8
โข ((2
โ โ โง ((๐
โ 1) / 2) โ โค) โ DECID 2 โฅ ((๐ โ 1) /
2)) |
32 | 29, 30, 31 | sylancr 414 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ DECID 2 โฅ ((๐ โ 1) / 2)) |
33 | | eldifsni 3721 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
2) |
34 | 33 | neneqd 2368 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ ยฌ ๐ =
2) |
35 | | prmuz2 12130 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
36 | 7, 35 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ ๐ โ
(โคโฅโ2)) |
37 | | 2prm 12126 |
. . . . . . . . . . . 12
โข 2 โ
โ |
38 | | dvdsprm 12136 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง 2 โ โ) โ (๐ โฅ 2 โ ๐ = 2)) |
39 | 36, 37, 38 | sylancl 413 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ (๐ โฅ 2 โ
๐ = 2)) |
40 | 34, 39 | mtbird 673 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ ยฌ ๐ โฅ
2) |
41 | 40 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ ๐ โฅ 2) |
42 | | 1cnd 7972 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ 1 โ โ) |
43 | 2 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((๐
โ 1) / 2) โ โ) |
44 | | simpr 110 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ 2 โฅ ((๐ โ 1) / 2)) |
45 | | oexpneg 11881 |
. . . . . . . . . . . . . . . 16
โข ((1
โ โ โง ((๐
โ 1) / 2) โ โ โง ยฌ 2 โฅ ((๐ โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) =
-(1โ((๐ โ 1) /
2))) |
46 | 42, 43, 44, 45 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) = -(1โ((๐ โ 1) /
2))) |
47 | 43 | nnzd 9373 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((๐
โ 1) / 2) โ โค) |
48 | | 1exp 10548 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ 1) / 2) โ โค
โ (1โ((๐ โ
1) / 2)) = 1) |
49 | 47, 48 | syl 14 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (1โ((๐ โ 1) / 2)) = 1) |
50 | 49 | negeqd 8151 |
. . . . . . . . . . . . . . 15
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ -(1โ((๐ โ 1) / 2)) = -1) |
51 | 46, 50 | eqtrd 2210 |
. . . . . . . . . . . . . 14
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (-1โ((๐ โ 1) / 2)) = -1) |
52 | 51 | oveq1d 5889 |
. . . . . . . . . . . . 13
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((-1โ((๐ โ 1) / 2)) + 1) = (-1 +
1)) |
53 | | ax-1cn 7903 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
54 | | neg1cn 9023 |
. . . . . . . . . . . . . 14
โข -1 โ
โ |
55 | | 1pneg1e0 9029 |
. . . . . . . . . . . . . 14
โข (1 + -1)
= 0 |
56 | 53, 54, 55 | addcomli 8101 |
. . . . . . . . . . . . 13
โข (-1 + 1)
= 0 |
57 | 52, 56 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ((-1โ((๐ โ 1) / 2)) + 1) = 0) |
58 | 57 | oveq2d 5890 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) = (2 โ
0)) |
59 | | 2cn 8989 |
. . . . . . . . . . . 12
โข 2 โ
โ |
60 | 59 | subid1i 8228 |
. . . . . . . . . . 11
โข (2
โ 0) = 2 |
61 | 58, 60 | eqtrdi 2226 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) =
2) |
62 | 61 | breq2d 4015 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ (๐
โฅ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) โ ๐ โฅ 2)) |
63 | 41, 62 | mtbird 673 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง ยฌ 2 โฅ ((๐
โ 1) / 2)) โ ยฌ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1))) |
64 | 63 | ex 115 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (ยฌ 2 โฅ ((๐
โ 1) / 2) โ ยฌ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1)))) |
65 | | condc 853 |
. . . . . . 7
โข
(DECID 2 โฅ ((๐ โ 1) / 2) โ ((ยฌ 2 โฅ
((๐ โ 1) / 2) โ
ยฌ ๐ โฅ (2 โ
((-1โ((๐ โ 1) /
2)) + 1))) โ (๐
โฅ (2 โ ((-1โ((๐ โ 1) / 2)) + 1)) โ 2 โฅ
((๐ โ 1) /
2)))) |
66 | 32, 64, 65 | sylc 62 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (๐ โฅ (2
โ ((-1โ((๐
โ 1) / 2)) + 1)) โ 2 โฅ ((๐ โ 1) / 2))) |
67 | 14 | a1i 9 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ 2 โ โค) |
68 | | moddvds 11805 |
. . . . . . 7
โข ((๐ โ โ โง 2 โ
โค โง ((-1โ((๐
โ 1) / 2)) + 1) โ โค) โ ((2 mod ๐) = (((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ ๐ โฅ (2 โ ((-1โ((๐ โ 1) / 2)) +
1)))) |
69 | 9, 67, 6, 68 | syl3anc 1238 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ
๐ โฅ (2 โ
((-1โ((๐ โ 1) /
2)) + 1)))) |
70 | | 4z 9282 |
. . . . . . . . 9
โข 4 โ
โค |
71 | | 4ne0 9016 |
. . . . . . . . 9
โข 4 โ
0 |
72 | | nnm1nn0 9216 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
73 | 9, 72 | syl 14 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โ0) |
74 | 73 | nn0zd 9372 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โค) |
75 | | dvdsval2 11796 |
. . . . . . . . 9
โข ((4
โ โค โง 4 โ 0 โง (๐ โ 1) โ โค) โ (4
โฅ (๐ โ 1)
โ ((๐ โ 1) / 4)
โ โค)) |
76 | 70, 71, 74, 75 | mp3an12i 1341 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ ((๐
โ 1) / 4) โ โค)) |
77 | 73 | nn0cnd 9230 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ (๐ โ 1) โ
โ) |
78 | 59 | a1i 9 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ 2 โ โ) |
79 | 29 | a1i 9 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ 2 โ โ) |
80 | 79 | nnap0d 8964 |
. . . . . . . . . . 11
โข (๐ โ (โ โ {2})
โ 2 # 0) |
81 | 77, 78, 78, 80, 80 | divdivap1d 8778 |
. . . . . . . . . 10
โข (๐ โ (โ โ {2})
โ (((๐ โ 1) / 2)
/ 2) = ((๐ โ 1) / (2
ยท 2))) |
82 | | 2t2e4 9072 |
. . . . . . . . . . 11
โข (2
ยท 2) = 4 |
83 | 82 | oveq2i 5885 |
. . . . . . . . . 10
โข ((๐ โ 1) / (2 ยท 2)) =
((๐ โ 1) /
4) |
84 | 81, 83 | eqtrdi 2226 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (((๐ โ 1) / 2)
/ 2) = ((๐ โ 1) /
4)) |
85 | 84 | eleq1d 2246 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ((((๐ โ 1) /
2) / 2) โ โค โ ((๐ โ 1) / 4) โ
โค)) |
86 | 76, 85 | bitr4d 191 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ (((๐
โ 1) / 2) / 2) โ โค)) |
87 | | 2ne0 9010 |
. . . . . . . 8
โข 2 โ
0 |
88 | | dvdsval2 11796 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง ((๐ โ 1) / 2) โ โค) โ (2
โฅ ((๐ โ 1) / 2)
โ (((๐ โ 1) / 2)
/ 2) โ โค)) |
89 | 14, 87, 30, 88 | mp3an12i 1341 |
. . . . . . 7
โข (๐ โ (โ โ {2})
โ (2 โฅ ((๐
โ 1) / 2) โ (((๐
โ 1) / 2) / 2) โ โค)) |
90 | 86, 89 | bitr4d 191 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ 2 โฅ ((๐ โ 1) / 2))) |
91 | 66, 69, 90 | 3imtr4d 203 |
. . . . 5
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ 4
โฅ (๐ โ
1))) |
92 | 54 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ -1 โ โ) |
93 | | neg1ap0 9027 |
. . . . . . . . . . . 12
โข -1 #
0 |
94 | 93 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ -1 # 0) |
95 | 14 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ 2 โ โค) |
96 | 86 | biimpa 296 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (((๐ โ 1)
/ 2) / 2) โ โค) |
97 | | expmulzap 10565 |
. . . . . . . . . . 11
โข (((-1
โ โ โง -1 # 0) โง (2 โ โค โง (((๐ โ 1) / 2) / 2) โ โค))
โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) =
((-1โ2)โ(((๐
โ 1) / 2) / 2))) |
98 | 92, 94, 95, 96, 97 | syl22anc 1239 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) =
((-1โ2)โ(((๐
โ 1) / 2) / 2))) |
99 | 2 | nncnd 8932 |
. . . . . . . . . . . . 13
โข (๐ โ (โ โ {2})
โ ((๐ โ 1) / 2)
โ โ) |
100 | 99, 78, 80 | divcanap2d 8748 |
. . . . . . . . . . . 12
โข (๐ โ (โ โ {2})
โ (2 ยท (((๐
โ 1) / 2) / 2)) = ((๐
โ 1) / 2)) |
101 | 100 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (2 ยท (((๐
โ 1) / 2) / 2)) = ((๐
โ 1) / 2)) |
102 | 101 | oveq2d 5890 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ(2 ยท (((๐ โ 1) / 2) / 2))) = (-1โ((๐ โ 1) /
2))) |
103 | | neg1sqe1 10614 |
. . . . . . . . . . . 12
โข
(-1โ2) = 1 |
104 | 103 | oveq1i 5884 |
. . . . . . . . . . 11
โข
((-1โ2)โ(((๐ โ 1) / 2) / 2)) = (1โ(((๐ โ 1) / 2) /
2)) |
105 | | 1exp 10548 |
. . . . . . . . . . . 12
โข ((((๐ โ 1) / 2) / 2) โ
โค โ (1โ(((๐
โ 1) / 2) / 2)) = 1) |
106 | 96, 105 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (1โ(((๐
โ 1) / 2) / 2)) = 1) |
107 | 104, 106 | eqtrid 2222 |
. . . . . . . . . 10
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ ((-1โ2)โ(((๐ โ 1) / 2) / 2)) = 1) |
108 | 98, 102, 107 | 3eqtr3d 2218 |
. . . . . . . . 9
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (-1โ((๐
โ 1) / 2)) = 1) |
109 | 108 | oveq1d 5889 |
. . . . . . . 8
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ ((-1โ((๐
โ 1) / 2)) + 1) = (1 + 1)) |
110 | 26, 109 | eqtr4id 2229 |
. . . . . . 7
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ 2 = ((-1โ((๐ โ 1) / 2)) + 1)) |
111 | 110 | oveq1d 5889 |
. . . . . 6
โข ((๐ โ (โ โ {2})
โง 4 โฅ (๐ โ
1)) โ (2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐)) |
112 | 111 | ex 115 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (4 โฅ (๐
โ 1) โ (2 mod ๐)
= (((-1โ((๐ โ 1)
/ 2)) + 1) mod ๐))) |
113 | 91, 112 | impbid 129 |
. . . 4
โข (๐ โ (โ โ {2})
โ ((2 mod ๐) =
(((-1โ((๐ โ 1) /
2)) + 1) mod ๐) โ 4
โฅ (๐ โ
1))) |
114 | 13, 28, 113 | 3bitr2d 216 |
. . 3
โข (๐ โ (โ โ {2})
โ (((((-1โ((๐
โ 1) / 2)) + 1) mod ๐) โ 1) = 1 โ 4 โฅ (๐ โ 1))) |
115 | | lgsval3 14389 |
. . . . 5
โข ((-1
โ โค โง ๐
โ (โ โ {2})) โ (-1 /L ๐) = ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
116 | 1, 115 | mpan 424 |
. . . 4
โข (๐ โ (โ โ {2})
โ (-1 /L ๐) = ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1)) |
117 | 116 | eqeq1d 2186 |
. . 3
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ ((((-1โ((๐ โ 1) / 2)) + 1) mod ๐) โ 1) = 1)) |
118 | | 4nn 9081 |
. . . . 5
โข 4 โ
โ |
119 | 118 | a1i 9 |
. . . 4
โข (๐ โ (โ โ {2})
โ 4 โ โ) |
120 | 7, 18 | syl 14 |
. . . 4
โข (๐ โ (โ โ {2})
โ ๐ โ
โค) |
121 | | 1zzd 9279 |
. . . 4
โข (๐ โ (โ โ {2})
โ 1 โ โค) |
122 | | moddvds 11805 |
. . . 4
โข ((4
โ โ โง ๐
โ โค โง 1 โ โค) โ ((๐ mod 4) = (1 mod 4) โ 4 โฅ (๐ โ 1))) |
123 | 119, 120,
121, 122 | syl3anc 1238 |
. . 3
โข (๐ โ (โ โ {2})
โ ((๐ mod 4) = (1 mod
4) โ 4 โฅ (๐
โ 1))) |
124 | 114, 117,
123 | 3bitr4d 220 |
. 2
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ (๐ mod 4) = (1 mod 4))) |
125 | | 1z 9278 |
. . . . 5
โข 1 โ
โค |
126 | | zq 9625 |
. . . . 5
โข (1 โ
โค โ 1 โ โ) |
127 | 125, 126 | ax-mp 5 |
. . . 4
โข 1 โ
โ |
128 | | zq 9625 |
. . . . 5
โข (4 โ
โค โ 4 โ โ) |
129 | 70, 128 | ax-mp 5 |
. . . 4
โข 4 โ
โ |
130 | | 0le1 8437 |
. . . 4
โข 0 โค
1 |
131 | | 1lt4 9092 |
. . . 4
โข 1 <
4 |
132 | | modqid 10348 |
. . . 4
โข (((1
โ โ โง 4 โ โ) โง (0 โค 1 โง 1 < 4)) โ
(1 mod 4) = 1) |
133 | 127, 129,
130, 131, 132 | mp4an 427 |
. . 3
โข (1 mod 4)
= 1 |
134 | 133 | eqeq2i 2188 |
. 2
โข ((๐ mod 4) = (1 mod 4) โ
(๐ mod 4) =
1) |
135 | 124, 134 | bitrdi 196 |
1
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ (๐ mod 4) = 1)) |