Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7385 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
(normโโ(๐ด โโ ๐ต)) =
(normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) |
2 | 1 | oveq1d 7377 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
((normโโ(๐ด โโ ๐ต))โ2) =
((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2)) |
3 | | fvoveq1 7385 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
(normโโ(๐ด +โ ๐ต)) =
(normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))) |
4 | 3 | oveq1d 7377 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
((normโโ(๐ด +โ ๐ต))โ2) =
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2)) |
5 | 2, 4 | oveq12d 7380 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
(((normโโ(๐ด โโ ๐ต))โ2) +
((normโโ(๐ด +โ ๐ต))โ2)) =
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2))) |
6 | | fveq2 6847 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
(normโโ๐ด) = (normโโif(๐ด โ โ, ๐ด,
0โ))) |
7 | 6 | oveq1d 7377 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
((normโโ๐ด)โ2) =
((normโโif(๐ด โ โ, ๐ด,
0โ))โ2)) |
8 | 7 | oveq2d 7378 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (2 ยท
((normโโ๐ด)โ2)) = (2 ยท
((normโโif(๐ด โ โ, ๐ด,
0โ))โ2))) |
9 | 8 | oveq1d 7377 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((2 ยท
((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2))) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโ๐ต)โ2)))) |
10 | 5, 9 | eqeq12d 2753 |
. 2
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ
((((normโโ(๐ด โโ ๐ต))โ2) +
((normโโ(๐ด +โ ๐ต))โ2)) = ((2 ยท
((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2))) โ
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2)) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโ๐ต)โ2))))) |
11 | | oveq2 7370 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))) |
12 | 11 | fveq2d 6851 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
(normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) =
(normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) |
13 | 12 | oveq1d 7377 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2) =
((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต,
0โ)))โ2)) |
14 | | oveq2 7370 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
+โ ๐ต) =
(if(๐ด โ โ, ๐ด, 0โ)
+โ if(๐ต
โ โ, ๐ต,
0โ))) |
15 | 14 | fveq2d 6851 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
(normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) =
(normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))) |
16 | 15 | oveq1d 7377 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2) =
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))โ2)) |
17 | 13, 16 | oveq12d 7380 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2)) =
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))โ2))) |
18 | | fveq2 6847 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
(normโโ๐ต) = (normโโif(๐ต โ โ, ๐ต,
0โ))) |
19 | 18 | oveq1d 7377 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
((normโโ๐ต)โ2) =
((normโโif(๐ต โ โ, ๐ต,
0โ))โ2)) |
20 | 19 | oveq2d 7378 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (2 ยท
((normโโ๐ต)โ2)) = (2 ยท
((normโโif(๐ต โ โ, ๐ต,
0โ))โ2))) |
21 | 20 | oveq2d 7378 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโ๐ต)โ2))) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโif(๐ต โ โ, ๐ต,
0โ))โ2)))) |
22 | 17, 21 | eqeq12d 2753 |
. 2
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ
((((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))โ2)) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโ๐ต)โ2))) โ
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))โ2)) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโif(๐ต โ โ, ๐ต,
0โ))โ2))))) |
23 | | ifhvhv0 30006 |
. . 3
โข if(๐ด โ โ, ๐ด, 0โ) โ
โ |
24 | | ifhvhv0 30006 |
. . 3
โข if(๐ต โ โ, ๐ต, 0โ) โ
โ |
25 | 23, 24 | normpari 30138 |
. 2
โข
(((normโโ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))โ2) +
((normโโ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))โ2)) = ((2 ยท
((normโโif(๐ด โ โ, ๐ด, 0โ))โ2)) + (2
ยท ((normโโif(๐ต โ โ, ๐ต,
0โ))โ2))) |
26 | 10, 22, 25 | dedth2h 4550 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((normโโ(๐ด โโ ๐ต))โ2) +
((normโโ(๐ด +โ ๐ต))โ2)) = ((2 ยท
((normโโ๐ด)โ2)) + (2 ยท
((normโโ๐ต)โ2)))) |