Step | Hyp | Ref
| Expression |
1 | | 2sq.1 |
. . 3
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
2 | 1 | 2sqlem1 26768 |
. 2
โข (๐ด โ ๐ โ โ๐ฅ โ โค[i] ๐ด = ((absโ๐ฅ)โ2)) |
3 | 1 | 2sqlem1 26768 |
. 2
โข (๐ต โ ๐ โ โ๐ฆ โ โค[i] ๐ต = ((absโ๐ฆ)โ2)) |
4 | | reeanv 3218 |
. . 3
โข
(โ๐ฅ โ
โค[i] โ๐ฆ โ
โค[i] (๐ด =
((absโ๐ฅ)โ2)
โง ๐ต = ((absโ๐ฆ)โ2)) โ (โ๐ฅ โ โค[i] ๐ด = ((absโ๐ฅ)โ2) โง โ๐ฆ โ โค[i] ๐ต = ((absโ๐ฆ)โ2))) |
5 | | gzmulcl 16811 |
. . . . . . 7
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
(๐ฅ ยท ๐ฆ) โ
โค[i]) |
6 | | gzcn 16805 |
. . . . . . . . . 10
โข (๐ฅ โ โค[i] โ ๐ฅ โ
โ) |
7 | | gzcn 16805 |
. . . . . . . . . 10
โข (๐ฆ โ โค[i] โ ๐ฆ โ
โ) |
8 | | absmul 15180 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(absโ(๐ฅ ยท
๐ฆ)) = ((absโ๐ฅ) ยท (absโ๐ฆ))) |
9 | 6, 7, 8 | syl2an 597 |
. . . . . . . . 9
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
(absโ(๐ฅ ยท
๐ฆ)) = ((absโ๐ฅ) ยท (absโ๐ฆ))) |
10 | 9 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
((absโ(๐ฅ ยท
๐ฆ))โ2) =
(((absโ๐ฅ) ยท
(absโ๐ฆ))โ2)) |
11 | 6 | abscld 15322 |
. . . . . . . . . 10
โข (๐ฅ โ โค[i] โ
(absโ๐ฅ) โ
โ) |
12 | 11 | recnd 11184 |
. . . . . . . . 9
โข (๐ฅ โ โค[i] โ
(absโ๐ฅ) โ
โ) |
13 | 7 | abscld 15322 |
. . . . . . . . . 10
โข (๐ฆ โ โค[i] โ
(absโ๐ฆ) โ
โ) |
14 | 13 | recnd 11184 |
. . . . . . . . 9
โข (๐ฆ โ โค[i] โ
(absโ๐ฆ) โ
โ) |
15 | | sqmul 14025 |
. . . . . . . . 9
โข
(((absโ๐ฅ)
โ โ โง (absโ๐ฆ) โ โ) โ (((absโ๐ฅ) ยท (absโ๐ฆ))โ2) = (((absโ๐ฅ)โ2) ยท
((absโ๐ฆ)โ2))) |
16 | 12, 14, 15 | syl2an 597 |
. . . . . . . 8
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
(((absโ๐ฅ) ยท
(absโ๐ฆ))โ2) =
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2))) |
17 | 10, 16 | eqtr2d 2778 |
. . . . . . 7
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2)) = ((absโ(๐ฅ ยท ๐ฆ))โ2)) |
18 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ง = (๐ฅ ยท ๐ฆ) โ (absโ๐ง) = (absโ(๐ฅ ยท ๐ฆ))) |
19 | 18 | oveq1d 7373 |
. . . . . . . 8
โข (๐ง = (๐ฅ ยท ๐ฆ) โ ((absโ๐ง)โ2) = ((absโ(๐ฅ ยท ๐ฆ))โ2)) |
20 | 19 | rspceeqv 3596 |
. . . . . . 7
โข (((๐ฅ ยท ๐ฆ) โ โค[i] โง (((absโ๐ฅ)โ2) ยท
((absโ๐ฆ)โ2)) =
((absโ(๐ฅ ยท
๐ฆ))โ2)) โ
โ๐ง โ โค[i]
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2)) = ((absโ๐ง)โ2)) |
21 | 5, 17, 20 | syl2anc 585 |
. . . . . 6
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
โ๐ง โ โค[i]
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2)) = ((absโ๐ง)โ2)) |
22 | 1 | 2sqlem1 26768 |
. . . . . 6
โข
((((absโ๐ฅ)โ2) ยท ((absโ๐ฆ)โ2)) โ ๐ โ โ๐ง โ โค[i]
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2)) = ((absโ๐ง)โ2)) |
23 | 21, 22 | sylibr 233 |
. . . . 5
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
(((absโ๐ฅ)โ2)
ยท ((absโ๐ฆ)โ2)) โ ๐) |
24 | | oveq12 7367 |
. . . . . 6
โข ((๐ด = ((absโ๐ฅ)โ2) โง ๐ต = ((absโ๐ฆ)โ2)) โ (๐ด ยท ๐ต) = (((absโ๐ฅ)โ2) ยท ((absโ๐ฆ)โ2))) |
25 | 24 | eleq1d 2823 |
. . . . 5
โข ((๐ด = ((absโ๐ฅ)โ2) โง ๐ต = ((absโ๐ฆ)โ2)) โ ((๐ด ยท ๐ต) โ ๐ โ (((absโ๐ฅ)โ2) ยท ((absโ๐ฆ)โ2)) โ ๐)) |
26 | 23, 25 | syl5ibrcom 247 |
. . . 4
โข ((๐ฅ โ โค[i] โง ๐ฆ โ โค[i]) โ
((๐ด = ((absโ๐ฅ)โ2) โง ๐ต = ((absโ๐ฆ)โ2)) โ (๐ด ยท ๐ต) โ ๐)) |
27 | 26 | rexlimivv 3197 |
. . 3
โข
(โ๐ฅ โ
โค[i] โ๐ฆ โ
โค[i] (๐ด =
((absโ๐ฅ)โ2)
โง ๐ต = ((absโ๐ฆ)โ2)) โ (๐ด ยท ๐ต) โ ๐) |
28 | 4, 27 | sylbir 234 |
. 2
โข
((โ๐ฅ โ
โค[i] ๐ด =
((absโ๐ฅ)โ2)
โง โ๐ฆ โ
โค[i] ๐ต =
((absโ๐ฆ)โ2))
โ (๐ด ยท ๐ต) โ ๐) |
29 | 2, 3, 28 | syl2anb 599 |
1
โข ((๐ด โ ๐ โง ๐ต โ ๐) โ (๐ด ยท ๐ต) โ ๐) |