Step | Hyp | Ref
| Expression |
1 | | 2sq.1 |
. . . 4
โข ๐ = ran (๐ค โ โค[i] โฆ ((absโ๐ค)โ2)) |
2 | 1 | 2sqlem1 26768 |
. . 3
โข (๐ด โ ๐ โ โ๐ง โ โค[i] ๐ด = ((absโ๐ง)โ2)) |
3 | | elgz 16804 |
. . . . . . 7
โข (๐ง โ โค[i] โ (๐ง โ โ โง
(โโ๐ง) โ
โค โง (โโ๐ง) โ โค)) |
4 | 3 | simp2bi 1147 |
. . . . . 6
โข (๐ง โ โค[i] โ
(โโ๐ง) โ
โค) |
5 | 3 | simp3bi 1148 |
. . . . . 6
โข (๐ง โ โค[i] โ
(โโ๐ง) โ
โค) |
6 | | gzcn 16805 |
. . . . . . 7
โข (๐ง โ โค[i] โ ๐ง โ
โ) |
7 | 6 | absvalsq2d 15329 |
. . . . . 6
โข (๐ง โ โค[i] โ
((absโ๐ง)โ2) =
(((โโ๐ง)โ2)
+ ((โโ๐ง)โ2))) |
8 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ฅ = (โโ๐ง) โ (๐ฅโ2) = ((โโ๐ง)โ2)) |
9 | 8 | oveq1d 7373 |
. . . . . . . 8
โข (๐ฅ = (โโ๐ง) โ ((๐ฅโ2) + (๐ฆโ2)) = (((โโ๐ง)โ2) + (๐ฆโ2))) |
10 | 9 | eqeq2d 2748 |
. . . . . . 7
โข (๐ฅ = (โโ๐ง) โ (((absโ๐ง)โ2) = ((๐ฅโ2) + (๐ฆโ2)) โ ((absโ๐ง)โ2) =
(((โโ๐ง)โ2)
+ (๐ฆโ2)))) |
11 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ฆ = (โโ๐ง) โ (๐ฆโ2) = ((โโ๐ง)โ2)) |
12 | 11 | oveq2d 7374 |
. . . . . . . 8
โข (๐ฆ = (โโ๐ง) โ (((โโ๐ง)โ2) + (๐ฆโ2)) = (((โโ๐ง)โ2) +
((โโ๐ง)โ2))) |
13 | 12 | eqeq2d 2748 |
. . . . . . 7
โข (๐ฆ = (โโ๐ง) โ (((absโ๐ง)โ2) =
(((โโ๐ง)โ2)
+ (๐ฆโ2)) โ
((absโ๐ง)โ2) =
(((โโ๐ง)โ2)
+ ((โโ๐ง)โ2)))) |
14 | 10, 13 | rspc2ev 3593 |
. . . . . 6
โข
(((โโ๐ง)
โ โค โง (โโ๐ง) โ โค โง ((absโ๐ง)โ2) =
(((โโ๐ง)โ2)
+ ((โโ๐ง)โ2))) โ โ๐ฅ โ โค โ๐ฆ โ โค ((absโ๐ง)โ2) = ((๐ฅโ2) + (๐ฆโ2))) |
15 | 4, 5, 7, 14 | syl3anc 1372 |
. . . . 5
โข (๐ง โ โค[i] โ
โ๐ฅ โ โค
โ๐ฆ โ โค
((absโ๐ง)โ2) =
((๐ฅโ2) + (๐ฆโ2))) |
16 | | eqeq1 2741 |
. . . . . 6
โข (๐ด = ((absโ๐ง)โ2) โ (๐ด = ((๐ฅโ2) + (๐ฆโ2)) โ ((absโ๐ง)โ2) = ((๐ฅโ2) + (๐ฆโ2)))) |
17 | 16 | 2rexbidv 3214 |
. . . . 5
โข (๐ด = ((absโ๐ง)โ2) โ (โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2)) โ โ๐ฅ โ โค โ๐ฆ โ โค ((absโ๐ง)โ2) = ((๐ฅโ2) + (๐ฆโ2)))) |
18 | 15, 17 | syl5ibrcom 247 |
. . . 4
โข (๐ง โ โค[i] โ (๐ด = ((absโ๐ง)โ2) โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2)))) |
19 | 18 | rexlimiv 3146 |
. . 3
โข
(โ๐ง โ
โค[i] ๐ด =
((absโ๐ง)โ2)
โ โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ด = ((๐ฅโ2) + (๐ฆโ2))) |
20 | 2, 19 | sylbi 216 |
. 2
โข (๐ด โ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2))) |
21 | | gzreim 16812 |
. . . . . 6
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ + (i ยท ๐ฆ)) โ
โค[i]) |
22 | | zcn 12505 |
. . . . . . . . 9
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
23 | | ax-icn 11111 |
. . . . . . . . . 10
โข i โ
โ |
24 | | zcn 12505 |
. . . . . . . . . 10
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
25 | | mulcl 11136 |
. . . . . . . . . 10
โข ((i
โ โ โง ๐ฆ
โ โ) โ (i ยท ๐ฆ) โ โ) |
26 | 23, 24, 25 | sylancr 588 |
. . . . . . . . 9
โข (๐ฆ โ โค โ (i
ยท ๐ฆ) โ
โ) |
27 | | addcl 11134 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง (i
ยท ๐ฆ) โ โ)
โ (๐ฅ + (i ยท
๐ฆ)) โ
โ) |
28 | 22, 26, 27 | syl2an 597 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ + (i ยท ๐ฆ)) โ
โ) |
29 | 28 | absvalsq2d 15329 |
. . . . . . 7
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
((absโ(๐ฅ + (i
ยท ๐ฆ)))โ2) =
(((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2) +
((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2))) |
30 | | zre 12504 |
. . . . . . . . . 10
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
31 | | zre 12504 |
. . . . . . . . . 10
โข (๐ฆ โ โค โ ๐ฆ โ
โ) |
32 | | crre 15000 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(โโ(๐ฅ + (i
ยท ๐ฆ))) = ๐ฅ) |
33 | 30, 31, 32 | syl2an 597 |
. . . . . . . . 9
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
(โโ(๐ฅ + (i
ยท ๐ฆ))) = ๐ฅ) |
34 | 33 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2) =
(๐ฅโ2)) |
35 | | crim 15001 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(โโ(๐ฅ + (i
ยท ๐ฆ))) = ๐ฆ) |
36 | 30, 31, 35 | syl2an 597 |
. . . . . . . . 9
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
(โโ(๐ฅ + (i
ยท ๐ฆ))) = ๐ฆ) |
37 | 36 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2) =
(๐ฆโ2)) |
38 | 34, 37 | oveq12d 7376 |
. . . . . . 7
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
(((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2) +
((โโ(๐ฅ + (i
ยท ๐ฆ)))โ2)) =
((๐ฅโ2) + (๐ฆโ2))) |
39 | 29, 38 | eqtr2d 2778 |
. . . . . 6
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅโ2) + (๐ฆโ2)) = ((absโ(๐ฅ + (i ยท ๐ฆ)))โ2)) |
40 | | fveq2 6843 |
. . . . . . . 8
โข (๐ง = (๐ฅ + (i ยท ๐ฆ)) โ (absโ๐ง) = (absโ(๐ฅ + (i ยท ๐ฆ)))) |
41 | 40 | oveq1d 7373 |
. . . . . . 7
โข (๐ง = (๐ฅ + (i ยท ๐ฆ)) โ ((absโ๐ง)โ2) = ((absโ(๐ฅ + (i ยท ๐ฆ)))โ2)) |
42 | 41 | rspceeqv 3596 |
. . . . . 6
โข (((๐ฅ + (i ยท ๐ฆ)) โ โค[i] โง
((๐ฅโ2) + (๐ฆโ2)) = ((absโ(๐ฅ + (i ยท ๐ฆ)))โ2)) โ โ๐ง โ โค[i] ((๐ฅโ2) + (๐ฆโ2)) = ((absโ๐ง)โ2)) |
43 | 21, 39, 42 | syl2anc 585 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ
โ๐ง โ โค[i]
((๐ฅโ2) + (๐ฆโ2)) = ((absโ๐ง)โ2)) |
44 | 1 | 2sqlem1 26768 |
. . . . 5
โข (((๐ฅโ2) + (๐ฆโ2)) โ ๐ โ โ๐ง โ โค[i] ((๐ฅโ2) + (๐ฆโ2)) = ((absโ๐ง)โ2)) |
45 | 43, 44 | sylibr 233 |
. . . 4
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ ((๐ฅโ2) + (๐ฆโ2)) โ ๐) |
46 | | eleq1 2826 |
. . . 4
โข (๐ด = ((๐ฅโ2) + (๐ฆโ2)) โ (๐ด โ ๐ โ ((๐ฅโ2) + (๐ฆโ2)) โ ๐)) |
47 | 45, 46 | syl5ibrcom 247 |
. . 3
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ด = ((๐ฅโ2) + (๐ฆโ2)) โ ๐ด โ ๐)) |
48 | 47 | rexlimivv 3197 |
. 2
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โค ๐ด = ((๐ฅโ2) + (๐ฆโ2)) โ ๐ด โ ๐) |
49 | 20, 48 | impbii 208 |
1
โข (๐ด โ ๐ โ โ๐ฅ โ โค โ๐ฆ โ โค ๐ด = ((๐ฅโ2) + (๐ฆโ2))) |