Step | Hyp | Ref
| Expression |
1 | | znegcl 12546 |
. . 3
โข (๐ โ โค โ -๐ โ
โค) |
2 | | expaddz 14021 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง -๐ โ โค)) โ (๐ดโ(๐ + -๐)) = ((๐ดโ๐) ยท (๐ดโ-๐))) |
3 | 1, 2 | sylanr2 682 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ(๐ + -๐)) = ((๐ดโ๐) ยท (๐ดโ-๐))) |
4 | | zcn 12512 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
5 | | zcn 12512 |
. . . . 5
โข (๐ โ โค โ ๐ โ
โ) |
6 | | negsub 11457 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + -๐) = (๐ โ ๐)) |
7 | 4, 5, 6 | syl2an 597 |
. . . 4
โข ((๐ โ โค โง ๐ โ โค) โ (๐ + -๐) = (๐ โ ๐)) |
8 | 7 | adantl 483 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ + -๐) = (๐ โ ๐)) |
9 | 8 | oveq2d 7377 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ(๐ + -๐)) = (๐ดโ(๐ โ ๐))) |
10 | | expnegz 14011 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
11 | 10 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
12 | 11 | adantrl 715 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
13 | 12 | oveq2d 7377 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ดโ๐) ยท (๐ดโ-๐)) = ((๐ดโ๐) ยท (1 / (๐ดโ๐)))) |
14 | | expclz 13999 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (๐ดโ๐) โ โ) |
15 | 14 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ (๐ดโ๐) โ โ) |
16 | 15 | adantrr 716 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ๐) โ โ) |
17 | | expclz 13999 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (๐ดโ๐) โ โ) |
18 | 17 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ (๐ดโ๐) โ โ) |
19 | 18 | adantrl 715 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ๐) โ โ) |
20 | | expne0i 14009 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0 โง ๐ โ โค) โ (๐ดโ๐) โ 0) |
21 | 20 | 3expa 1119 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ โ โค) โ (๐ดโ๐) โ 0) |
22 | 21 | adantrl 715 |
. . . 4
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ๐) โ 0) |
23 | 16, 19, 22 | divrecd 11942 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ดโ๐) / (๐ดโ๐)) = ((๐ดโ๐) ยท (1 / (๐ดโ๐)))) |
24 | 13, 23 | eqtr4d 2776 |
. 2
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ ((๐ดโ๐) ยท (๐ดโ-๐)) = ((๐ดโ๐) / (๐ดโ๐))) |
25 | 3, 9, 24 | 3eqtr3d 2781 |
1
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ โ โค โง ๐ โ โค)) โ (๐ดโ(๐ โ ๐)) = ((๐ดโ๐) / (๐ดโ๐))) |