Step | Hyp | Ref
| Expression |
1 | | 1cnd 11237 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 โ
โ) |
2 | | simpl 481 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ ๐ด โ
โ) |
3 | 1, 2 | subcld 11599 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) โ
โ) |
4 | | simpr 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 1) โ ๐ด โ 1) |
5 | 4 | necomd 2986 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 โ ๐ด) |
6 | 1, 2, 5 | subne0d 11608 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) โ 0) |
7 | 1, 3, 6 | divcan4d 12024 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) / (1 โ
๐ด)) = 1) |
8 | 7 | eqcomd 2731 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ 1 = ((1 ยท
(1 โ ๐ด)) / (1 โ
๐ด))) |
9 | 8 | oveq1d 7430 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ (1 /
(1 โ ๐ด))) = (((1
ยท (1 โ ๐ด)) /
(1 โ ๐ด)) โ (1 /
(1 โ ๐ด)))) |
10 | 1, 3 | mulcld 11262 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 ยท (1
โ ๐ด)) โ
โ) |
11 | 10, 1, 3, 6 | divsubdird 12057 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (((1 ยท
(1 โ ๐ด)) / (1 โ
๐ด)) โ (1 / (1 โ
๐ด)))) |
12 | 3 | mullidd 11260 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 ยท (1
โ ๐ด)) = (1 โ
๐ด)) |
13 | 12 | oveq1d 7430 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) โ 1) =
((1 โ ๐ด) โ
1)) |
14 | | negcl 11488 |
. . . . . . 7
โข (๐ด โ โ โ -๐ด โ
โ) |
15 | 14 | adantr 479 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ -๐ด โ
โ) |
16 | 1, 2 | negsubd 11605 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 + -๐ด) = (1 โ ๐ด)) |
17 | 16 | eqcomd 2731 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ ๐ด) = (1 + -๐ด)) |
18 | 1, 15, 17 | mvrladdd 11655 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 โ
๐ด) โ 1) = -๐ด) |
19 | 13, 18 | eqtrd 2765 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ ((1 ยท (1
โ ๐ด)) โ 1) =
-๐ด) |
20 | 19 | oveq1d 7430 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (-๐ด / (1 โ ๐ด))) |
21 | 2, 3, 6 | divneg2d 12032 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ -(๐ด / (1 โ ๐ด)) = (๐ด / -(1 โ ๐ด))) |
22 | 2, 3, 6 | divnegd 12031 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ -(๐ด / (1 โ ๐ด)) = (-๐ด / (1 โ ๐ด))) |
23 | 1, 2 | negsubdi2d 11615 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 1) โ -(1 โ
๐ด) = (๐ด โ 1)) |
24 | 23 | oveq2d 7431 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 1) โ (๐ด / -(1 โ ๐ด)) = (๐ด / (๐ด โ 1))) |
25 | 21, 22, 24 | 3eqtr3d 2773 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 1) โ (-๐ด / (1 โ ๐ด)) = (๐ด / (๐ด โ 1))) |
26 | 20, 25 | eqtrd 2765 |
. 2
โข ((๐ด โ โ โง ๐ด โ 1) โ (((1 ยท (1
โ ๐ด)) โ 1) / (1
โ ๐ด)) = (๐ด / (๐ด โ 1))) |
27 | 9, 11, 26 | 3eqtr2d 2771 |
1
โข ((๐ด โ โ โง ๐ด โ 1) โ (1 โ (1 /
(1 โ ๐ด))) = (๐ด / (๐ด โ 1))) |