Step | Hyp | Ref
| Expression |
1 | | oveq1 7411 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด โโ
๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) |
2 | 1, 1 | oveq12d 7422 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) = ((if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) |
3 | | id 22 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ๐ด = if(๐ด โ โ, ๐ด, 0โ)) |
4 | 3, 3 | oveq12d 7422 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด
ยทih ๐ด) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ))) |
5 | 4 | oveq1d 7419 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) = ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต))) |
6 | | oveq1 7411 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด
ยทih ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต)) |
7 | | oveq2 7412 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ต
ยทih ๐ด) = (๐ต ยทih
if(๐ด โ โ, ๐ด,
0โ))) |
8 | 6, 7 | oveq12d 7422 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐ด
ยทih ๐ต) + (๐ต ยทih ๐ด)) = ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด,
0โ)))) |
9 | 5, 8 | oveq12d 7422 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐ด
ยทih ๐ด) + (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) = (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด,
0โ))))) |
10 | 2, 9 | eqeq12d 2749 |
. 2
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด))) โ ((if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) = (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด,
0โ)))))) |
11 | | oveq2 7412 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))) |
12 | 11, 11 | oveq12d 7422 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) = ((if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) |
13 | | id 22 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ๐ต = if(๐ต โ โ, ๐ต, 0โ)) |
14 | 13, 13 | oveq12d 7422 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐ต
ยทih ๐ต) = (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) |
15 | 14 | oveq2d 7420 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต)) = ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)))) |
16 | | oveq2 7412 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) |
17 | | oveq1 7411 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐ต
ยทih if(๐ด โ โ, ๐ด, 0โ)) = (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ))) |
18 | 16, 17 | oveq12d 7422 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด, 0โ))) =
((if(๐ด โ โ,
๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)))) |
19 | 15, 18 | oveq12d 7422 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด, 0โ)))) =
(((if(๐ด โ โ,
๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ))))) |
20 | 12, 19 | eqeq12d 2749 |
. 2
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) = (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (๐ต
ยทih ๐ต)) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih ๐ต) + (๐ต ยทih
if(๐ด โ โ, ๐ด, 0โ))))
โ ((if(๐ด โ
โ, ๐ด,
0โ) โโ if(๐ต โ โ, ๐ต, 0โ))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))) = (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ด โ โ, ๐ด,
0โ)))))) |
21 | | ifhvhv0 30253 |
. . 3
โข if(๐ด โ โ, ๐ด, 0โ) โ
โ |
22 | | ifhvhv0 30253 |
. . 3
โข if(๐ต โ โ, ๐ต, 0โ) โ
โ |
23 | 21, 22, 21, 22 | normlem9 30349 |
. 2
โข
((if(๐ด โ
โ, ๐ด,
0โ) โโ if(๐ต โ โ, ๐ต, 0โ))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))) = (((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ))) โ ((if(๐ด โ โ, ๐ด, 0โ)
ยทih if(๐ต โ โ, ๐ต, 0โ)) + (if(๐ต โ โ, ๐ต, 0โ)
ยทih if(๐ด โ โ, ๐ด, 0โ)))) |
24 | 10, 20, 23 | dedth2h 4586 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โโ
๐ต)
ยทih (๐ด โโ ๐ต)) = (((๐ด ยทih ๐ด) + (๐ต ยทih ๐ต)) โ ((๐ด ยทih ๐ต) + (๐ต ยทih ๐ด)))) |