Step | Hyp | Ref
| Expression |
1 | | lgsquad2.1 |
. 2
โข (๐ โ ๐ โ โ) |
2 | | lgsquad2.2 |
. 2
โข (๐ โ ยฌ 2 โฅ ๐) |
3 | | lgsquad2.3 |
. 2
โข (๐ โ ๐ โ โ) |
4 | | lgsquad2.4 |
. 2
โข (๐ โ ยฌ 2 โฅ ๐) |
5 | | lgsquad2.5 |
. 2
โข (๐ โ (๐ gcd ๐) = 1) |
6 | 3 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โ) |
7 | 4 | adantr 482 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ยฌ 2 โฅ ๐) |
8 | | simprl 770 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ (โ โ
{2})) |
9 | | eldifi 4087 |
. . . . . 6
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
10 | 8, 9 | syl 17 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โ) |
11 | | prmnn 16551 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
12 | 10, 11 | syl 17 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โ) |
13 | | eldifsni 4751 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
2) |
14 | 8, 13 | syl 17 |
. . . . . . 7
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ 2) |
15 | 14 | necomd 3000 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ 2 โ ๐) |
16 | 15 | neneqd 2949 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ยฌ 2 = ๐) |
17 | | 2z 12536 |
. . . . . . 7
โข 2 โ
โค |
18 | | uzid 12779 |
. . . . . . 7
โข (2 โ
โค โ 2 โ (โคโฅโ2)) |
19 | 17, 18 | ax-mp 5 |
. . . . . 6
โข 2 โ
(โคโฅโ2) |
20 | | dvdsprm 16580 |
. . . . . 6
โข ((2
โ (โคโฅโ2) โง ๐ โ โ) โ (2 โฅ ๐ โ 2 = ๐)) |
21 | 19, 10, 20 | sylancr 588 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (2 โฅ ๐ โ 2 = ๐)) |
22 | 16, 21 | mtbird 325 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ยฌ 2 โฅ ๐) |
23 | 6 | nnzd 12527 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โค) |
24 | 12 | nnzd 12527 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โค) |
25 | 23, 24 | gcdcomd 16395 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ gcd ๐) = (๐ gcd ๐)) |
26 | | simprr 772 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ gcd ๐) = 1) |
27 | 25, 26 | eqtrd 2777 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ gcd ๐) = 1) |
28 | | simprl 770 |
. . . . 5
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ (โ โ
{2})) |
29 | 8 | adantr 482 |
. . . . 5
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ (โ โ
{2})) |
30 | | eldifi 4087 |
. . . . . . . 8
โข (๐ โ (โ โ {2})
โ ๐ โ
โ) |
31 | | prmrp 16589 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
32 | 30, 10, 31 | syl2anr 598 |
. . . . . . 7
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง ๐ โ (โ โ {2})) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
33 | 32 | biimpd 228 |
. . . . . 6
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง ๐ โ (โ โ {2})) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
34 | 33 | impr 456 |
. . . . 5
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ ๐) |
35 | | lgsquad 26734 |
. . . . 5
โข ((๐ โ (โ โ {2})
โง ๐ โ (โ
โ {2}) โง ๐ โ
๐) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
36 | 28, 29, 34, 35 | syl3anc 1372 |
. . . 4
โข (((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
37 | | biid 261 |
. . . 4
โข
(โ๐ฅ โ
(1...๐ฆ)((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ
โ๐ฅ โ (1...๐ฆ)((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
38 | 6, 7, 12, 22, 27, 36, 37 | lgsquad2lem2 26736 |
. . 3
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
39 | | lgscl 26662 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
40 | 24, 23, 39 | syl2anc 585 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ /L ๐) โ โค) |
41 | | lgscl 26662 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
42 | 23, 24, 41 | syl2anc 585 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ /L ๐) โ โค) |
43 | | zcn 12505 |
. . . . 5
โข ((๐ /L ๐) โ โค โ (๐ /L ๐) โ
โ) |
44 | | zcn 12505 |
. . . . 5
โข ((๐ /L ๐) โ โค โ (๐ /L ๐) โ
โ) |
45 | | mulcom 11138 |
. . . . 5
โข (((๐ /L ๐) โ โ โง (๐ /L ๐) โ โ) โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท (๐ /L ๐))) |
46 | 43, 44, 45 | syl2an 597 |
. . . 4
โข (((๐ /L ๐) โ โค โง (๐ /L ๐) โ โค) โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท (๐ /L ๐))) |
47 | 40, 42, 46 | syl2anc 585 |
. . 3
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท (๐ /L ๐))) |
48 | 12 | nncnd 12170 |
. . . . . . 7
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โ) |
49 | | ax-1cn 11110 |
. . . . . . 7
โข 1 โ
โ |
50 | | subcl 11401 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
51 | 48, 49, 50 | sylancl 587 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ โ 1) โ โ) |
52 | 51 | halfcld 12399 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ โ 1) / 2) โ
โ) |
53 | 6 | nncnd 12170 |
. . . . . . 7
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ๐ โ โ) |
54 | | subcl 11401 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
55 | 53, 49, 54 | sylancl 587 |
. . . . . 6
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (๐ โ 1) โ โ) |
56 | 55 | halfcld 12399 |
. . . . 5
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ โ 1) / 2) โ
โ) |
57 | 52, 56 | mulcomd 11177 |
. . . 4
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = (((๐ โ 1) / 2) ยท ((๐ โ 1) /
2))) |
58 | 57 | oveq2d 7374 |
. . 3
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ (-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2))) =
(-1โ(((๐ โ 1) /
2) ยท ((๐ โ 1)
/ 2)))) |
59 | 38, 47, 58 | 3eqtr4d 2787 |
. 2
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) |
60 | | biid 261 |
. 2
โข
(โ๐ฅ โ
(1...๐ฆ)((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ โ๐ฅ โ (1...๐ฆ)((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))) |
61 | 1, 2, 3, 4, 5, 59,
60 | lgsquad2lem2 26736 |
1
โข (๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |