Step | Hyp | Ref
| Expression |
1 | | elznn0 12572 |
. . 3
โข (๐ถ โ โค โ (๐ถ โ โ โง (๐ถ โ โ0 โจ
-๐ถ โ
โ0))) |
2 | | cxpmul2 26196 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ0)
โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ)) |
3 | 2 | 3expia 1121 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ถ โ โ0
โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
4 | 3 | ad4ant13 749 |
. . . . 5
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ถ โ โ0 โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
5 | | simplll 773 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ๐ด โ
โ) |
6 | | simplr 767 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ๐ต โ
โ) |
7 | | simprr 771 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ -๐ถ โ
โ0) |
8 | | cxpmul2 26196 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง -๐ถ โ โ0)
โ (๐ดโ๐(๐ต ยท -๐ถ)) = ((๐ดโ๐๐ต)โ-๐ถ)) |
9 | 5, 6, 7, 8 | syl3anc 1371 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐(๐ต ยท -๐ถ)) = ((๐ดโ๐๐ต)โ-๐ถ)) |
10 | 9 | oveq2d 7424 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (1 /
(๐ดโ๐(๐ต ยท -๐ถ))) = (1 / ((๐ดโ๐๐ต)โ-๐ถ))) |
11 | | simprl 769 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ๐ถ โ
โ) |
12 | 11 | recnd 11241 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ๐ถ โ
โ) |
13 | 6, 12 | mulneg2d 11667 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ต ยท -๐ถ) = -(๐ต ยท ๐ถ)) |
14 | 13 | negeqd 11453 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ -(๐ต ยท -๐ถ) = --(๐ต ยท ๐ถ)) |
15 | 6, 12 | mulcld 11233 |
. . . . . . . . . . 11
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ต ยท ๐ถ) โ โ) |
16 | 15 | negnegd 11561 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ
--(๐ต ยท ๐ถ) = (๐ต ยท ๐ถ)) |
17 | 14, 16 | eqtrd 2772 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ -(๐ต ยท -๐ถ) = (๐ต ยท ๐ถ)) |
18 | 17 | oveq2d 7424 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐-(๐ต ยท -๐ถ)) = (๐ดโ๐(๐ต ยท ๐ถ))) |
19 | | simpllr 774 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ๐ด โ 0) |
20 | 12 | negcld 11557 |
. . . . . . . . . 10
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ -๐ถ โ
โ) |
21 | 6, 20 | mulcld 11233 |
. . . . . . . . 9
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ต ยท -๐ถ) โ โ) |
22 | | cxpneg 26188 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0 โง (๐ต ยท -๐ถ) โ โ) โ (๐ดโ๐-(๐ต ยท -๐ถ)) = (1 / (๐ดโ๐(๐ต ยท -๐ถ)))) |
23 | 5, 19, 21, 22 | syl3anc 1371 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐-(๐ต ยท -๐ถ)) = (1 / (๐ดโ๐(๐ต ยท -๐ถ)))) |
24 | 18, 23 | eqtr3d 2774 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐(๐ต ยท ๐ถ)) = (1 / (๐ดโ๐(๐ต ยท -๐ถ)))) |
25 | | cxpcl 26181 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ดโ๐๐ต) โ
โ) |
26 | 25 | ad4ant13 749 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐๐ต) โ
โ) |
27 | | expneg2 14035 |
. . . . . . . 8
โข (((๐ดโ๐๐ต) โ โ โง ๐ถ โ โ โง -๐ถ โ โ0)
โ ((๐ดโ๐๐ต)โ๐ถ) = (1 / ((๐ดโ๐๐ต)โ-๐ถ))) |
28 | 26, 12, 7, 27 | syl3anc 1371 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ ((๐ดโ๐๐ต)โ๐ถ) = (1 / ((๐ดโ๐๐ต)โ-๐ถ))) |
29 | 10, 24, 28 | 3eqtr4d 2782 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง (๐ถ โ โ โง -๐ถ โ โ0)) โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ)) |
30 | 29 | expr 457 |
. . . . 5
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง ๐ถ โ โ) โ (-๐ถ โ โ0 โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
31 | 4, 30 | jaod 857 |
. . . 4
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ถ โ โ0 โจ -๐ถ โ โ0)
โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
32 | 31 | expimpd 454 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โ ((๐ถ โ โ โง (๐ถ โ โ0 โจ -๐ถ โ โ0))
โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
33 | 1, 32 | biimtrid 241 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ) โ (๐ถ โ โค โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ))) |
34 | 33 | impr 455 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ต โ โ โง ๐ถ โ โค)) โ (๐ดโ๐(๐ต ยท ๐ถ)) = ((๐ดโ๐๐ต)โ๐ถ)) |