Step | Hyp | Ref
| Expression |
1 | | 1cnd 11158 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 โ
โ) |
2 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ ๐ด โ
โ) |
3 | 1, 2 | subcld 11520 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) โ
โ) |
4 | | simpr 486 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 1) โ ๐ด โ 1) |
5 | 4 | necomd 2996 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 โ ๐ด) |
6 | 1, 2, 5 | subne0d 11529 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) โ 0) |
7 | 1, 3, 6 | divcan4d 11945 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) / (1 โ
๐ด)) = 1) |
8 | 7 | eqcomd 2739 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 = ((1 ยท
(1 โ ๐ด)) / (1 โ
๐ด))) |
9 | 8 | oveq1d 7376 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ (1 /
(1 โ ๐ด))) = (((1
ยท (1 โ ๐ด)) /
(1 โ ๐ด)) โ (1 /
(1 โ ๐ด)))) |
10 | 1, 3 | mulcld 11183 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 ยท (1
โ ๐ด)) โ
โ) |
11 | 10, 1, 3, 6 | divsubdird 11978 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (((1 ยท
(1 โ ๐ด)) / (1 โ
๐ด)) โ (1 / (1 โ
๐ด)))) |
12 | 3 | mullidd 11181 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 ยท (1
โ ๐ด)) = (1 โ
๐ด)) |
13 | 12 | oveq1d 7376 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) โ 1) =
((1 โ ๐ด) โ
1)) |
14 | | negcl 11409 |
. . . . . . 7
โข (๐ด โ โ โ -๐ด โ
โ) |
15 | 14 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ -๐ด โ
โ) |
16 | 1, 2 | negsubd 11526 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 + -๐ด) = (1 โ ๐ด)) |
17 | 16 | eqcomd 2739 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) = (1 + -๐ด)) |
18 | 1, 15, 17 | mvrladdd 11576 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 โ
๐ด) โ 1) = -๐ด) |
19 | 13, 18 | eqtrd 2773 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) โ 1) =
-๐ด) |
20 | 19 | oveq1d 7376 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (-๐ด / (1 โ ๐ด))) |
21 | 2, 3, 6 | divneg2d 11953 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ -(๐ด / (1 โ ๐ด)) = (๐ด / -(1 โ ๐ด))) |
22 | 2, 3, 6 | divnegd 11952 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ -(๐ด / (1 โ ๐ด)) = (-๐ด / (1 โ ๐ด))) |
23 | 1, 2 | negsubdi2d 11536 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ -(1 โ
๐ด) = (๐ด โ 1)) |
24 | 23 | oveq2d 7377 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ (๐ด / -(1 โ ๐ด)) = (๐ด / (๐ด โ 1))) |
25 | 21, 22, 24 | 3eqtr3d 2781 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (-๐ด / (1 โ ๐ด)) = (๐ด / (๐ด โ 1))) |
26 | 20, 25 | eqtrd 2773 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (๐ด / (๐ด โ 1))) |
27 | 9, 11, 26 | 3eqtr2d 2779 |
1
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ (1 /
(1 โ ๐ด))) = (๐ด / (๐ด โ 1))) |