Step | Hyp | Ref
| Expression |
1 | | oveq2 7419 |
. . . . . . . 8
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ (๐ด ยทih (๐โ๐ด)) = (๐ด ยทih (๐ต
ยทโ ๐ด))) |
2 | 1 | eleq1d 2818 |
. . . . . . 7
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ)) |
3 | | eigpos.1 |
. . . . . . . . 9
โข ๐ด โ โ |
4 | | eigpos.2 |
. . . . . . . . . 10
โข ๐ต โ โ |
5 | 4, 3 | hvmulcli 30522 |
. . . . . . . . 9
โข (๐ต
ยทโ ๐ด) โ โ |
6 | | hire 30602 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ต
ยทโ ๐ด) โ โ) โ ((๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ โ (๐ด ยทih (๐ต
ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด))) |
7 | 3, 5, 6 | mp2an 690 |
. . . . . . . 8
โข ((๐ด
ยทih (๐ต ยทโ ๐ด)) โ โ โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด)) |
8 | | oveq1 7418 |
. . . . . . . . 9
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐โ๐ด) ยทih ๐ด) = ((๐ต ยทโ ๐ด)
ยทih ๐ด)) |
9 | 1, 8 | eqeq12d 2748 |
. . . . . . . 8
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ (๐ด ยทih (๐ต
ยทโ ๐ด)) = ((๐ต ยทโ ๐ด)
ยทih ๐ด))) |
10 | 7, 9 | bitr4id 289 |
. . . . . . 7
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐ต
ยทโ ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
11 | 2, 10 | bitrd 278 |
. . . . . 6
โข ((๐โ๐ด) = (๐ต ยทโ ๐ด) โ ((๐ด ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
12 | 11 | adantr 481 |
. . . . 5
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) โ โ โ (๐ด ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด))) |
13 | 3, 4 | eigrei 31342 |
. . . . 5
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) = ((๐โ๐ด) ยทih ๐ด) โ ๐ต โ โ)) |
14 | 12, 13 | bitrd 278 |
. . . 4
โข (((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ) โ ((๐ด
ยทih (๐โ๐ด)) โ โ โ ๐ต โ โ)) |
15 | 14 | biimpac 479 |
. . 3
โข (((๐ด
ยทih (๐โ๐ด)) โ โ โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ๐ต โ
โ) |
16 | 15 | adantlr 713 |
. 2
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ ๐ต โ
โ) |
17 | | hiidrcl 30603 |
. . . . 5
โข (๐ด โ โ โ (๐ด
ยทih ๐ด) โ โ) |
18 | 3, 17 | mp1i 13 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih ๐ด) โ โ) |
19 | | ax-his4 30593 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (๐ด
ยทih ๐ด)) |
20 | 3, 19 | mpan 688 |
. . . . 5
โข (๐ด โ 0โ
โ 0 < (๐ด
ยทih ๐ด)) |
21 | 20 | ad2antll 727 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 <
(๐ด
ยทih ๐ด)) |
22 | 18, 21 | elrpd 13017 |
. . 3
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih ๐ด) โ
โ+) |
23 | | simplr 767 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
(๐ด
ยทih (๐โ๐ด))) |
24 | 1 | ad2antrl 726 |
. . . . 5
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐โ๐ด)) = (๐ด ยทih (๐ต
ยทโ ๐ด))) |
25 | | his5 30594 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ โง ๐ด โ โ) โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((โโ๐ต) ยท (๐ด ยทih ๐ด))) |
26 | 4, 3, 3, 25 | mp3an 1461 |
. . . . . 6
โข (๐ด
ยทih (๐ต ยทโ ๐ด)) = ((โโ๐ต) ยท (๐ด ยทih ๐ด)) |
27 | 16 | cjred 15177 |
. . . . . . 7
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ
(โโ๐ต) = ๐ต) |
28 | 27 | oveq1d 7426 |
. . . . . 6
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ
((โโ๐ต)
ยท (๐ด
ยทih ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
29 | 26, 28 | eqtrid 2784 |
. . . . 5
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐ต ยทโ ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
30 | 24, 29 | eqtrd 2772 |
. . . 4
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ด
ยทih (๐โ๐ด)) = (๐ต ยท (๐ด ยทih ๐ด))) |
31 | 23, 30 | breqtrd 5174 |
. . 3
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
(๐ต ยท (๐ด
ยทih ๐ด))) |
32 | 16, 22, 31 | prodge0ld 13086 |
. 2
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ 0 โค
๐ต) |
33 | 16, 32 | jca 512 |
1
โข ((((๐ด
ยทih (๐โ๐ด)) โ โ โง 0 โค (๐ด
ยทih (๐โ๐ด))) โง ((๐โ๐ด) = (๐ต ยทโ ๐ด) โง ๐ด โ 0โ)) โ (๐ต โ โ โง 0 โค
๐ต)) |