Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ๐ด) = (๐โif(๐ด โ โ, ๐ด, 0โ))) |
2 | 1 | oveq1d 7424 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ๐ด) ยทih ๐ต) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต)) |
3 | | fvoveq1 7432 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ(๐ด +โ ๐ต)) = (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))) |
4 | | oveq1 7416 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด +โ ๐ต) = (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) |
5 | 3, 4 | oveq12d 7427 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))) |
6 | | fvoveq1 7432 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ(๐ด โโ ๐ต)) = (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) |
7 | | oveq1 7416 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด โโ
๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) |
8 | 6, 7 | oveq12d 7427 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต)) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) |
9 | 5, 8 | oveq12d 7427 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) = (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)))) |
10 | | fvoveq1 7432 |
. . . . . . . 8
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ(๐ด +โ (i
ยทโ ๐ต))) = (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต)))) |
11 | | oveq1 7416 |
. . . . . . . 8
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด +โ (i
ยทโ ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) |
12 | 10, 11 | oveq12d 7427 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต)))) |
13 | | fvoveq1 7432 |
. . . . . . . 8
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐โ(๐ด โโ (i
ยทโ ๐ต))) = (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))) |
14 | | oveq1 7416 |
. . . . . . . 8
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (๐ด โโ (i
ยทโ ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))) |
15 | 13, 14 | oveq12d 7427 |
. . . . . . 7
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))) |
16 | 12, 15 | oveq12d 7427 |
. . . . . 6
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))) = (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))))) |
17 | 16 | oveq2d 7425 |
. . . . 5
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (i ยท
(((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต))))) = (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) |
18 | 9, 17 | oveq12d 7427 |
. . . 4
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ ((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) = ((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))))))) |
19 | 18 | oveq1d 7424 |
. . 3
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) / 4)) |
20 | 2, 19 | eqeq12d 2749 |
. 2
โข (๐ด = if(๐ด โ โ, ๐ด, 0โ) โ (((๐โ๐ด) ยทih ๐ต) = (((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4) โ ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) / 4))) |
21 | | oveq2 7417 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) = ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ))) |
22 | | oveq2 7417 |
. . . . . . . 8
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
+โ ๐ต) =
(if(๐ด โ โ, ๐ด, 0โ)
+โ if(๐ต
โ โ, ๐ต,
0โ))) |
23 | 22 | fveq2d 6896 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) = (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))) |
24 | 23, 22 | oveq12d 7427 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต,
0โ)))) |
25 | | oveq2 7417 |
. . . . . . . 8
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต) = (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))) |
26 | 25 | fveq2d 6896 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) = (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) |
27 | 26, 25 | oveq12d 7427 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) |
28 | 24, 27 | oveq12d 7427 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) = (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ))))) |
29 | | oveq2 7417 |
. . . . . . . . . 10
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (i
ยทโ ๐ต) = (i ยทโ
if(๐ต โ โ, ๐ต,
0โ))) |
30 | 29 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) |
31 | 30 | fveq2d 6896 |
. . . . . . . 8
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) = (๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ))))) |
32 | 31, 30 | oveq12d 7427 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ))))) |
33 | 29 | oveq2d 7425 |
. . . . . . . . 9
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)) = (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ)))) |
34 | 33 | fveq2d 6896 |
. . . . . . . 8
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))) = (๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ))))) |
35 | 34, 33 | oveq12d 7427 |
. . . . . . 7
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))) = ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ))))) |
36 | 32, 35 | oveq12d 7427 |
. . . . . 6
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))) = (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ)))))) |
37 | 36 | oveq2d 7425 |
. . . . 5
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (i ยท
(((๐โ(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต))))) = (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ))))))) |
38 | 28, 37 | oveq12d 7427 |
. . . 4
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ ((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) = ((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) + (i ยท
(((๐โ(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต,
0โ)))))))) |
39 | 38 | oveq1d 7424 |
. . 3
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) / 4) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) + (i ยท
(((๐โ(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))))) /
4)) |
40 | 21, 39 | eqeq12d 2749 |
. 2
โข (๐ต = if(๐ต โ โ, ๐ต, 0โ) โ (((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih ๐ต) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
๐ต)) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต)) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
โโ ๐ต))) + (i ยท (((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ ๐ต))) ยทih
(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ ๐ต))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ ๐ต)))))) / 4) โ ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) + (i ยท
(((๐โ(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))))) /
4))) |
41 | | lnopeq0.1 |
. . 3
โข ๐ โ LinOp |
42 | | ifhvhv0 30275 |
. . 3
โข if(๐ด โ โ, ๐ด, 0โ) โ
โ |
43 | | ifhvhv0 30275 |
. . 3
โข if(๐ต โ โ, ๐ต, 0โ) โ
โ |
44 | 41, 42, 43 | lnopeq0lem1 31258 |
. 2
โข ((๐โif(๐ด โ โ, ๐ด, 0โ))
ยทih if(๐ต โ โ, ๐ต, 0โ)) = (((((๐โ(if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
if(๐ต โ โ, ๐ต, 0โ)))
โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ if(๐ต โ โ, ๐ต, 0โ)))) + (i ยท
(((๐โ(if(๐ด โ โ, ๐ด, 0โ)
+โ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ) +โ
(i ยทโ if(๐ต โ โ, ๐ต, 0โ)))) โ ((๐โ(if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))
ยทih (if(๐ด โ โ, ๐ด, 0โ)
โโ (i ยทโ if(๐ต โ โ, ๐ต, 0โ))))))) /
4) |
45 | 20, 40, 44 | dedth2h 4588 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐โ๐ด) ยทih ๐ต) = (((((๐โ(๐ด +โ ๐ต)) ยทih
(๐ด +โ
๐ต)) โ ((๐โ(๐ด โโ ๐ต))
ยทih (๐ด โโ ๐ต))) + (i ยท (((๐โ(๐ด +โ (i
ยทโ ๐ต))) ยทih
(๐ด +โ (i
ยทโ ๐ต))) โ ((๐โ(๐ด โโ (i
ยทโ ๐ต))) ยทih
(๐ด
โโ (i ยทโ ๐ต)))))) / 4)) |