Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
โข (๐ โ ๐ โ (โ โ
{2})) |
2 | | lgseisen.1 |
. . . . 5
โข (๐ โ ๐ โ (โ โ
{2})) |
3 | | lgseisen.3 |
. . . . . 6
โข (๐ โ ๐ โ ๐) |
4 | 3 | necomd 3000 |
. . . . 5
โข (๐ โ ๐ โ ๐) |
5 | | lgsquad.5 |
. . . . 5
โข ๐ = ((๐ โ 1) / 2) |
6 | | lgsquad.4 |
. . . . 5
โข ๐ = ((๐ โ 1) / 2) |
7 | | eleq1w 2821 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (๐ฅ โ (1...๐) โ ๐ง โ (1...๐))) |
8 | | eleq1w 2821 |
. . . . . . . . . 10
โข (๐ฆ = ๐ค โ (๐ฆ โ (1...๐) โ ๐ค โ (1...๐))) |
9 | 7, 8 | bi2anan9 638 |
. . . . . . . . 9
โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ (๐ง โ (1...๐) โง ๐ค โ (1...๐)))) |
10 | 9 | biancomd 465 |
. . . . . . . 8
โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ (๐ค โ (1...๐) โง ๐ง โ (1...๐)))) |
11 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ (๐ฅ ยท ๐) = (๐ง ยท ๐)) |
12 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ฆ = ๐ค โ (๐ฆ ยท ๐) = (๐ค ยท ๐)) |
13 | 11, 12 | breqan12d 5122 |
. . . . . . . 8
โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โ (๐ง ยท ๐) < (๐ค ยท ๐))) |
14 | 10, 13 | anbi12d 632 |
. . . . . . 7
โข ((๐ฅ = ๐ง โง ๐ฆ = ๐ค) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โ ((๐ค โ (1...๐) โง ๐ง โ (1...๐)) โง (๐ง ยท ๐) < (๐ค ยท ๐)))) |
15 | 14 | ancoms 460 |
. . . . . 6
โข ((๐ฆ = ๐ค โง ๐ฅ = ๐ง) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โ ((๐ค โ (1...๐) โง ๐ง โ (1...๐)) โง (๐ง ยท ๐) < (๐ค ยท ๐)))) |
16 | 15 | cbvopabv 5179 |
. . . . 5
โข
{โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} = {โจ๐ค, ๐งโฉ โฃ ((๐ค โ (1...๐) โง ๐ง โ (1...๐)) โง (๐ง ยท ๐) < (๐ค ยท ๐))} |
17 | 1, 2, 4, 5, 6, 16 | lgsquadlem2 26732 |
. . . 4
โข (๐ โ (๐ /L ๐) = (-1โ(โฏโ{โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}))) |
18 | | relopabv 5778 |
. . . . . . . 8
โข Rel
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} |
19 | | fzfid 13879 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ Fin) |
20 | | fzfid 13879 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ Fin) |
21 | | xpfi 9262 |
. . . . . . . . . 10
โข
(((1...๐) โ Fin
โง (1...๐) โ Fin)
โ ((1...๐) ร
(1...๐)) โ
Fin) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ ((1...๐) ร (1...๐)) โ Fin) |
23 | | opabssxp 5725 |
. . . . . . . . 9
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ ((1...๐) ร (1...๐)) |
24 | | ssfi 9118 |
. . . . . . . . 9
โข
((((1...๐) ร
(1...๐)) โ Fin โง
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ ((1...๐) ร (1...๐))) โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ Fin) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . 8
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ Fin) |
26 | | cnven 8978 |
. . . . . . . 8
โข ((Rel
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โง {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ Fin) โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ โก{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) |
27 | 18, 25, 26 | sylancr 588 |
. . . . . . 7
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ โก{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) |
28 | | cnvopab 6092 |
. . . . . . 7
โข โก{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} = {โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} |
29 | 27, 28 | breqtrdi 5147 |
. . . . . 6
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ {โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) |
30 | | hasheni 14249 |
. . . . . 6
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ {โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ (โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) = (โฏโ{โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))})) |
31 | 29, 30 | syl 17 |
. . . . 5
โข (๐ โ
(โฏโ{โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) = (โฏโ{โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))})) |
32 | 31 | oveq2d 7374 |
. . . 4
โข (๐ โ
(-1โ(โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))})) = (-1โ(โฏโ{โจ๐ฆ, ๐ฅโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}))) |
33 | 17, 32 | eqtr4d 2780 |
. . 3
โข (๐ โ (๐ /L ๐) = (-1โ(โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}))) |
34 | | lgsquad.6 |
. . . 4
โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))} |
35 | 2, 1, 3, 6, 5, 34 | lgsquadlem2 26732 |
. . 3
โข (๐ โ (๐ /L ๐) = (-1โ(โฏโ๐))) |
36 | 33, 35 | oveq12d 7376 |
. 2
โข (๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = ((-1โ(โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))})) ยท (-1โ(โฏโ๐)))) |
37 | | neg1cn 12268 |
. . . 4
โข -1 โ
โ |
38 | 37 | a1i 11 |
. . 3
โข (๐ โ -1 โ
โ) |
39 | | opabssxp 5725 |
. . . . . 6
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))} โ ((1...๐) ร (1...๐)) |
40 | 34, 39 | eqsstri 3979 |
. . . . 5
โข ๐ โ ((1...๐) ร (1...๐)) |
41 | | ssfi 9118 |
. . . . 5
โข
((((1...๐) ร
(1...๐)) โ Fin โง
๐ โ ((1...๐) ร (1...๐))) โ ๐ โ Fin) |
42 | 22, 40, 41 | sylancl 587 |
. . . 4
โข (๐ โ ๐ โ Fin) |
43 | | hashcl 14257 |
. . . 4
โข (๐ โ Fin โ
(โฏโ๐) โ
โ0) |
44 | 42, 43 | syl 17 |
. . 3
โข (๐ โ (โฏโ๐) โ
โ0) |
45 | | hashcl 14257 |
. . . 4
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ Fin โ
(โฏโ{โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) โ
โ0) |
46 | 25, 45 | syl 17 |
. . 3
โข (๐ โ
(โฏโ{โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) โ
โ0) |
47 | 38, 44, 46 | expaddd 14054 |
. 2
โข (๐ โ
(-1โ((โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) + (โฏโ๐))) = ((-1โ(โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))})) ยท (-1โ(โฏโ๐)))) |
48 | 1 | eldifad 3923 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
50 | | prmnn 16551 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ ๐ โ
โ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
52 | 1, 5 | gausslemma2dlem0b 26708 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ โ โ) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
54 | 53 | nnzd 12527 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โค) |
55 | | prmz 16552 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โ ๐ โ
โค) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โค) |
57 | | peano2zm 12547 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โ 1) โ โค) |
59 | 53 | nnred 12169 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
60 | 58 | zred 12608 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โ 1) โ โ) |
61 | | prmuz2 16573 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
62 | 49, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ
(โคโฅโ2)) |
63 | | uz2m1nn 12849 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ
(โคโฅโ2) โ (๐ โ 1) โ โ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โ 1) โ โ) |
65 | 64 | nnrpd 12956 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โ 1) โ
โ+) |
66 | | rphalflt 12945 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ 1) โ
โ+ โ ((๐ โ 1) / 2) < (๐ โ 1)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ โ 1) / 2) < (๐ โ 1)) |
68 | 5, 67 | eqbrtrid 5141 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ < (๐ โ 1)) |
69 | 59, 60, 68 | ltled 11304 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โค (๐ โ 1)) |
70 | | eluz2 12770 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ 1) โ
(โคโฅโ๐) โ (๐ โ โค โง (๐ โ 1) โ โค โง ๐ โค (๐ โ 1))) |
71 | 54, 58, 69, 70 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โ 1) โ
(โคโฅโ๐)) |
72 | | fzss2 13482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ 1) โ
(โคโฅโ๐) โ (1...๐) โ (1...(๐ โ 1))) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (1...๐) โ (1...(๐ โ 1))) |
74 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฆ โ (1...๐)) |
75 | 73, 74 | sseldd 3946 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฆ โ (1...(๐ โ 1))) |
76 | | fzm1ndvds 16205 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ฆ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐ฆ) |
77 | 51, 75, 76 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ยฌ ๐ โฅ ๐ฆ) |
78 | 4 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ ๐) |
79 | 2 | eldifad 3923 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ โ) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
81 | | prmrp 16589 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
82 | 49, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ gcd ๐) = 1 โ ๐ โ ๐)) |
83 | 78, 82 | mpbird 257 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ gcd ๐) = 1) |
84 | | prmz 16552 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โค) |
85 | 80, 84 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โค) |
86 | | elfzelz 13442 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ (1...๐) โ ๐ฆ โ โค) |
87 | 86 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฆ โ โค) |
88 | | coprmdvds 16530 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง ๐ โ โค โง ๐ฆ โ โค) โ ((๐ โฅ (๐ ยท ๐ฆ) โง (๐ gcd ๐) = 1) โ ๐ โฅ ๐ฆ)) |
89 | 56, 85, 87, 88 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ โฅ (๐ ยท ๐ฆ) โง (๐ gcd ๐) = 1) โ ๐ โฅ ๐ฆ)) |
90 | 83, 89 | mpan2d 693 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โฅ (๐ ยท ๐ฆ) โ ๐ โฅ ๐ฆ)) |
91 | 77, 90 | mtod 197 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ยฌ ๐ โฅ (๐ ยท ๐ฆ)) |
92 | | prmnn 16551 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โ) |
93 | 80, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
94 | 93 | nncnd 12170 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โ โ) |
95 | | elfznn 13471 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ (1...๐) โ ๐ฆ โ โ) |
96 | 95 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฆ โ โ) |
97 | 96 | nncnd 12170 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฆ โ โ) |
98 | 94, 97 | mulcomd 11177 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ ยท ๐ฆ) = (๐ฆ ยท ๐)) |
99 | 98 | breq2d 5118 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ โฅ (๐ ยท ๐ฆ) โ ๐ โฅ (๐ฆ ยท ๐))) |
100 | 91, 99 | mtbid 324 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ยฌ ๐ โฅ (๐ฆ ยท ๐)) |
101 | | elfzelz 13442 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โค) |
102 | 101 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฅ โ โค) |
103 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ฅ ยท ๐)) |
104 | 102, 56, 103 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ โฅ (๐ฅ ยท ๐)) |
105 | | breq2 5110 |
. . . . . . . . . . . . . 14
โข ((๐ฅ ยท ๐) = (๐ฆ ยท ๐) โ (๐ โฅ (๐ฅ ยท ๐) โ ๐ โฅ (๐ฆ ยท ๐))) |
106 | 104, 105 | syl5ibcom 244 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ฅ ยท ๐) = (๐ฆ ยท ๐) โ ๐ โฅ (๐ฆ ยท ๐))) |
107 | 106 | necon3bd 2958 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (ยฌ ๐ โฅ (๐ฆ ยท ๐) โ (๐ฅ ยท ๐) โ (๐ฆ ยท ๐))) |
108 | 100, 107 | mpd 15 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ฅ ยท ๐) โ (๐ฆ ยท ๐)) |
109 | | elfznn 13471 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (1...๐) โ ๐ฅ โ โ) |
110 | 109 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ๐ฅ โ โ) |
111 | 110, 51 | nnmulcld 12207 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ฅ ยท ๐) โ โ) |
112 | 111 | nnred 12169 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ฅ ยท ๐) โ โ) |
113 | 96, 93 | nnmulcld 12207 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ฆ ยท ๐) โ โ) |
114 | 113 | nnred 12169 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ (๐ฆ ยท ๐) โ โ) |
115 | 112, 114 | lttri2d 11295 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ฅ ยท ๐) โ (๐ฆ ยท ๐) โ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
116 | 108, 115 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) |
117 | 116 | ex 414 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
118 | 117 | pm4.71rd 564 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ (((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)) โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))))) |
119 | | ancom 462 |
. . . . . . . 8
โข ((((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)) โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
120 | 118, 119 | bitr2di 288 |
. . . . . . 7
โข (๐ โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) โ (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)))) |
121 | 120 | opabbidv 5172 |
. . . . . 6
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))}) |
122 | | unopab 5188 |
. . . . . . 7
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))}) = {โจ๐ฅ, ๐ฆโฉ โฃ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โจ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
123 | 34 | uneq2i 4121 |
. . . . . . 7
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐) = ({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))}) |
124 | | andi 1007 |
. . . . . . . 8
โข (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โจ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
125 | 124 | opabbii 5173 |
. . . . . . 7
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} = {โจ๐ฅ, ๐ฆโฉ โฃ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โจ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
126 | 122, 123,
125 | 3eqtr4i 2775 |
. . . . . 6
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐) = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โจ (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
127 | | df-xp 5640 |
. . . . . 6
โข
((1...๐) ร
(1...๐)) = {โจ๐ฅ, ๐ฆโฉ โฃ (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))} |
128 | 121, 126,
127 | 3eqtr4g 2802 |
. . . . 5
โข (๐ โ ({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐) = ((1...๐) ร (1...๐))) |
129 | 128 | fveq2d 6847 |
. . . 4
โข (๐ โ
(โฏโ({โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐)) = (โฏโ((1...๐) ร (1...๐)))) |
130 | | inopab 5786 |
. . . . . . 7
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))}) = {โจ๐ฅ, ๐ฆโฉ โฃ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โง ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
131 | 34 | ineq2i 4170 |
. . . . . . 7
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ ๐) = ({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))}) |
132 | | anandi 675 |
. . . . . . . 8
โข (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) โ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โง ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
133 | 132 | opabbii 5173 |
. . . . . . 7
โข
{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} = {โจ๐ฅ, ๐ฆโฉ โฃ (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐)) โง ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
134 | 130, 131,
133 | 3eqtr4i 2775 |
. . . . . 6
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ ๐) = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} |
135 | | ltnsym2 11255 |
. . . . . . . . . . . 12
โข (((๐ฅ ยท ๐) โ โ โง (๐ฆ ยท ๐) โ โ) โ ยฌ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) |
136 | 112, 114,
135 | syl2anc 585 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐))) โ ยฌ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) |
137 | 136 | ex 414 |
. . . . . . . . . 10
โข (๐ โ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ ยฌ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
138 | | imnan 401 |
. . . . . . . . . 10
โข (((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โ ยฌ ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) โ ยฌ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
139 | 137, 138 | sylib 217 |
. . . . . . . . 9
โข (๐ โ ยฌ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
140 | 139 | nexdv 1940 |
. . . . . . . 8
โข (๐ โ ยฌ โ๐ฆ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
141 | 140 | nexdv 1940 |
. . . . . . 7
โข (๐ โ ยฌ โ๐ฅโ๐ฆ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
142 | | opabn0 5511 |
. . . . . . . 8
โข
({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} โ โ
โ โ๐ฅโ๐ฆ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))) |
143 | 142 | necon1bbii 2994 |
. . . . . . 7
โข (ยฌ
โ๐ฅโ๐ฆ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐))) โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} = โ
) |
144 | 141, 143 | sylib 217 |
. . . . . 6
โข (๐ โ {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง ((๐ฅ ยท ๐) < (๐ฆ ยท ๐) โง (๐ฆ ยท ๐) < (๐ฅ ยท ๐)))} = โ
) |
145 | 134, 144 | eqtrid 2789 |
. . . . 5
โข (๐ โ ({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ ๐) = โ
) |
146 | | hashun 14283 |
. . . . 5
โข
(({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โ Fin โง ๐ โ Fin โง ({โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โฉ ๐) = โ
) โ
(โฏโ({โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐)) = ((โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) + (โฏโ๐))) |
147 | 25, 42, 145, 146 | syl3anc 1372 |
. . . 4
โข (๐ โ
(โฏโ({โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))} โช ๐)) = ((โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) + (โฏโ๐))) |
148 | | hashxp 14335 |
. . . . . 6
โข
(((1...๐) โ Fin
โง (1...๐) โ Fin)
โ (โฏโ((1...๐) ร (1...๐))) = ((โฏโ(1...๐)) ยท (โฏโ(1...๐)))) |
149 | 19, 20, 148 | syl2anc 585 |
. . . . 5
โข (๐ โ (โฏโ((1...๐) ร (1...๐))) = ((โฏโ(1...๐)) ยท (โฏโ(1...๐)))) |
150 | 2, 6 | gausslemma2dlem0b 26708 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
151 | 150 | nnnn0d 12474 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
152 | | hashfz1 14247 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
153 | 151, 152 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโ(1...๐)) = ๐) |
154 | 52 | nnnn0d 12474 |
. . . . . . 7
โข (๐ โ ๐ โ
โ0) |
155 | | hashfz1 14247 |
. . . . . . 7
โข (๐ โ โ0
โ (โฏโ(1...๐)) = ๐) |
156 | 154, 155 | syl 17 |
. . . . . 6
โข (๐ โ (โฏโ(1...๐)) = ๐) |
157 | 153, 156 | oveq12d 7376 |
. . . . 5
โข (๐ โ ((โฏโ(1...๐)) ยท
(โฏโ(1...๐))) =
(๐ ยท ๐)) |
158 | 149, 157 | eqtrd 2777 |
. . . 4
โข (๐ โ (โฏโ((1...๐) ร (1...๐))) = (๐ ยท ๐)) |
159 | 129, 147,
158 | 3eqtr3d 2785 |
. . 3
โข (๐ โ
((โฏโ{โจ๐ฅ,
๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) + (โฏโ๐)) = (๐ ยท ๐)) |
160 | 159 | oveq2d 7374 |
. 2
โข (๐ โ
(-1โ((โฏโ{โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ (1...๐) โง ๐ฆ โ (1...๐)) โง (๐ฅ ยท ๐) < (๐ฆ ยท ๐))}) + (โฏโ๐))) = (-1โ(๐ ยท ๐))) |
161 | 36, 47, 160 | 3eqtr2d 2783 |
1
โข (๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(๐ ยท ๐))) |