Step | Hyp | Ref
| Expression |
1 | | fveq2 6891 |
. . . . 5
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ (โโ๐) = (โโif((๐ โ โ โง
(absโ๐) = 1), ๐, 1))) |
2 | 1 | oveq1d 7429 |
. . . 4
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ ((โโ๐) ยท (๐ด ยทih ๐ต)) = ((โโif((๐ โ โ โง
(absโ๐) = 1), ๐, 1)) ยท (๐ด
ยทih ๐ต))) |
3 | | oveq1 7421 |
. . . 4
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ (๐ ยท (๐ต ยทih ๐ด)) = (if((๐ โ โ โง (absโ๐) = 1), ๐, 1) ยท (๐ต ยทih ๐ด))) |
4 | 2, 3 | oveq12d 7432 |
. . 3
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ (((โโ๐) ยท (๐ด ยทih ๐ต)) + (๐ ยท (๐ต ยทih ๐ด))) =
(((โโif((๐
โ โ โง (absโ๐) = 1), ๐, 1)) ยท (๐ด ยทih ๐ต)) + (if((๐ โ โ โง (absโ๐) = 1), ๐, 1) ยท (๐ต ยทih ๐ด)))) |
5 | 4 | breq1d 5152 |
. 2
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ ((((โโ๐) ยท (๐ด ยทih ๐ต)) + (๐ ยท (๐ต ยทih ๐ด))) โค (2 ยท
((โโ(๐ต
ยทih ๐ต)) ยท (โโ(๐ด
ยทih ๐ด)))) โ (((โโif((๐ โ โ โง
(absโ๐) = 1), ๐, 1)) ยท (๐ด
ยทih ๐ต)) + (if((๐ โ โ โง (absโ๐) = 1), ๐, 1) ยท (๐ต ยทih ๐ด))) โค (2 ยท
((โโ(๐ต
ยทih ๐ต)) ยท (โโ(๐ด
ยทih ๐ด)))))) |
6 | | eleq1 2816 |
. . . . . 6
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ (๐ โ โ โ if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ โ)) |
7 | | fveq2 6891 |
. . . . . . 7
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ (absโ๐) = (absโif((๐ โ โ โง (absโ๐) = 1), ๐, 1))) |
8 | 7 | eqeq1d 2729 |
. . . . . 6
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ ((absโ๐) = 1 โ (absโif((๐ โ โ โง
(absโ๐) = 1), ๐, 1)) = 1)) |
9 | 6, 8 | anbi12d 630 |
. . . . 5
โข (๐ = if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ ((๐ โ โ โง (absโ๐) = 1) โ (if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ โ โง
(absโif((๐ โ
โ โง (absโ๐)
= 1), ๐, 1)) =
1))) |
10 | | eleq1 2816 |
. . . . . 6
โข (1 =
if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ (1 โ โ
โ if((๐ โ โ
โง (absโ๐) = 1),
๐, 1) โ
โ)) |
11 | | fveq2 6891 |
. . . . . . 7
โข (1 =
if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ (absโ1) =
(absโif((๐ โ
โ โง (absโ๐)
= 1), ๐,
1))) |
12 | 11 | eqeq1d 2729 |
. . . . . 6
โข (1 =
if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ ((absโ1) = 1
โ (absโif((๐
โ โ โง (absโ๐) = 1), ๐, 1)) = 1)) |
13 | 10, 12 | anbi12d 630 |
. . . . 5
โข (1 =
if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ ((1 โ โ
โง (absโ1) = 1) โ (if((๐ โ โ โง (absโ๐) = 1), ๐, 1) โ โ โง
(absโif((๐ โ
โ โง (absโ๐)
= 1), ๐, 1)) =
1))) |
14 | | ax-1cn 11182 |
. . . . . 6
โข 1 โ
โ |
15 | | abs1 15262 |
. . . . . 6
โข
(absโ1) = 1 |
16 | 14, 15 | pm3.2i 470 |
. . . . 5
โข (1 โ
โ โง (absโ1) = 1) |
17 | 9, 13, 16 | elimhyp 4589 |
. . . 4
โข
(if((๐ โ
โ โง (absโ๐)
= 1), ๐, 1) โ โ
โง (absโif((๐
โ โ โง (absโ๐) = 1), ๐, 1)) = 1) |
18 | 17 | simpli 483 |
. . 3
โข if((๐ โ โ โง
(absโ๐) = 1), ๐, 1) โ
โ |
19 | | normlem7t.1 |
. . 3
โข ๐ด โ โ |
20 | | normlem7t.2 |
. . 3
โข ๐ต โ โ |
21 | 17 | simpri 485 |
. . 3
โข
(absโif((๐
โ โ โง (absโ๐) = 1), ๐, 1)) = 1 |
22 | 18, 19, 20, 21 | normlem7 30900 |
. 2
โข
(((โโif((๐ โ โ โง (absโ๐) = 1), ๐, 1)) ยท (๐ด ยทih ๐ต)) + (if((๐ โ โ โง (absโ๐) = 1), ๐, 1) ยท (๐ต ยทih ๐ด))) โค (2 ยท
((โโ(๐ต
ยทih ๐ต)) ยท (โโ(๐ด
ยทih ๐ด)))) |
23 | 5, 22 | dedth 4582 |
1
โข ((๐ โ โ โง
(absโ๐) = 1) โ
(((โโ๐)
ยท (๐ด
ยทih ๐ต)) + (๐ ยท (๐ต ยทih ๐ด))) โค (2 ยท
((โโ(๐ต
ยทih ๐ต)) ยท (โโ(๐ด
ยทih ๐ด))))) |