Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ด โ โ) |
2 | | simp21 1207 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ด โ 0) |
3 | | simp1r 1199 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ต โ โ) |
4 | 1, 3 | subcld 11571 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด โ ๐ต) โ โ) |
5 | | simp23 1209 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ด โ ๐ต) |
6 | 1, 3, 5 | subne0d 11580 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด โ ๐ต) โ 0) |
7 | | isosctrlem3.1 |
. . . 4
โข ๐น = (๐ฅ โ (โ โ {0}), ๐ฆ โ (โ โ {0})
โฆ (โโ(logโ(๐ฆ / ๐ฅ)))) |
8 | 7 | angneg 26308 |
. . 3
โข (((๐ด โ โ โง ๐ด โ 0) โง ((๐ด โ ๐ต) โ โ โง (๐ด โ ๐ต) โ 0)) โ (-๐ด๐น-(๐ด โ ๐ต)) = (๐ด๐น(๐ด โ ๐ต))) |
9 | 1, 2, 4, 6, 8 | syl22anc 838 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (-๐ด๐น-(๐ด โ ๐ต)) = (๐ด๐น(๐ด โ ๐ต))) |
10 | 1, 3 | negsubdi2d 11587 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ -(๐ด โ ๐ต) = (๐ต โ ๐ด)) |
11 | 10 | oveq2d 7425 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (-๐ด๐น-(๐ด โ ๐ต)) = (-๐ด๐น(๐ต โ ๐ด))) |
12 | | 1cnd 11209 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ 1 โ โ) |
13 | | ax-1ne0 11179 |
. . . . . 6
โข 1 โ
0 |
14 | 13 | a1i 11 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ 1 โ 0) |
15 | 3, 1, 2 | divcld 11990 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ต / ๐ด) โ โ) |
16 | 12, 15 | subcld 11571 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (1 โ (๐ต / ๐ด)) โ โ) |
17 | 5 | necomd 2997 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ต โ ๐ด) |
18 | 3, 1, 2, 17 | divne1d 12001 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ต / ๐ด) โ 1) |
19 | 18 | necomd 2997 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ 1 โ (๐ต / ๐ด)) |
20 | 12, 15, 19 | subne0d 11580 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (1 โ (๐ต / ๐ด)) โ 0) |
21 | 7, 12, 14, 16, 20 | angvald 26309 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (1๐น(1 โ (๐ต / ๐ด))) = (โโ(logโ((1 โ
(๐ต / ๐ด)) / 1)))) |
22 | 16 | div1d 11982 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((1 โ (๐ต / ๐ด)) / 1) = (1 โ (๐ต / ๐ด))) |
23 | 22 | fveq2d 6896 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (logโ((1 โ (๐ต / ๐ด)) / 1)) = (logโ(1 โ (๐ต / ๐ด)))) |
24 | 23 | fveq2d 6896 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (โโ(logโ((1
โ (๐ต / ๐ด)) / 1))) =
(โโ(logโ(1 โ (๐ต / ๐ด))))) |
25 | 3, 1, 2 | absdivd 15402 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ(๐ต / ๐ด)) = ((absโ๐ต) / (absโ๐ด))) |
26 | | simp3 1139 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ๐ด) = (absโ๐ต)) |
27 | 26 | eqcomd 2739 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ๐ต) = (absโ๐ด)) |
28 | 27 | oveq1d 7424 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((absโ๐ต) / (absโ๐ด)) = ((absโ๐ด) / (absโ๐ด))) |
29 | 1 | abscld 15383 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ๐ด) โ โ) |
30 | 29 | recnd 11242 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ๐ด) โ โ) |
31 | 1, 2 | absne0d 15394 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ๐ด) โ 0) |
32 | 30, 31 | dividd 11988 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((absโ๐ด) / (absโ๐ด)) = 1) |
33 | 25, 28, 32 | 3eqtrd 2777 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (absโ(๐ต / ๐ด)) = 1) |
34 | 19 | neneqd 2946 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ยฌ 1 = (๐ต / ๐ด)) |
35 | | isosctrlem2 26324 |
. . . . . 6
โข (((๐ต / ๐ด) โ โ โง (absโ(๐ต / ๐ด)) = 1 โง ยฌ 1 = (๐ต / ๐ด)) โ (โโ(logโ(1
โ (๐ต / ๐ด)))) =
(โโ(logโ(-(๐ต / ๐ด) / (1 โ (๐ต / ๐ด)))))) |
36 | 15, 33, 34, 35 | syl3anc 1372 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (โโ(logโ(1
โ (๐ต / ๐ด)))) =
(โโ(logโ(-(๐ต / ๐ด) / (1 โ (๐ต / ๐ด)))))) |
37 | 15 | negcld 11558 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ -(๐ต / ๐ด) โ โ) |
38 | | simp22 1208 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ๐ต โ 0) |
39 | 3, 1, 38, 2 | divne0d 12006 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ต / ๐ด) โ 0) |
40 | 15, 39 | negne0d 11569 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ -(๐ต / ๐ด) โ 0) |
41 | 7, 16, 20, 37, 40 | angvald 26309 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด)) = (โโ(logโ(-(๐ต / ๐ด) / (1 โ (๐ต / ๐ด)))))) |
42 | 36, 41 | eqtr4d 2776 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (โโ(logโ(1
โ (๐ต / ๐ด)))) = ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด))) |
43 | 21, 24, 42 | 3eqtrd 2777 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (1๐น(1 โ (๐ต / ๐ด))) = ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด))) |
44 | 1 | mulridd 11231 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท 1) = ๐ด) |
45 | 1, 12, 15 | subdid 11670 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท (1 โ (๐ต / ๐ด))) = ((๐ด ยท 1) โ (๐ด ยท (๐ต / ๐ด)))) |
46 | 3, 1, 2 | divcan2d 11992 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท (๐ต / ๐ด)) = ๐ต) |
47 | 44, 46 | oveq12d 7427 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด ยท 1) โ (๐ด ยท (๐ต / ๐ด))) = (๐ด โ ๐ต)) |
48 | 45, 47 | eqtrd 2773 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท (1 โ (๐ต / ๐ด))) = (๐ด โ ๐ต)) |
49 | 44, 48 | oveq12d 7427 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด ยท 1)๐น(๐ด ยท (1 โ (๐ต / ๐ด)))) = (๐ด๐น(๐ด โ ๐ต))) |
50 | 7 | angcan 26307 |
. . . . 5
โข (((1
โ โ โง 1 โ 0) โง ((1 โ (๐ต / ๐ด)) โ โ โง (1 โ (๐ต / ๐ด)) โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท 1)๐น(๐ด ยท (1 โ (๐ต / ๐ด)))) = (1๐น(1 โ (๐ต / ๐ด)))) |
51 | 12, 14, 16, 20, 1, 2, 50 | syl222anc 1387 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด ยท 1)๐น(๐ด ยท (1 โ (๐ต / ๐ด)))) = (1๐น(1 โ (๐ต / ๐ด)))) |
52 | 49, 51 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด๐น(๐ด โ ๐ต)) = (1๐น(1 โ (๐ต / ๐ด)))) |
53 | 1, 15 | mulneg2d 11668 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท -(๐ต / ๐ด)) = -(๐ด ยท (๐ต / ๐ด))) |
54 | 46 | negeqd 11454 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ -(๐ด ยท (๐ต / ๐ด)) = -๐ต) |
55 | 53, 54 | eqtrd 2773 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด ยท -(๐ต / ๐ด)) = -๐ต) |
56 | 48, 55 | oveq12d 7427 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท -(๐ต / ๐ด))) = ((๐ด โ ๐ต)๐น-๐ต)) |
57 | 7 | angcan 26307 |
. . . . 5
โข ((((1
โ (๐ต / ๐ด)) โ โ โง (1
โ (๐ต / ๐ด)) โ 0) โง (-(๐ต / ๐ด) โ โ โง -(๐ต / ๐ด) โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท -(๐ต / ๐ด))) = ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด))) |
58 | 16, 20, 37, 40, 1, 2, 57 | syl222anc 1387 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด ยท (1 โ (๐ต / ๐ด)))๐น(๐ด ยท -(๐ต / ๐ด))) = ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด))) |
59 | 56, 58 | eqtr3d 2775 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ ((๐ด โ ๐ต)๐น-๐ต) = ((1 โ (๐ต / ๐ด))๐น-(๐ต / ๐ด))) |
60 | 43, 52, 59 | 3eqtr4d 2783 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (๐ด๐น(๐ด โ ๐ต)) = ((๐ด โ ๐ต)๐น-๐ต)) |
61 | 9, 11, 60 | 3eqtr3d 2781 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต) โง (absโ๐ด) = (absโ๐ต)) โ (-๐ด๐น(๐ต โ ๐ด)) = ((๐ด โ ๐ต)๐น-๐ต)) |