Step | Hyp | Ref
| Expression |
1 | | 4sq.1 |
. . . 4
โข ๐ = {๐ โฃ โ๐ฅ โ โค โ๐ฆ โ โค โ๐ง โ โค โ๐ค โ โค ๐ = (((๐ฅโ2) + (๐ฆโ2)) + ((๐งโ2) + (๐คโ2)))} |
2 | 1 | 4sqlem2 12353 |
. . 3
โข (๐ด โ ๐ โ โ๐ โ โค โ๐ โ โค โ๐ โ โค โ๐ โ โค ๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
3 | | gzreim 12343 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (i ยท ๐)) โ
โค[i]) |
4 | 3 | adantr 276 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (๐ + (i ยท ๐)) โ
โค[i]) |
5 | | gzreim 12343 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (i ยท ๐)) โ
โค[i]) |
6 | 5 | adantl 277 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (๐ + (i ยท ๐)) โ
โค[i]) |
7 | | gzcn 12336 |
. . . . . . . . . . . 12
โข ((๐ + (i ยท ๐)) โ โค[i] โ
(๐ + (i ยท ๐)) โ
โ) |
8 | 3, 7 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (i ยท ๐)) โ
โ) |
9 | 8 | absvalsq2d 11159 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐ + (i
ยท ๐)))โ2) =
(((โโ(๐ + (i
ยท ๐)))โ2) +
((โโ(๐ + (i
ยท ๐)))โ2))) |
10 | | zre 9228 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
11 | | zre 9228 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
12 | | crre 10833 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
13 | 10, 11, 12 | syl2an 289 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
14 | 13 | oveq1d 5880 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ
((โโ(๐ + (i
ยท ๐)))โ2) =
(๐โ2)) |
15 | | crim 10834 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
16 | 10, 11, 15 | syl2an 289 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
17 | 16 | oveq1d 5880 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ
((โโ(๐ + (i
ยท ๐)))โ2) =
(๐โ2)) |
18 | 14, 17 | oveq12d 5883 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
(((โโ(๐ + (i
ยท ๐)))โ2) +
((โโ(๐ + (i
ยท ๐)))โ2)) =
((๐โ2) + (๐โ2))) |
19 | 9, 18 | eqtrd 2208 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐ + (i
ยท ๐)))โ2) =
((๐โ2) + (๐โ2))) |
20 | | gzcn 12336 |
. . . . . . . . . . . 12
โข ((๐ + (i ยท ๐)) โ โค[i] โ
(๐ + (i ยท ๐)) โ
โ) |
21 | 5, 20 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + (i ยท ๐)) โ
โ) |
22 | 21 | absvalsq2d 11159 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐ + (i
ยท ๐)))โ2) =
(((โโ(๐ + (i
ยท ๐)))โ2) +
((โโ(๐ + (i
ยท ๐)))โ2))) |
23 | | zre 9228 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
24 | | zre 9228 |
. . . . . . . . . . . . 13
โข (๐ โ โค โ ๐ โ
โ) |
25 | | crre 10833 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
26 | 23, 24, 25 | syl2an 289 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
27 | 26 | oveq1d 5880 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ
((โโ(๐ + (i
ยท ๐)))โ2) =
(๐โ2)) |
28 | | crim 10834 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
29 | 23, 24, 28 | syl2an 289 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โค) โ
(โโ(๐ + (i
ยท ๐))) = ๐) |
30 | 29 | oveq1d 5880 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โค) โ
((โโ(๐ + (i
ยท ๐)))โ2) =
(๐โ2)) |
31 | 27, 30 | oveq12d 5883 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โค) โ
(((โโ(๐ + (i
ยท ๐)))โ2) +
((โโ(๐ + (i
ยท ๐)))โ2)) =
((๐โ2) + (๐โ2))) |
32 | 22, 31 | eqtrd 2208 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โค) โ
((absโ(๐ + (i
ยท ๐)))โ2) =
((๐โ2) + (๐โ2))) |
33 | 19, 32 | oveqan12d 5884 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ
(((absโ(๐ + (i
ยท ๐)))โ2) +
((absโ(๐ + (i
ยท ๐)))โ2)) =
(((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2)))) |
34 | 33 | eqcomd 2181 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ
(((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ(๐ + (i ยท ๐)))โ2))) |
35 | | fveq2 5507 |
. . . . . . . . . . 11
โข (๐ข = (๐ + (i ยท ๐)) โ (absโ๐ข) = (absโ(๐ + (i ยท ๐)))) |
36 | 35 | oveq1d 5880 |
. . . . . . . . . 10
โข (๐ข = (๐ + (i ยท ๐)) โ ((absโ๐ข)โ2) = ((absโ(๐ + (i ยท ๐)))โ2)) |
37 | 36 | oveq1d 5880 |
. . . . . . . . 9
โข (๐ข = (๐ + (i ยท ๐)) โ (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ๐ฃ)โ2))) |
38 | 37 | eqeq2d 2187 |
. . . . . . . 8
โข (๐ข = (๐ + (i ยท ๐)) โ ((((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ๐ฃ)โ2)))) |
39 | | fveq2 5507 |
. . . . . . . . . . 11
โข (๐ฃ = (๐ + (i ยท ๐)) โ (absโ๐ฃ) = (absโ(๐ + (i ยท ๐)))) |
40 | 39 | oveq1d 5880 |
. . . . . . . . . 10
โข (๐ฃ = (๐ + (i ยท ๐)) โ ((absโ๐ฃ)โ2) = ((absโ(๐ + (i ยท ๐)))โ2)) |
41 | 40 | oveq2d 5881 |
. . . . . . . . 9
โข (๐ฃ = (๐ + (i ยท ๐)) โ (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ๐ฃ)โ2)) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ(๐ + (i ยท ๐)))โ2))) |
42 | 41 | eqeq2d 2187 |
. . . . . . . 8
โข (๐ฃ = (๐ + (i ยท ๐)) โ ((((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ๐ฃ)โ2)) โ (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ(๐ + (i ยท ๐)))โ2)))) |
43 | 38, 42 | rspc2ev 2854 |
. . . . . . 7
โข (((๐ + (i ยท ๐)) โ โค[i] โง
(๐ + (i ยท ๐)) โ โค[i] โง
(((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ(๐ + (i ยท ๐)))โ2) + ((absโ(๐ + (i ยท ๐)))โ2))) โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2))) |
44 | 4, 6, 34, 43 | syl3anc 1238 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ
โ๐ข โ โค[i]
โ๐ฃ โ โค[i]
(((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2))) |
45 | | eqeq1 2182 |
. . . . . . 7
โข (๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ (๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)))) |
46 | 45 | 2rexbidv 2500 |
. . . . . 6
โข (๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ (โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)))) |
47 | 44, 46 | syl5ibrcom 157 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โค) โง (๐ โ โค โง ๐ โ โค)) โ (๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)))) |
48 | 47 | rexlimdvva 2600 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ
(โ๐ โ โค
โ๐ โ โค
๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)))) |
49 | 48 | rexlimivv 2598 |
. . 3
โข
(โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค โ๐ โ
โค ๐ด = (((๐โ2) + (๐โ2)) + ((๐โ2) + (๐โ2))) โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2))) |
50 | 2, 49 | sylbi 121 |
. 2
โข (๐ด โ ๐ โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2))) |
51 | 1 | 4sqlem4a 12355 |
. . . 4
โข ((๐ข โ โค[i] โง ๐ฃ โ โค[i]) โ
(((absโ๐ข)โ2) +
((absโ๐ฃ)โ2))
โ ๐) |
52 | | eleq1a 2247 |
. . . 4
โข
((((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ ๐ โ (๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ ๐ด โ ๐)) |
53 | 51, 52 | syl 14 |
. . 3
โข ((๐ข โ โค[i] โง ๐ฃ โ โค[i]) โ
(๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2)) โ ๐ด โ ๐)) |
54 | 53 | rexlimivv 2598 |
. 2
โข
(โ๐ข โ
โค[i] โ๐ฃ โ
โค[i] ๐ด =
(((absโ๐ข)โ2) +
((absโ๐ฃ)โ2))
โ ๐ด โ ๐) |
55 | 50, 54 | impbii 126 |
1
โข (๐ด โ ๐ โ โ๐ข โ โค[i] โ๐ฃ โ โค[i] ๐ด = (((absโ๐ข)โ2) + ((absโ๐ฃ)โ2))) |