Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . . 8
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ (๐ด ยทih (๐โ๐ด)) = (๐ด ยทih (๐ต
ยทโ ๐ด))) |
2 | 1 | eleq1d 2823 |
. . . . . . 7
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ)) |
3 | | eigpos.1 |
. . . . . . . . 9
โข ๐ด โ โ |
4 | | eigpos.2 |
. . . . . . . . . 10
โข ๐ต โ โ |
5 | 4, 3 | hvmulcli 29998 |
. . . . . . . . 9
โข (๐ต
ยทโ ๐ด) โ โ |
6 | | hire 30078 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ต
ยทโ ๐ด) โ โ) โ ((๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ โ (๐ด ยทih (๐ต
ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด))) |
7 | 3, 5, 6 | mp2an 691 |
. . . . . . . 8
โข ((๐ด
ยทih (๐ต ยทโ ๐ด)) โ โ โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด)) |
8 | | oveq1 7369 |
. . . . . . . . 9
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐โ๐ด) ยทih ๐ด) = ((๐ต ยทโ ๐ด)
ยทih ๐ด)) |
9 | 1, 8 | eqeq12d 2753 |
. . . . . . . 8
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ (๐ด ยทih (๐ต
ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด))) |
10 | 7, 9 | bitr4id 290 |
. . . . . . 7
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
11 | 2, 10 | bitrd 279 |
. . . . . 6
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
12 | 11 | adantr 482 |
. . . . 5
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
13 | 3, 4 | eigrei 30818 |
. . . . 5
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) |
14 | 12, 13 | bitrd 279 |
. . . 4
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) โ โ โ ๐ต โ โ)) |
15 | 14 | biimpac 480 |
. . 3
โข (((๐ด
ยทih (๐โ๐ด)) โ โ โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ๐ต โ
โ) |
16 | 15 | adantlr 714 |
. 2
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ๐ต โ
โ) |
17 | | hiidrcl 30079 |
. . . . 5
โข (๐ด โ โ โ (๐ด
ยทih ๐ด) โ โ) |
18 | 3, 17 | mp1i 13 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih ๐ด) โ โ) |
19 | | ax-his4 30069 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (๐ด
ยทih ๐ด)) |
20 | 3, 19 | mpan 689 |
. . . . 5
โข (๐ด โ 0โ
โ 0 < (๐ด
ยทih ๐ด)) |
21 | 20 | ad2antll 728 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 <
(๐ด
ยทih ๐ด)) |
22 | 18, 21 | elrpd 12961 |
. . 3
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih ๐ด) โ
โ+) |
23 | | simplr 768 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
(๐ด
ยทih (๐โ๐ด))) |
24 | 1 | ad2antrl 727 |
. . . . 5
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐โ๐ด)) = (๐ด ยทih (๐ต
ยทโ ๐ด))) |
25 | | his5 30070 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ โง ๐ด โ โ) โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((โโ๐ต) ยท (๐ด ยทih ๐ด))) |
26 | 4, 3, 3, 25 | mp3an 1462 |
. . . . . 6
โข (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((โโ๐ต) ยท (๐ด ยทih ๐ด)) |
27 | 16 | cjred 15118 |
. . . . . . 7
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ
(โโ๐ต) = ๐ต) |
28 | 27 | oveq1d 7377 |
. . . . . 6
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ
((โโ๐ต)
ยท (๐ด
ยทih ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
29 | 26, 28 | eqtrid 2789 |
. . . . 5
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
30 | 24, 29 | eqtrd 2777 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐โ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
31 | 23, 30 | breqtrd 5136 |
. . 3
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
(๐ต ยท (๐ด
ยทih ๐ด))) |
32 | 16, 22, 31 | prodge0ld 13030 |
. 2
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
๐ต) |
33 | 16, 32 | jca 513 |
1
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ต โ โ โง 0 โค
๐ต)) |