Step | Hyp | Ref
| Expression |
1 | | 2sqb.1 |
. . . . . 6
โข (๐ โ (๐ โ โ โง ๐ โ 2)) |
2 | 1 | simpld 495 |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | | nprmdvds1 16642 |
. . . . 5
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
4 | 2, 3 | syl 17 |
. . . 4
โข (๐ โ ยฌ ๐ โฅ 1) |
5 | | prmz 16611 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
6 | 2, 5 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โค) |
7 | | 1z 12591 |
. . . . 5
โข 1 โ
โค |
8 | | dvdsnegb 16216 |
. . . . 5
โข ((๐ โ โค โง 1 โ
โค) โ (๐ โฅ
1 โ ๐ โฅ
-1)) |
9 | 6, 7, 8 | sylancl 586 |
. . . 4
โข (๐ โ (๐ โฅ 1 โ ๐ โฅ -1)) |
10 | 4, 9 | mtbid 323 |
. . 3
โข (๐ โ ยฌ ๐ โฅ -1) |
11 | | 2sqb.2 |
. . . . . 6
โข (๐ โ (๐ โ โค โง ๐ โ โค)) |
12 | 11 | simpld 495 |
. . . . 5
โข (๐ โ ๐ โ โค) |
13 | | 2sqb.5 |
. . . . 5
โข (๐ โ ๐ต โ โค) |
14 | 12, 13 | zmulcld 12671 |
. . . 4
โข (๐ โ (๐ ยท ๐ต) โ โค) |
15 | | zsqcl 14093 |
. . . . . . . . 9
โข (๐ต โ โค โ (๐ตโ2) โ
โค) |
16 | 13, 15 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ตโ2) โ โค) |
17 | | dvdsmul1 16220 |
. . . . . . . 8
โข ((๐ โ โค โง (๐ตโ2) โ โค) โ
๐ โฅ (๐ ยท (๐ตโ2))) |
18 | 6, 16, 17 | syl2anc 584 |
. . . . . . 7
โข (๐ โ ๐ โฅ (๐ ยท (๐ตโ2))) |
19 | 11 | simprd 496 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โค) |
20 | 19, 13 | zmulcld 12671 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท ๐ต) โ โค) |
21 | | zsqcl 14093 |
. . . . . . . . . . . 12
โข ((๐ ยท ๐ต) โ โค โ ((๐ ยท ๐ต)โ2) โ โค) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((๐ ยท ๐ต)โ2) โ โค) |
23 | | peano2zm 12604 |
. . . . . . . . . . 11
โข (((๐ ยท ๐ต)โ2) โ โค โ (((๐ ยท ๐ต)โ2) โ 1) โ
โค) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (((๐ ยท ๐ต)โ2) โ 1) โ
โค) |
25 | 24 | zcnd 12666 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท ๐ต)โ2) โ 1) โ
โ) |
26 | | zsqcl 14093 |
. . . . . . . . . . . 12
โข ((๐ ยท ๐ต) โ โค โ ((๐ ยท ๐ต)โ2) โ โค) |
27 | 14, 26 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ((๐ ยท ๐ต)โ2) โ โค) |
28 | 27 | peano2zd 12668 |
. . . . . . . . . 10
โข (๐ โ (((๐ ยท ๐ต)โ2) + 1) โ
โค) |
29 | 28 | zcnd 12666 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท ๐ต)โ2) + 1) โ
โ) |
30 | 25, 29 | addcomd 11415 |
. . . . . . . 8
โข (๐ โ ((((๐ ยท ๐ต)โ2) โ 1) + (((๐ ยท ๐ต)โ2) + 1)) = ((((๐ ยท ๐ต)โ2) + 1) + (((๐ ยท ๐ต)โ2) โ 1))) |
31 | 27 | zcnd 12666 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท ๐ต)โ2) โ โ) |
32 | | ax-1cn 11167 |
. . . . . . . . . 10
โข 1 โ
โ |
33 | 32 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
34 | 22 | zcnd 12666 |
. . . . . . . . 9
โข (๐ โ ((๐ ยท ๐ต)โ2) โ โ) |
35 | 31, 33, 34 | ppncand 11610 |
. . . . . . . 8
โข (๐ โ ((((๐ ยท ๐ต)โ2) + 1) + (((๐ ยท ๐ต)โ2) โ 1)) = (((๐ ยท ๐ต)โ2) + ((๐ ยท ๐ต)โ2))) |
36 | | zsqcl 14093 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐โ2) โ
โค) |
37 | 12, 36 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โ โค) |
38 | 37 | zcnd 12666 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) โ โ) |
39 | | zsqcl 14093 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐โ2) โ
โค) |
40 | 19, 39 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ (๐โ2) โ โค) |
41 | 40 | zcnd 12666 |
. . . . . . . . . 10
โข (๐ โ (๐โ2) โ โ) |
42 | 16 | zcnd 12666 |
. . . . . . . . . 10
โข (๐ โ (๐ตโ2) โ โ) |
43 | 38, 41, 42 | adddird 11238 |
. . . . . . . . 9
โข (๐ โ (((๐โ2) + (๐โ2)) ยท (๐ตโ2)) = (((๐โ2) ยท (๐ตโ2)) + ((๐โ2) ยท (๐ตโ2)))) |
44 | | 2sqb.3 |
. . . . . . . . . 10
โข (๐ โ ๐ = ((๐โ2) + (๐โ2))) |
45 | 44 | oveq1d 7423 |
. . . . . . . . 9
โข (๐ โ (๐ ยท (๐ตโ2)) = (((๐โ2) + (๐โ2)) ยท (๐ตโ2))) |
46 | 12 | zcnd 12666 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
47 | 13 | zcnd 12666 |
. . . . . . . . . . 11
โข (๐ โ ๐ต โ โ) |
48 | 46, 47 | sqmuld 14122 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ต)โ2) = ((๐โ2) ยท (๐ตโ2))) |
49 | 19 | zcnd 12666 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
50 | 49, 47 | sqmuld 14122 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ต)โ2) = ((๐โ2) ยท (๐ตโ2))) |
51 | 48, 50 | oveq12d 7426 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท ๐ต)โ2) + ((๐ ยท ๐ต)โ2)) = (((๐โ2) ยท (๐ตโ2)) + ((๐โ2) ยท (๐ตโ2)))) |
52 | 43, 45, 51 | 3eqtr4rd 2783 |
. . . . . . . 8
โข (๐ โ (((๐ ยท ๐ต)โ2) + ((๐ ยท ๐ต)โ2)) = (๐ ยท (๐ตโ2))) |
53 | 30, 35, 52 | 3eqtrd 2776 |
. . . . . . 7
โข (๐ โ ((((๐ ยท ๐ต)โ2) โ 1) + (((๐ ยท ๐ต)โ2) + 1)) = (๐ ยท (๐ตโ2))) |
54 | 18, 53 | breqtrrd 5176 |
. . . . . 6
โข (๐ โ ๐ โฅ ((((๐ ยท ๐ต)โ2) โ 1) + (((๐ ยท ๐ต)โ2) + 1))) |
55 | | 2sqb.4 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โค) |
56 | | dvdsmul1 16220 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ด โ โค) โ ๐ โฅ (๐ ยท ๐ด)) |
57 | 6, 55, 56 | syl2anc 584 |
. . . . . . . . . . 11
โข (๐ โ ๐ โฅ (๐ ยท ๐ด)) |
58 | 6, 55 | zmulcld 12671 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท ๐ด) โ โค) |
59 | | dvdsnegb 16216 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง (๐ ยท ๐ด) โ โค) โ (๐ โฅ (๐ ยท ๐ด) โ ๐ โฅ -(๐ ยท ๐ด))) |
60 | 6, 58, 59 | syl2anc 584 |
. . . . . . . . . . 11
โข (๐ โ (๐ โฅ (๐ ยท ๐ด) โ ๐ โฅ -(๐ ยท ๐ด))) |
61 | 57, 60 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ ๐ โฅ -(๐ ยท ๐ด)) |
62 | 20 | zcnd 12666 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท ๐ต) โ โ) |
63 | | negsubdi2 11518 |
. . . . . . . . . . . 12
โข ((1
โ โ โง (๐
ยท ๐ต) โ โ)
โ -(1 โ (๐
ยท ๐ต)) = ((๐ ยท ๐ต) โ 1)) |
64 | 32, 62, 63 | sylancr 587 |
. . . . . . . . . . 11
โข (๐ โ -(1 โ (๐ ยท ๐ต)) = ((๐ ยท ๐ต) โ 1)) |
65 | 58 | zcnd 12666 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท ๐ด) โ โ) |
66 | 19 | zred 12665 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ โ) |
67 | | absresq 15248 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ
((absโ๐)โ2) =
(๐โ2)) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((absโ๐)โ2) = (๐โ2)) |
69 | 66 | resqcld 14089 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐โ2) โ โ) |
70 | | prmnn 16610 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
71 | 2, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ โ โ) |
72 | 71 | nnred 12226 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ โ) |
73 | 72 | resqcld 14089 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐โ2) โ โ) |
74 | | zsqcl2 14102 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โค โ (๐โ2) โ
โ0) |
75 | 12, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ (๐โ2) โ
โ0) |
76 | | nn0addge2 12518 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐โ2) โ โ โง
(๐โ2) โ
โ0) โ (๐โ2) โค ((๐โ2) + (๐โ2))) |
77 | 69, 75, 76 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐โ2) โค ((๐โ2) + (๐โ2))) |
78 | 77, 44 | breqtrrd 5176 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐โ2) โค ๐) |
79 | 6 | zcnd 12666 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐ โ โ) |
80 | 79 | exp1d 14105 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐โ1) = ๐) |
81 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 โ
โค) |
82 | | 2z 12593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 2 โ
โค |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 2 โ
โค) |
84 | | prmuz2 16632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
85 | 2, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ ๐ โ
(โคโฅโ2)) |
86 | | eluz2gt1 12903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ
(โคโฅโ2) โ 1 < ๐) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 < ๐) |
88 | | 1lt2 12382 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 1 <
2 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 < 2) |
90 | | ltexp2a 14130 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ โ โ โง 1 โ
โค โง 2 โ โค) โง (1 < ๐ โง 1 < 2)) โ (๐โ1) < (๐โ2)) |
91 | 72, 81, 83, 87, 89, 90 | syl32anc 1378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐โ1) < (๐โ2)) |
92 | 80, 91 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ < (๐โ2)) |
93 | 69, 72, 73, 78, 92 | lelttrd 11371 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐โ2) < (๐โ2)) |
94 | 68, 93 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((absโ๐)โ2) < (๐โ2)) |
95 | 49 | abscld 15382 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (absโ๐) โ
โ) |
96 | 49 | absge0d 15390 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 0 โค (absโ๐)) |
97 | 71 | nnnn0d 12531 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ
โ0) |
98 | 97 | nn0ge0d 12534 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 0 โค ๐) |
99 | 95, 72, 96, 98 | lt2sqd 14218 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((absโ๐) < ๐ โ ((absโ๐)โ2) < (๐โ2))) |
100 | 94, 99 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (absโ๐) < ๐) |
101 | 6 | zred 12665 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ โ โ) |
102 | 95, 101 | ltnled 11360 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ((absโ๐) < ๐ โ ยฌ ๐ โค (absโ๐))) |
103 | 100, 102 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ยฌ ๐ โค (absโ๐)) |
104 | | sqnprm 16638 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ ยฌ
(๐โ2) โ
โ) |
105 | 12, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ยฌ (๐โ2) โ โ) |
106 | 49 | abs00ad 15236 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ((absโ๐) = 0 โ ๐ = 0)) |
107 | 44, 2 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((๐โ2) + (๐โ2)) โ โ) |
108 | | sq0i 14156 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ = 0 โ (๐โ2) = 0) |
109 | 108 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ = 0 โ ((๐โ2) + (๐โ2)) = ((๐โ2) + 0)) |
110 | 109 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = 0 โ (((๐โ2) + (๐โ2)) โ โ โ ((๐โ2) + 0) โ
โ)) |
111 | 107, 110 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (๐ = 0 โ ((๐โ2) + 0) โ
โ)) |
112 | 38 | addridd 11413 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ((๐โ2) + 0) = (๐โ2)) |
113 | 112 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ (((๐โ2) + 0) โ โ โ (๐โ2) โ
โ)) |
114 | 111, 113 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (๐ = 0 โ (๐โ2) โ โ)) |
115 | 106, 114 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((absโ๐) = 0 โ (๐โ2) โ โ)) |
116 | 105, 115 | mtod 197 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ยฌ (absโ๐) = 0) |
117 | | nn0abscl 15258 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โค โ
(absโ๐) โ
โ0) |
118 | 19, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (absโ๐) โ
โ0) |
119 | | elnn0 12473 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((absโ๐)
โ โ0 โ ((absโ๐) โ โ โจ (absโ๐) = 0)) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ((absโ๐) โ โ โจ
(absโ๐) =
0)) |
121 | 120 | ord 862 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (ยฌ (absโ๐) โ โ โ
(absโ๐) =
0)) |
122 | 116, 121 | mt3d 148 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (absโ๐) โ
โ) |
123 | | dvdsle 16252 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง
(absโ๐) โ
โ) โ (๐ โฅ
(absโ๐) โ ๐ โค (absโ๐))) |
124 | 6, 122, 123 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ โฅ (absโ๐) โ ๐ โค (absโ๐))) |
125 | 103, 124 | mtod 197 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ยฌ ๐ โฅ (absโ๐)) |
126 | | dvdsabsb 16218 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (absโ๐))) |
127 | 6, 19, 126 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ โฅ ๐ โ ๐ โฅ (absโ๐))) |
128 | 125, 127 | mtbird 324 |
. . . . . . . . . . . . . . 15
โข (๐ โ ยฌ ๐ โฅ ๐) |
129 | | coprm 16647 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ โค) โ (ยฌ
๐ โฅ ๐ โ (๐ gcd ๐) = 1)) |
130 | 2, 19, 129 | syl2anc 584 |
. . . . . . . . . . . . . . 15
โข (๐ โ (ยฌ ๐ โฅ ๐ โ (๐ gcd ๐) = 1)) |
131 | 128, 130 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ gcd ๐) = 1) |
132 | | 2sqb.6 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ gcd ๐) = ((๐ ยท ๐ด) + (๐ ยท ๐ต))) |
133 | 131, 132 | eqtr3d 2774 |
. . . . . . . . . . . . 13
โข (๐ โ 1 = ((๐ ยท ๐ด) + (๐ ยท ๐ต))) |
134 | 65, 62, 133 | mvrraddd 11625 |
. . . . . . . . . . . 12
โข (๐ โ (1 โ (๐ ยท ๐ต)) = (๐ ยท ๐ด)) |
135 | 134 | negeqd 11453 |
. . . . . . . . . . 11
โข (๐ โ -(1 โ (๐ ยท ๐ต)) = -(๐ ยท ๐ด)) |
136 | 64, 135 | eqtr3d 2774 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ต) โ 1) = -(๐ ยท ๐ด)) |
137 | 61, 136 | breqtrrd 5176 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ ((๐ ยท ๐ต) โ 1)) |
138 | 20 | peano2zd 12668 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ต) + 1) โ โค) |
139 | | peano2zm 12604 |
. . . . . . . . . . 11
โข ((๐ ยท ๐ต) โ โค โ ((๐ ยท ๐ต) โ 1) โ
โค) |
140 | 20, 139 | syl 17 |
. . . . . . . . . 10
โข (๐ โ ((๐ ยท ๐ต) โ 1) โ
โค) |
141 | | dvdsmultr2 16240 |
. . . . . . . . . 10
โข ((๐ โ โค โง ((๐ ยท ๐ต) + 1) โ โค โง ((๐ ยท ๐ต) โ 1) โ โค) โ (๐ โฅ ((๐ ยท ๐ต) โ 1) โ ๐ โฅ (((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1)))) |
142 | 6, 138, 140, 141 | syl3anc 1371 |
. . . . . . . . 9
โข (๐ โ (๐ โฅ ((๐ ยท ๐ต) โ 1) โ ๐ โฅ (((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1)))) |
143 | 137, 142 | mpd 15 |
. . . . . . . 8
โข (๐ โ ๐ โฅ (((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1))) |
144 | | sq1 14158 |
. . . . . . . . . 10
โข
(1โ2) = 1 |
145 | 144 | oveq2i 7419 |
. . . . . . . . 9
โข (((๐ ยท ๐ต)โ2) โ (1โ2)) = (((๐ ยท ๐ต)โ2) โ 1) |
146 | | subsq 14173 |
. . . . . . . . . 10
โข (((๐ ยท ๐ต) โ โ โง 1 โ โ)
โ (((๐ ยท ๐ต)โ2) โ (1โ2)) =
(((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1))) |
147 | 62, 32, 146 | sylancl 586 |
. . . . . . . . 9
โข (๐ โ (((๐ ยท ๐ต)โ2) โ (1โ2)) = (((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1))) |
148 | 145, 147 | eqtr3id 2786 |
. . . . . . . 8
โข (๐ โ (((๐ ยท ๐ต)โ2) โ 1) = (((๐ ยท ๐ต) + 1) ยท ((๐ ยท ๐ต) โ 1))) |
149 | 143, 148 | breqtrrd 5176 |
. . . . . . 7
โข (๐ โ ๐ โฅ (((๐ ยท ๐ต)โ2) โ 1)) |
150 | | dvdsadd2b 16248 |
. . . . . . 7
โข ((๐ โ โค โง (((๐ ยท ๐ต)โ2) + 1) โ โค โง
((((๐ ยท ๐ต)โ2) โ 1) โ
โค โง ๐ โฅ
(((๐ ยท ๐ต)โ2) โ 1))) โ
(๐ โฅ (((๐ ยท ๐ต)โ2) + 1) โ ๐ โฅ ((((๐ ยท ๐ต)โ2) โ 1) + (((๐ ยท ๐ต)โ2) + 1)))) |
151 | 6, 28, 24, 149, 150 | syl112anc 1374 |
. . . . . 6
โข (๐ โ (๐ โฅ (((๐ ยท ๐ต)โ2) + 1) โ ๐ โฅ ((((๐ ยท ๐ต)โ2) โ 1) + (((๐ ยท ๐ต)โ2) + 1)))) |
152 | 54, 151 | mpbird 256 |
. . . . 5
โข (๐ โ ๐ โฅ (((๐ ยท ๐ต)โ2) + 1)) |
153 | | subneg 11508 |
. . . . . 6
โข ((((๐ ยท ๐ต)โ2) โ โ โง 1 โ
โ) โ (((๐
ยท ๐ต)โ2) โ
-1) = (((๐ ยท ๐ต)โ2) + 1)) |
154 | 31, 32, 153 | sylancl 586 |
. . . . 5
โข (๐ โ (((๐ ยท ๐ต)โ2) โ -1) = (((๐ ยท ๐ต)โ2) + 1)) |
155 | 152, 154 | breqtrrd 5176 |
. . . 4
โข (๐ โ ๐ โฅ (((๐ ยท ๐ต)โ2) โ -1)) |
156 | | oveq1 7415 |
. . . . . . 7
โข (๐ฅ = (๐ ยท ๐ต) โ (๐ฅโ2) = ((๐ ยท ๐ต)โ2)) |
157 | 156 | oveq1d 7423 |
. . . . . 6
โข (๐ฅ = (๐ ยท ๐ต) โ ((๐ฅโ2) โ -1) = (((๐ ยท ๐ต)โ2) โ -1)) |
158 | 157 | breq2d 5160 |
. . . . 5
โข (๐ฅ = (๐ ยท ๐ต) โ (๐ โฅ ((๐ฅโ2) โ -1) โ ๐ โฅ (((๐ ยท ๐ต)โ2) โ -1))) |
159 | 158 | rspcev 3612 |
. . . 4
โข (((๐ ยท ๐ต) โ โค โง ๐ โฅ (((๐ ยท ๐ต)โ2) โ -1)) โ โ๐ฅ โ โค ๐ โฅ ((๐ฅโ2) โ -1)) |
160 | 14, 155, 159 | syl2anc 584 |
. . 3
โข (๐ โ โ๐ฅ โ โค ๐ โฅ ((๐ฅโ2) โ -1)) |
161 | | neg1z 12597 |
. . . 4
โข -1 โ
โค |
162 | | eldifsn 4790 |
. . . . 5
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
163 | 1, 162 | sylibr 233 |
. . . 4
โข (๐ โ ๐ โ (โ โ
{2})) |
164 | | lgsqr 26851 |
. . . 4
โข ((-1
โ โค โง ๐
โ (โ โ {2})) โ ((-1 /L ๐) = 1 โ (ยฌ ๐ โฅ -1 โง โ๐ฅ โ โค ๐ โฅ ((๐ฅโ2) โ -1)))) |
165 | 161, 163,
164 | sylancr 587 |
. . 3
โข (๐ โ ((-1 /L
๐) = 1 โ (ยฌ ๐ โฅ -1 โง โ๐ฅ โ โค ๐ โฅ ((๐ฅโ2) โ -1)))) |
166 | 10, 160, 165 | mpbir2and 711 |
. 2
โข (๐ โ (-1 /L
๐) = 1) |
167 | | m1lgs 26888 |
. . 3
โข (๐ โ (โ โ {2})
โ ((-1 /L ๐) = 1 โ (๐ mod 4) = 1)) |
168 | 163, 167 | syl 17 |
. 2
โข (๐ โ ((-1 /L
๐) = 1 โ (๐ mod 4) = 1)) |
169 | 166, 168 | mpbid 231 |
1
โข (๐ โ (๐ mod 4) = 1) |