Step | Hyp | Ref
| Expression |
1 | | simplrl 774 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โ) |
2 | | nnz 12584 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
4 | | nnz 12584 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
5 | 4 | ad3antrrr 727 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โค) |
6 | | lgscl 27051 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
7 | 3, 5, 6 | syl2anc 583 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โค) |
8 | 7 | zred 12671 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
9 | | absresq 15254 |
. . . . . . 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 16460 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = (๐ gcd ๐)) |
12 | | simpr 484 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
13 | 11, 12 | eqtrd 2771 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
14 | | lgsabs1 27076 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐
/L ๐)) =
1 โ (๐ gcd ๐) = 1)) |
15 | 3, 5, 14 | syl2anc 583 |
. . . . . . . . 9
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐)) = 1 โ (๐ gcd ๐) = 1)) |
16 | 13, 15 | mpbird 257 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (absโ(๐ /L ๐)) = 1) |
17 | 16 | oveq1d 7427 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐))โ2) = (1โ2)) |
18 | | sq1 14164 |
. . . . . . 7
โข
(1โ2) = 1 |
19 | 17, 18 | eqtrdi 2787 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((absโ(๐ /L ๐))โ2) = 1) |
20 | 7 | zcnd 12672 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
21 | 20 | sqvald 14113 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐)โ2) = ((๐ /L ๐) ยท (๐ /L ๐))) |
22 | 10, 19, 21 | 3eqtr3d 2779 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ 1 = ((๐ /L ๐) ยท (๐ /L ๐))) |
23 | 22 | oveq2d 7428 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = ((๐ /L ๐) ยท ((๐ /L ๐) ยท (๐ /L ๐)))) |
24 | | lgscl 27051 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ (๐ /L ๐) โ
โค) |
25 | 5, 3, 24 | syl2anc 583 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โค) |
26 | 25 | zcnd 12672 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) โ โ) |
27 | 26, 20, 20 | mulassd 11242 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท ((๐ /L ๐) ยท (๐ /L ๐)))) |
28 | 23, 27 | eqtr4d 2774 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐))) |
29 | 26 | mulridd 11236 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท 1) = (๐ /L ๐)) |
30 | | simplll 772 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ๐ โ โ) |
31 | | simpllr 773 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
32 | | simplrr 775 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
33 | 30, 31, 1, 32, 12 | lgsquad2 27126 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
34 | 33 | oveq1d 7427 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (((๐ /L ๐) ยท (๐ /L ๐)) ยท (๐ /L ๐)) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
35 | 28, 29, 34 | 3eqtr3d 2779 |
. 2
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง (๐ gcd ๐) = 1) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
36 | | neg1cn 12331 |
. . . . . 6
โข -1 โ
โ |
37 | 36 | a1i 11 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ -1 โ
โ) |
38 | | neg1ne0 12333 |
. . . . . 6
โข -1 โ
0 |
39 | 38 | a1i 11 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ -1 โ 0) |
40 | 4 | ad3antrrr 727 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ๐ โ โค) |
41 | | simpllr 773 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
42 | | 1zzd 12598 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 1 โ
โค) |
43 | | 2prm 16634 |
. . . . . . . . 9
โข 2 โ
โ |
44 | | nprmdvds1 16648 |
. . . . . . . . 9
โข (2 โ
โ โ ยฌ 2 โฅ 1) |
45 | 43, 44 | mp1i 13 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ
1) |
46 | | omoe 16312 |
. . . . . . . 8
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ โ 1)) |
47 | 40, 41, 42, 45, 46 | syl22anc 836 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 2 โฅ (๐ โ 1)) |
48 | | 2z 12599 |
. . . . . . . 8
โข 2 โ
โค |
49 | | 2ne0 12321 |
. . . . . . . 8
โข 2 โ
0 |
50 | | peano2zm 12610 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
51 | 40, 50 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ โ 1) โ โค) |
52 | | dvdsval2 16205 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง (๐ โ 1) โ โค) โ (2
โฅ (๐ โ 1)
โ ((๐ โ 1) / 2)
โ โค)) |
53 | 48, 49, 51, 52 | mp3an12i 1464 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (2 โฅ (๐ โ 1) โ ((๐ โ 1) / 2) โ
โค)) |
54 | 47, 53 | mpbid 231 |
. . . . . 6
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((๐ โ 1) / 2) โ
โค) |
55 | 2 | adantr 480 |
. . . . . . . . 9
โข ((๐ โ โ โง ยฌ 2
โฅ ๐) โ ๐ โ
โค) |
56 | 55 | ad2antlr 724 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ๐ โ โค) |
57 | | simplrr 775 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ยฌ 2 โฅ ๐) |
58 | | omoe 16312 |
. . . . . . . 8
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ โ 1)) |
59 | 56, 57, 42, 45, 58 | syl22anc 836 |
. . . . . . 7
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ 2 โฅ (๐ โ 1)) |
60 | | peano2zm 12610 |
. . . . . . . . 9
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
61 | 56, 60 | syl 17 |
. . . . . . . 8
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ โ 1) โ โค) |
62 | | dvdsval2 16205 |
. . . . . . . 8
โข ((2
โ โค โง 2 โ 0 โง (๐ โ 1) โ โค) โ (2
โฅ (๐ โ 1)
โ ((๐ โ 1) / 2)
โ โค)) |
63 | 48, 49, 61, 62 | mp3an12i 1464 |
. . . . . . 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 12677 |
. . . . 5
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) โ
โค) |
66 | 37, 39, 65 | expclzd 14121 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ
โ) |
67 | 66 | mul01d 11418 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท 0) =
0) |
68 | | lgsne0 27075 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
69 | | gcdcom 16459 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (๐ gcd ๐)) |
70 | 69 | eqeq1d 2733 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ gcd ๐) = 1 โ (๐ gcd ๐) = 1)) |
71 | 68, 70 | bitrd 279 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
72 | 2, 4, 71 | syl2anr 596 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
73 | 72 | necon1bbid 2979 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
74 | 73 | ad2ant2r 744 |
. . . . 5
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
75 | 74 | biimpa 476 |
. . . 4
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = 0) |
76 | 75 | oveq2d 7428 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐)) = ((-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2)))
ยท 0)) |
77 | | lgsne0 27075 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โค) โ ((๐ /L ๐) โ 0 โ (๐ gcd ๐) = 1)) |
78 | 77 | necon1bbid 2979 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
79 | 4, 2, 78 | syl2an 595 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
80 | 79 | ad2ant2r 744 |
. . . 4
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (ยฌ
(๐ gcd ๐) = 1 โ (๐ /L ๐) = 0)) |
81 | 80 | biimpa 476 |
. . 3
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = 0) |
82 | 67, 76, 81 | 3eqtr4rd 2782 |
. 2
โข ((((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โง ยฌ
(๐ gcd ๐) = 1) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(๐ /L
๐))) |
83 | 35, 82 | pm2.61dan 810 |
1
โข (((๐ โ โ โง ยฌ 2
โฅ ๐) โง (๐ โ โ โง ยฌ 2
โฅ ๐)) โ (๐ /L ๐) = ((-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2)))
ยท (๐
/L ๐))) |