Step | Hyp | Ref
| Expression |
1 | | lgsquad2.1 |
. . . 4
โข (๐ โ ๐ โ โ) |
2 | | 2nn 12227 |
. . . . 5
โข 2 โ
โ |
3 | 2 | a1i 11 |
. . . 4
โข (๐ โ 2 โ
โ) |
4 | | lgsquad2.3 |
. . . 4
โข (๐ โ ๐ โ โ) |
5 | 1 | nnzd 12527 |
. . . . . 6
โข (๐ โ ๐ โ โค) |
6 | | 2z 12536 |
. . . . . 6
โข 2 โ
โค |
7 | | gcdcom 16394 |
. . . . . 6
โข ((๐ โ โค โง 2 โ
โค) โ (๐ gcd 2) =
(2 gcd ๐)) |
8 | 5, 6, 7 | sylancl 587 |
. . . . 5
โข (๐ โ (๐ gcd 2) = (2 gcd ๐)) |
9 | | lgsquad2.2 |
. . . . . 6
โข (๐ โ ยฌ 2 โฅ ๐) |
10 | | 2prm 16569 |
. . . . . . 7
โข 2 โ
โ |
11 | | coprm 16588 |
. . . . . . 7
โข ((2
โ โ โง ๐
โ โค) โ (ยฌ 2 โฅ ๐ โ (2 gcd ๐) = 1)) |
12 | 10, 5, 11 | sylancr 588 |
. . . . . 6
โข (๐ โ (ยฌ 2 โฅ ๐ โ (2 gcd ๐) = 1)) |
13 | 9, 12 | mpbid 231 |
. . . . 5
โข (๐ โ (2 gcd ๐) = 1) |
14 | 8, 13 | eqtrd 2777 |
. . . 4
โข (๐ โ (๐ gcd 2) = 1) |
15 | | rpmulgcd 16438 |
. . . 4
โข (((๐ โ โ โง 2 โ
โ โง ๐ โ
โ) โง (๐ gcd 2) =
1) โ (๐ gcd (2
ยท ๐)) = (๐ gcd ๐)) |
16 | 1, 3, 4, 14, 15 | syl31anc 1374 |
. . 3
โข (๐ โ (๐ gcd (2 ยท ๐)) = (๐ gcd ๐)) |
17 | | lgsquad2.5 |
. . 3
โข (๐ โ (๐ gcd ๐) = 1) |
18 | 16, 17 | eqtrd 2777 |
. 2
โข (๐ โ (๐ gcd (2 ยท ๐)) = 1) |
19 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = 1 โ (๐ /L ๐) = (1 /L ๐)) |
20 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = 1 โ (๐ /L ๐) = (๐ /L 1)) |
21 | 19, 20 | oveq12d 7376 |
. . . . . . 7
โข (๐ = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((1 /L ๐) ยท (๐ /L 1))) |
22 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = 1 โ (๐ โ 1) = (1 โ 1)) |
23 | | 1m1e0 12226 |
. . . . . . . . . . . 12
โข (1
โ 1) = 0 |
24 | 22, 23 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ = 1 โ (๐ โ 1) = 0) |
25 | 24 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = 1 โ ((๐ โ 1) / 2) = (0 / 2)) |
26 | | 2cn 12229 |
. . . . . . . . . . 11
โข 2 โ
โ |
27 | | 2ne0 12258 |
. . . . . . . . . . 11
โข 2 โ
0 |
28 | 26, 27 | div0i 11890 |
. . . . . . . . . 10
โข (0 / 2) =
0 |
29 | 25, 28 | eqtrdi 2793 |
. . . . . . . . 9
โข (๐ = 1 โ ((๐ โ 1) / 2) = 0) |
30 | 29 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = 1 โ (((๐ โ 1) / 2) ยท
((๐ โ 1) / 2)) = (0
ยท ((๐ โ 1) /
2))) |
31 | 30 | oveq2d 7374 |
. . . . . . 7
โข (๐ = 1 โ (-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2))) =
(-1โ(0 ยท ((๐
โ 1) / 2)))) |
32 | 21, 31 | eqeq12d 2753 |
. . . . . 6
โข (๐ = 1 โ (((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ ((1
/L ๐)
ยท (๐
/L 1)) = (-1โ(0 ยท ((๐ โ 1) / 2))))) |
33 | 32 | imbi2d 341 |
. . . . 5
โข (๐ = 1 โ (((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ ((๐ gcd (2 ยท ๐)) = 1 โ ((1
/L ๐)
ยท (๐
/L 1)) = (-1โ(0 ยท ((๐ โ 1) / 2)))))) |
34 | 33 | imbi2d 341 |
. . . 4
โข (๐ = 1 โ ((๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((1 /L ๐) ยท (๐ /L 1)) = (-1โ(0
ยท ((๐ โ 1) /
2))))))) |
35 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ฅ โ (๐ gcd (2 ยท ๐)) = (๐ฅ gcd (2 ยท ๐))) |
36 | 35 | eqeq1d 2739 |
. . . . . 6
โข (๐ = ๐ฅ โ ((๐ gcd (2 ยท ๐)) = 1 โ (๐ฅ gcd (2 ยท ๐)) = 1)) |
37 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ /L ๐) = (๐ฅ /L ๐)) |
38 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ /L ๐) = (๐ /L ๐ฅ)) |
39 | 37, 38 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ฅ โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ))) |
40 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ โ 1) = (๐ฅ โ 1)) |
41 | 40 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ ((๐ โ 1) / 2) = ((๐ฅ โ 1) / 2)) |
42 | 41 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = (((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))) |
43 | 42 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ฅ โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) = (-1โ(((๐ฅ โ 1) / 2) ยท
((๐ โ 1) /
2)))) |
44 | 39, 43 | eqeq12d 2753 |
. . . . . 6
โข (๐ = ๐ฅ โ (((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))) |
45 | 36, 44 | imbi12d 345 |
. . . . 5
โข (๐ = ๐ฅ โ (((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ ((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) |
46 | 45 | imbi2d 341 |
. . . 4
โข (๐ = ๐ฅ โ ((๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (๐ โ ((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) |
47 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ฆ โ (๐ gcd (2 ยท ๐)) = (๐ฆ gcd (2 ยท ๐))) |
48 | 47 | eqeq1d 2739 |
. . . . . 6
โข (๐ = ๐ฆ โ ((๐ gcd (2 ยท ๐)) = 1 โ (๐ฆ gcd (2 ยท ๐)) = 1)) |
49 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = ๐ฆ โ (๐ /L ๐) = (๐ฆ /L ๐)) |
50 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ฆ โ (๐ /L ๐) = (๐ /L ๐ฆ)) |
51 | 49, 50 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ฆ โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ))) |
52 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ โ 1) = (๐ฆ โ 1)) |
53 | 52 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ ((๐ โ 1) / 2) = ((๐ฆ โ 1) / 2)) |
54 | 53 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ฆ โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = (((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))) |
55 | 54 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ฆ โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) = (-1โ(((๐ฆ โ 1) / 2) ยท
((๐ โ 1) /
2)))) |
56 | 51, 55 | eqeq12d 2753 |
. . . . . 6
โข (๐ = ๐ฆ โ (((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))) |
57 | 48, 56 | imbi12d 345 |
. . . . 5
โข (๐ = ๐ฆ โ (((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) |
58 | 57 | imbi2d 341 |
. . . 4
โข (๐ = ๐ฆ โ ((๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (๐ โ ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) |
59 | | oveq1 7365 |
. . . . . . 7
โข (๐ = (๐ฅ ยท ๐ฆ) โ (๐ gcd (2 ยท ๐)) = ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐))) |
60 | 59 | eqeq1d 2739 |
. . . . . 6
โข (๐ = (๐ฅ ยท ๐ฆ) โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1)) |
61 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = (๐ฅ ยท ๐ฆ) โ (๐ /L ๐) = ((๐ฅ ยท ๐ฆ) /L ๐)) |
62 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = (๐ฅ ยท ๐ฆ) โ (๐ /L ๐) = (๐ /L (๐ฅ ยท ๐ฆ))) |
63 | 61, 62 | oveq12d 7376 |
. . . . . . 7
โข (๐ = (๐ฅ ยท ๐ฆ) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ)))) |
64 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = (๐ฅ ยท ๐ฆ) โ (๐ โ 1) = ((๐ฅ ยท ๐ฆ) โ 1)) |
65 | 64 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = (๐ฅ ยท ๐ฆ) โ ((๐ โ 1) / 2) = (((๐ฅ ยท ๐ฆ) โ 1) / 2)) |
66 | 65 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = (๐ฅ ยท ๐ฆ) โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))) |
67 | 66 | oveq2d 7374 |
. . . . . . 7
โข (๐ = (๐ฅ ยท ๐ฆ) โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
68 | 63, 67 | eqeq12d 2753 |
. . . . . 6
โข (๐ = (๐ฅ ยท ๐ฆ) โ (((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
69 | 60, 68 | imbi12d 345 |
. . . . 5
โข (๐ = (๐ฅ ยท ๐ฆ) โ (((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2)))))) |
70 | 69 | imbi2d 341 |
. . . 4
โข (๐ = (๐ฅ ยท ๐ฆ) โ ((๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (๐ โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))))))) |
71 | | oveq1 7365 |
. . . . . . 7
โข (๐ = ๐ โ (๐ gcd (2 ยท ๐)) = (๐ gcd (2 ยท ๐))) |
72 | 71 | eqeq1d 2739 |
. . . . . 6
โข (๐ = ๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ (๐ gcd (2 ยท ๐)) = 1)) |
73 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ /L ๐) = (๐ /L ๐)) |
74 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ /L ๐) = (๐ /L ๐)) |
75 | 73, 74 | oveq12d 7376 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((๐ /L ๐) ยท (๐ /L ๐))) |
76 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ โ 1) = (๐ โ 1)) |
77 | 76 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ โ 1) / 2) = ((๐ โ 1) / 2)) |
78 | 77 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = (((๐ โ 1) / 2) ยท ((๐ โ 1) /
2))) |
79 | 78 | oveq2d 7374 |
. . . . . . 7
โข (๐ = ๐ โ (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) = (-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) /
2)))) |
80 | 75, 79 | eqeq12d 2753 |
. . . . . 6
โข (๐ = ๐ โ (((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
81 | 72, 80 | imbi12d 345 |
. . . . 5
โข (๐ = ๐ โ (((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))))) |
82 | 81 | imbi2d 341 |
. . . 4
โข (๐ = ๐ โ ((๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2))))))) |
83 | | 1t1e1 12316 |
. . . . . . 7
โข (1
ยท 1) = 1 |
84 | | neg1cn 12268 |
. . . . . . . 8
โข -1 โ
โ |
85 | | exp0 13972 |
. . . . . . . 8
โข (-1
โ โ โ (-1โ0) = 1) |
86 | 84, 85 | ax-mp 5 |
. . . . . . 7
โข
(-1โ0) = 1 |
87 | 83, 86 | eqtr4i 2768 |
. . . . . 6
โข (1
ยท 1) = (-1โ0) |
88 | | sq1 14100 |
. . . . . . . . 9
โข
(1โ2) = 1 |
89 | 88 | oveq1i 7368 |
. . . . . . . 8
โข
((1โ2) /L ๐) = (1 /L ๐) |
90 | | 1z 12534 |
. . . . . . . . . 10
โข 1 โ
โค |
91 | | ax-1ne0 11121 |
. . . . . . . . . 10
โข 1 โ
0 |
92 | 90, 91 | pm3.2i 472 |
. . . . . . . . 9
โข (1 โ
โค โง 1 โ 0) |
93 | 4 | nnzd 12527 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
94 | | 1gcd 16415 |
. . . . . . . . . 10
โข (๐ โ โค โ (1 gcd
๐) = 1) |
95 | 93, 94 | syl 17 |
. . . . . . . . 9
โข (๐ โ (1 gcd ๐) = 1) |
96 | | lgssq 26688 |
. . . . . . . . 9
โข (((1
โ โค โง 1 โ 0) โง ๐ โ โค โง (1 gcd ๐) = 1) โ ((1โ2)
/L ๐) =
1) |
97 | 92, 93, 95, 96 | mp3an2i 1467 |
. . . . . . . 8
โข (๐ โ ((1โ2)
/L ๐) =
1) |
98 | 89, 97 | eqtr3id 2791 |
. . . . . . 7
โข (๐ โ (1 /L
๐) = 1) |
99 | 88 | oveq2i 7369 |
. . . . . . . 8
โข (๐ /L
(1โ2)) = (๐
/L 1) |
100 | | 1nn 12165 |
. . . . . . . . . 10
โข 1 โ
โ |
101 | 100 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
102 | | gcd1 16409 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ gcd 1) = 1) |
103 | 93, 102 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ gcd 1) = 1) |
104 | | lgssq2 26689 |
. . . . . . . . 9
โข ((๐ โ โค โง 1 โ
โ โง (๐ gcd 1) =
1) โ (๐
/L (1โ2)) = 1) |
105 | 93, 101, 103, 104 | syl3anc 1372 |
. . . . . . . 8
โข (๐ โ (๐ /L (1โ2)) =
1) |
106 | 99, 105 | eqtr3id 2791 |
. . . . . . 7
โข (๐ โ (๐ /L 1) =
1) |
107 | 98, 106 | oveq12d 7376 |
. . . . . 6
โข (๐ โ ((1 /L
๐) ยท (๐ /L 1)) = (1
ยท 1)) |
108 | | nnm1nn0 12455 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
109 | 4, 108 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ โ 1) โ
โ0) |
110 | 109 | nn0cnd 12476 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โ) |
111 | 110 | halfcld 12399 |
. . . . . . . 8
โข (๐ โ ((๐ โ 1) / 2) โ
โ) |
112 | 111 | mul02d 11354 |
. . . . . . 7
โข (๐ โ (0 ยท ((๐ โ 1) / 2)) =
0) |
113 | 112 | oveq2d 7374 |
. . . . . 6
โข (๐ โ (-1โ(0 ยท
((๐ โ 1) / 2))) =
(-1โ0)) |
114 | 87, 107, 113 | 3eqtr4a 2803 |
. . . . 5
โข (๐ โ ((1 /L
๐) ยท (๐ /L 1)) =
(-1โ(0 ยท ((๐
โ 1) / 2)))) |
115 | 114 | a1d 25 |
. . . 4
โข (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((1 /L ๐) ยท (๐ /L 1)) = (-1โ(0
ยท ((๐ โ 1) /
2))))) |
116 | | simprl 770 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ โ) |
117 | | prmz 16552 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
118 | 117 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ โค) |
119 | 6 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ 2 โ
โค) |
120 | 4 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ โ) |
121 | 120 | nnzd 12527 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ โค) |
122 | | zmulcl 12553 |
. . . . . . . . . . . 12
โข ((2
โ โค โง ๐
โ โค) โ (2 ยท ๐) โ โค) |
123 | 6, 121, 122 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (2 ยท ๐) โ
โค) |
124 | | simprr 772 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (๐ gcd (2 ยท ๐)) = 1) |
125 | | dvdsmul1 16161 |
. . . . . . . . . . . 12
โข ((2
โ โค โง ๐
โ โค) โ 2 โฅ (2 ยท ๐)) |
126 | 6, 121, 125 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ 2 โฅ (2 ยท ๐)) |
127 | | rpdvds 16537 |
. . . . . . . . . . 11
โข (((๐ โ โค โง 2 โ
โค โง (2 ยท ๐) โ โค) โง ((๐ gcd (2 ยท ๐)) = 1 โง 2 โฅ (2 ยท ๐))) โ (๐ gcd 2) = 1) |
128 | 118, 119,
123, 124, 126, 127 | syl32anc 1379 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (๐ gcd 2) = 1) |
129 | | prmrp 16589 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 2 โ
โ) โ ((๐ gcd 2)
= 1 โ ๐ โ
2)) |
130 | 116, 10, 129 | sylancl 587 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ((๐ gcd 2) = 1 โ ๐ โ 2)) |
131 | 128, 130 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ 2) |
132 | | eldifsn 4748 |
. . . . . . . . 9
โข (๐ โ (โ โ {2})
โ (๐ โ โ
โง ๐ โ
2)) |
133 | 116, 131,
132 | sylanbrc 584 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ (โ โ
{2})) |
134 | | prmnn 16551 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
135 | 134 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ๐ โ โ) |
136 | 2 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ 2 โ
โ) |
137 | | rpmulgcd 16438 |
. . . . . . . . . 10
โข (((๐ โ โ โง 2 โ
โ โง ๐ โ
โ) โง (๐ gcd 2) =
1) โ (๐ gcd (2
ยท ๐)) = (๐ gcd ๐)) |
138 | 135, 136,
120, 128, 137 | syl31anc 1374 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (๐ gcd (2 ยท ๐)) = (๐ gcd ๐)) |
139 | 138, 124 | eqtr3d 2779 |
. . . . . . . 8
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (๐ gcd ๐) = 1) |
140 | 133, 139 | jca 513 |
. . . . . . 7
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) |
141 | | lgsquad2lem2.f |
. . . . . . 7
โข ((๐ โง (๐ โ (โ โ {2}) โง (๐ gcd ๐) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) |
142 | 140, 141 | syldan 592 |
. . . . . 6
โข ((๐ โง (๐ โ โ โง (๐ gcd (2 ยท ๐)) = 1)) โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))) |
143 | 142 | exp32 422 |
. . . . 5
โข (๐ โ (๐ โ โ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) |
144 | 143 | com12 32 |
. . . 4
โข (๐ โ โ โ (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) |
145 | | jcab 519 |
. . . . 5
โข ((๐ โ (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) โ ((๐ โ ((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โง (๐ โ ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) |
146 | | simplrl 776 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ๐ฅ โ
(โคโฅโ2)) |
147 | | eluz2nn 12810 |
. . . . . . . . . . . 12
โข (๐ฅ โ
(โคโฅโ2) โ ๐ฅ โ โ) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ๐ฅ โ
โ) |
149 | | simplrr 777 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ๐ฆ โ
(โคโฅโ2)) |
150 | | eluz2nn 12810 |
. . . . . . . . . . . 12
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โ) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ๐ฆ โ
โ) |
152 | 148, 151 | nnmulcld 12207 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ (๐ฅ ยท ๐ฆ) โ โ) |
153 | | n2dvds1 16251 |
. . . . . . . . . . . 12
โข ยฌ 2
โฅ 1 |
154 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ โ โค) |
155 | 6, 154, 125 | sylancr 588 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ 2 โฅ (2 ยท ๐)) |
156 | | eluzelz 12774 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ
(โคโฅโ2) โ ๐ฅ โ โค) |
157 | | eluzelz 12774 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โค) |
158 | 156, 157 | anim12i 614 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ (๐ฅ โ โค
โง ๐ฆ โ
โค)) |
159 | 158 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฅ โ โค โง ๐ฆ โ โค)) |
160 | | zmulcl 12553 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ ยท ๐ฆ) โ โค) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฅ ยท ๐ฆ) โ โค) |
162 | 6, 154, 122 | sylancr 588 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (2 ยท ๐) โ โค) |
163 | | dvdsgcd 16426 |
. . . . . . . . . . . . . . 15
โข ((2
โ โค โง (๐ฅ
ยท ๐ฆ) โ โค
โง (2 ยท ๐) โ
โค) โ ((2 โฅ (๐ฅ ยท ๐ฆ) โง 2 โฅ (2 ยท ๐)) โ 2 โฅ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)))) |
164 | 6, 161, 162, 163 | mp3an2i 1467 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((2 โฅ (๐ฅ ยท ๐ฆ) โง 2 โฅ (2 ยท ๐)) โ 2 โฅ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)))) |
165 | 155, 164 | mpan2d 693 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (2 โฅ (๐ฅ ยท ๐ฆ) โ 2 โฅ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)))) |
166 | | simpr 486 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) |
167 | 166 | breq2d 5118 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (2 โฅ ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) โ 2 โฅ 1)) |
168 | 165, 167 | sylibd 238 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (2 โฅ (๐ฅ ยท ๐ฆ) โ 2 โฅ 1)) |
169 | 153, 168 | mtoi 198 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ยฌ 2 โฅ (๐ฅ ยท ๐ฆ)) |
170 | 169 | adantrr 716 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ยฌ 2
โฅ (๐ฅ ยท ๐ฆ)) |
171 | 4 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ๐ โ
โ) |
172 | | lgsquad2.4 |
. . . . . . . . . . 11
โข (๐ โ ยฌ 2 โฅ ๐) |
173 | 172 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ยฌ 2
โฅ ๐) |
174 | | dvdsmul2 16162 |
. . . . . . . . . . . . 13
โข ((2
โ โค โง ๐
โ โค) โ ๐
โฅ (2 ยท ๐)) |
175 | 6, 154, 174 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ โฅ (2 ยท ๐)) |
176 | | rpdvds 16537 |
. . . . . . . . . . . 12
โข ((((๐ฅ ยท ๐ฆ) โ โค โง ๐ โ โค โง (2 ยท ๐) โ โค) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง ๐ โฅ (2 ยท ๐))) โ ((๐ฅ ยท ๐ฆ) gcd ๐) = 1) |
177 | 161, 154,
162, 166, 175, 176 | syl32anc 1379 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((๐ฅ ยท ๐ฆ) gcd ๐) = 1) |
178 | 177 | adantrr 716 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ((๐ฅ ยท ๐ฆ) gcd ๐) = 1) |
179 | | eqidd 2738 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ (๐ฅ ยท ๐ฆ) = (๐ฅ ยท ๐ฆ)) |
180 | 159 | simpld 496 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ฅ โ โค) |
181 | 180, 162 | gcdcomd 16395 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฅ gcd (2 ยท ๐)) = ((2 ยท ๐) gcd ๐ฅ)) |
182 | 162, 161 | gcdcomd 16395 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((2 ยท ๐) gcd (๐ฅ ยท ๐ฆ)) = ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐))) |
183 | 182, 166 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((2 ยท ๐) gcd (๐ฅ ยท ๐ฆ)) = 1) |
184 | | dvdsmul1 16161 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ๐ฅ โฅ (๐ฅ ยท ๐ฆ)) |
185 | 159, 184 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ฅ โฅ (๐ฅ ยท ๐ฆ)) |
186 | | rpdvds 16537 |
. . . . . . . . . . . . . 14
โข ((((2
ยท ๐) โ โค
โง ๐ฅ โ โค
โง (๐ฅ ยท ๐ฆ) โ โค) โง (((2
ยท ๐) gcd (๐ฅ ยท ๐ฆ)) = 1 โง ๐ฅ โฅ (๐ฅ ยท ๐ฆ))) โ ((2 ยท ๐) gcd ๐ฅ) = 1) |
187 | 162, 180,
161, 183, 185, 186 | syl32anc 1379 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((2 ยท ๐) gcd ๐ฅ) = 1) |
188 | 181, 187 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฅ gcd (2 ยท ๐)) = 1) |
189 | 188 | adantrr 716 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ (๐ฅ gcd (2 ยท ๐)) = 1) |
190 | | simprrl 780 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))) |
191 | 189, 190 | mpd 15 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) |
192 | 159 | simprd 497 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ฆ โ โค) |
193 | 192, 162 | gcdcomd 16395 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฆ gcd (2 ยท ๐)) = ((2 ยท ๐) gcd ๐ฆ)) |
194 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ๐ฆ โฅ (๐ฅ ยท ๐ฆ)) |
195 | 159, 194 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ๐ฆ โฅ (๐ฅ ยท ๐ฆ)) |
196 | | rpdvds 16537 |
. . . . . . . . . . . . . 14
โข ((((2
ยท ๐) โ โค
โง ๐ฆ โ โค
โง (๐ฅ ยท ๐ฆ) โ โค) โง (((2
ยท ๐) gcd (๐ฅ ยท ๐ฆ)) = 1 โง ๐ฆ โฅ (๐ฅ ยท ๐ฆ))) โ ((2 ยท ๐) gcd ๐ฆ) = 1) |
197 | 162, 192,
161, 183, 195, 196 | syl32anc 1379 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ ((2 ยท ๐) gcd ๐ฆ) = 1) |
198 | 193, 197 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง ((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1) โ (๐ฆ gcd (2 ยท ๐)) = 1) |
199 | 198 | adantrr 716 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ (๐ฆ gcd (2 ยท ๐)) = 1) |
200 | | simprrr 781 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))) |
201 | 199, 200 | mpd 15 |
. . . . . . . . . 10
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2)))) |
202 | 152, 170,
171, 173, 178, 148, 151, 179, 191, 201 | lgsquad2lem1 26735 |
. . . . . . . . 9
โข (((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โง (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โง (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))))) โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
203 | 202 | exp32 422 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ ((((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2)))))) |
204 | 203 | com23 86 |
. . . . . . 7
โข ((๐ โง (๐ฅ โ (โคโฅโ2)
โง ๐ฆ โ
(โคโฅโ2))) โ ((((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2)))))) |
205 | 204 | expcom 415 |
. . . . . 6
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ (๐ โ ((((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))))))) |
206 | 205 | a2d 29 |
. . . . 5
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ((๐ โ (((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2)))) โง ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) โ (๐ โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))))))) |
207 | 145, 206 | biimtrrid 242 |
. . . 4
โข ((๐ฅ โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ (((๐ โ ((๐ฅ gcd (2 ยท ๐)) = 1 โ ((๐ฅ /L ๐) ยท (๐ /L ๐ฅ)) = (-1โ(((๐ฅ โ 1) / 2) ยท ((๐ โ 1) / 2))))) โง (๐ โ ((๐ฆ gcd (2 ยท ๐)) = 1 โ ((๐ฆ /L ๐) ยท (๐ /L ๐ฆ)) = (-1โ(((๐ฆ โ 1) / 2) ยท ((๐ โ 1) / 2)))))) โ (๐ โ (((๐ฅ ยท ๐ฆ) gcd (2 ยท ๐)) = 1 โ (((๐ฅ ยท ๐ฆ) /L ๐) ยท (๐ /L (๐ฅ ยท ๐ฆ))) = (-1โ((((๐ฅ ยท ๐ฆ) โ 1) / 2) ยท ((๐ โ 1) /
2))))))) |
208 | 34, 46, 58, 70, 82, 115, 144, 207 | prmind 16563 |
. . 3
โข (๐ โ โ โ (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))))) |
209 | 1, 208 | mpcom 38 |
. 2
โข (๐ โ ((๐ gcd (2 ยท ๐)) = 1 โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
210 | 18, 209 | mpd 15 |
1
โข (๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |