Step | Hyp | Ref
| Expression |
1 | | simplrl 773 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โ) |
2 | | nnz 12583 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
4 | | nnz 12583 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
5 | 4 | ad3antrrr 726 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
6 | | lgscl 27050 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
7 | 3, 5, 6 | syl2anc 582 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โค) |
8 | 7 | zred 12670 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
9 | | absresq 15253 |
. . . . . . 7
โข ((๐ /L ๐) โ โ โ
((absโ(๐
/L ๐))โ2) = ((๐ /L ๐)โ2)) |
10 | 8, 9 | syl 17 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐))โ2) = ((๐ /L ๐)โ2)) |
11 | 3, 5 | gcdcomd 16459 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = (๐ gcd ๐)) |
12 | | simpr 483 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
13 | 11, 12 | eqtrd 2770 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
14 | | lgsabs1 27075 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐
/L ๐)) =
1 โ (๐ gcd ๐) = 1)) |
15 | 3, 5, 14 | syl2anc 582 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐)) = 1 โ (๐ gcd ๐) = 1)) |
16 | 13, 15 | mpbird 256 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (absโ(๐ /L ๐)) = 1) |
17 | 16 | oveq1d 7426 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐))โ2) = (1โ2)) |
18 | | sq1 14163 |
. . . . . . 7
โข
(1โ2) = 1 |
19 | 17, 18 | eqtrdi 2786 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐))โ2) = 1) |
20 | 7 | zcnd 12671 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
21 | 20 | sqvald 14112 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐)โ2) = ((๐ /L ๐) ยท (๐ /L ๐))) |
22 | 10, 19, 21 | 3eqtr3d 2778 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ 1 = ((๐ /L ๐) ยท (๐ /L ๐))) |
23 | 22 | oveq2d 7427 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = ((๐ /L ๐) ยท ((๐ /L ๐) ยท (๐ /L ๐)))) |
24 | | lgscl 27050 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
25 | 5, 3, 24 | syl2anc 582 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โค) |
26 | 25 | zcnd 12671 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
27 | 26, 20, 20 | mulassd 11241 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท ((๐ /L ๐) ยท (๐ /L ๐)))) |
28 | 23, 27 | eqtr4d 2773 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐))) |
29 | 26 | mulridd 11235 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = (๐ /L ๐)) |
30 | | simplll 771 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โ) |
31 | | simpllr 772 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
32 | | simplrr 774 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
33 | 30, 31, 1, 32, 12 | lgsquad2 27125 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
34 | 33 | oveq1d 7426 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐)) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
35 | 28, 29, 34 | 3eqtr3d 2778 |
. 2
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
36 | | neg1cn 12330 |
. . . . . 6
โข -1 โ
โ |
37 | 36 | a1i 11 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ -1 โ
โ) |
38 | | neg1ne0 12332 |
. . . . . 6
โข -1 โ
0 |
39 | 38 | a1i 11 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ -1 โ 0) |
40 | 4 | ad3antrrr 726 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ๐ โ โค) |
41 | | simpllr 772 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
42 | | 1zzd 12597 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 1 โ
โค) |
43 | | 2prm 16633 |
. . . . . . . . 9
โข 2 โ
โ |
44 | | nprmdvds1 16647 |
. . . . . . . . 9
โข (2 โ
โ โ ยฌ 2 โฅ 1) |
45 | 43, 44 | mp1i 13 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ
1) |
46 | | omoe 16311 |
. . . . . . . 8
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ โ 1)) |
47 | 40, 41, 42, 45, 46 | syl22anc 835 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 2 โฅ (๐ โ 1)) |
48 | | 2z 12598 |
. . . . . . . 8
โข 2 โ
โค |
49 | | 2ne0 12320 |
. . . . . . . 8
โข 2 โ
0 |
50 | | peano2zm 12609 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
51 | 40, 50 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ โ 1) โ โค) |
52 | | dvdsval2 16204 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง (๐ โ 1) โ โค) โ (2
โฅ (๐ โ 1)
โ ((๐ โ 1) / 2)
โ โค)) |
53 | 48, 49, 51, 52 | mp3an12i 1463 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (2 โฅ (๐ โ 1) โ ((๐ โ 1) / 2) โ
โค)) |
54 | 47, 53 | mpbid 231 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((๐ โ 1) / 2) โ
โค) |
55 | 2 | adantr 479 |
. . . . . . . . 9
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ
โค) |
56 | 55 | ad2antlr 723 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ๐ โ โค) |
57 | | simplrr 774 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
58 | | omoe 16311 |
. . . . . . . 8
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ โ 1)) |
59 | 56, 57, 42, 45, 58 | syl22anc 835 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 2 โฅ (๐ โ 1)) |
60 | | peano2zm 12609 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
61 | 56, 60 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ โ 1) โ โค) |
62 | | dvdsval2 16204 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง (๐ โ 1) โ โค) โ (2
โฅ (๐ โ 1)
โ ((๐ โ 1) / 2)
โ โค)) |
63 | 48, 49, 61, 62 | mp3an12i 1463 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (2 โฅ (๐ โ 1) โ ((๐ โ 1) / 2) โ
โค)) |
64 | 59, 63 | mpbid 231 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((๐ โ 1) / 2) โ
โค) |
65 | 54, 64 | zmulcld 12676 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) โ
โค) |
66 | 37, 39, 65 | expclzd 14120 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ
โ) |
67 | 66 | mul01d 11417 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท 0) =
0) |
68 | | lgsne0 27074 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
69 | | gcdcom 16458 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (๐ gcd ๐)) |
70 | 69 | eqeq1d 2732 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) = 1 โ (๐ gcd ๐) = 1)) |
71 | 68, 70 | bitrd 278 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
72 | 2, 4, 71 | syl2anr 595 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
73 | 72 | necon1bbid 2978 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
74 | 73 | ad2ant2r 743 |
. . . . 5
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
75 | 74 | biimpa 475 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = 0) |
76 | 75 | oveq2d 7427 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐)) = ((-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2)))
ยท 0)) |
77 | | lgsne0 27074 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
78 | 77 | necon1bbid 2978 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
79 | 4, 2, 78 | syl2an 594 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
80 | 79 | ad2ant2r 743 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
81 | 80 | biimpa 475 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = 0) |
82 | 67, 76, 81 | 3eqtr4rd 2781 |
. 2
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
83 | 35, 82 | pm2.61dan 809 |
1
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2)))
ยท (๐
/L ๐))) |