Step |
Hyp |
Ref |
Expression |
1 |
|
isosctrlem3.1 |
โข ๐น = ( ๐ฅ โ ( โ โ { 0 } ) , ๐ฆ โ ( โ โ { 0 } ) โฆ ( โ โ ( log โ ( ๐ฆ / ๐ฅ ) ) ) ) |
2 |
|
simp1l |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ด โ โ ) |
3 |
|
simp21 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ด โ 0 ) |
4 |
|
simp1r |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ต โ โ ) |
5 |
2 4
|
subcld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด โ ๐ต ) โ โ ) |
6 |
|
simp23 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ด โ ๐ต ) |
7 |
2 4 6
|
subne0d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด โ ๐ต ) โ 0 ) |
8 |
1
|
angneg |
โข ( ( ( ๐ด โ โ โง ๐ด โ 0 ) โง ( ( ๐ด โ ๐ต ) โ โ โง ( ๐ด โ ๐ต ) โ 0 ) ) โ ( - ๐ด ๐น - ( ๐ด โ ๐ต ) ) = ( ๐ด ๐น ( ๐ด โ ๐ต ) ) ) |
9 |
2 3 5 7 8
|
syl22anc |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( - ๐ด ๐น - ( ๐ด โ ๐ต ) ) = ( ๐ด ๐น ( ๐ด โ ๐ต ) ) ) |
10 |
2 4
|
negsubdi2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ - ( ๐ด โ ๐ต ) = ( ๐ต โ ๐ด ) ) |
11 |
10
|
oveq2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( - ๐ด ๐น - ( ๐ด โ ๐ต ) ) = ( - ๐ด ๐น ( ๐ต โ ๐ด ) ) ) |
12 |
|
1cnd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ 1 โ โ ) |
13 |
|
ax-1ne0 |
โข 1 โ 0 |
14 |
13
|
a1i |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ 1 โ 0 ) |
15 |
4 2 3
|
divcld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ต / ๐ด ) โ โ ) |
16 |
12 15
|
subcld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( 1 โ ( ๐ต / ๐ด ) ) โ โ ) |
17 |
6
|
necomd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ต โ ๐ด ) |
18 |
4 2 3 17
|
divne1d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ต / ๐ด ) โ 1 ) |
19 |
18
|
necomd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ 1 โ ( ๐ต / ๐ด ) ) |
20 |
12 15 19
|
subne0d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( 1 โ ( ๐ต / ๐ด ) ) โ 0 ) |
21 |
1 12 14 16 20
|
angvald |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( 1 ๐น ( 1 โ ( ๐ต / ๐ด ) ) ) = ( โ โ ( log โ ( ( 1 โ ( ๐ต / ๐ด ) ) / 1 ) ) ) ) |
22 |
16
|
div1d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( 1 โ ( ๐ต / ๐ด ) ) / 1 ) = ( 1 โ ( ๐ต / ๐ด ) ) ) |
23 |
22
|
fveq2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( log โ ( ( 1 โ ( ๐ต / ๐ด ) ) / 1 ) ) = ( log โ ( 1 โ ( ๐ต / ๐ด ) ) ) ) |
24 |
23
|
fveq2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( โ โ ( log โ ( ( 1 โ ( ๐ต / ๐ด ) ) / 1 ) ) ) = ( โ โ ( log โ ( 1 โ ( ๐ต / ๐ด ) ) ) ) ) |
25 |
4 2 3
|
absdivd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ( ๐ต / ๐ด ) ) = ( ( abs โ ๐ต ) / ( abs โ ๐ด ) ) ) |
26 |
|
simp3 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ๐ด ) = ( abs โ ๐ต ) ) |
27 |
26
|
eqcomd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ๐ต ) = ( abs โ ๐ด ) ) |
28 |
27
|
oveq1d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( abs โ ๐ต ) / ( abs โ ๐ด ) ) = ( ( abs โ ๐ด ) / ( abs โ ๐ด ) ) ) |
29 |
2
|
abscld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ๐ด ) โ โ ) |
30 |
29
|
recnd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ๐ด ) โ โ ) |
31 |
2 3
|
absne0d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ๐ด ) โ 0 ) |
32 |
30 31
|
dividd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( abs โ ๐ด ) / ( abs โ ๐ด ) ) = 1 ) |
33 |
25 28 32
|
3eqtrd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( abs โ ( ๐ต / ๐ด ) ) = 1 ) |
34 |
19
|
neneqd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ยฌ 1 = ( ๐ต / ๐ด ) ) |
35 |
|
isosctrlem2 |
โข ( ( ( ๐ต / ๐ด ) โ โ โง ( abs โ ( ๐ต / ๐ด ) ) = 1 โง ยฌ 1 = ( ๐ต / ๐ด ) ) โ ( โ โ ( log โ ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( โ โ ( log โ ( - ( ๐ต / ๐ด ) / ( 1 โ ( ๐ต / ๐ด ) ) ) ) ) ) |
36 |
15 33 34 35
|
syl3anc |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( โ โ ( log โ ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( โ โ ( log โ ( - ( ๐ต / ๐ด ) / ( 1 โ ( ๐ต / ๐ด ) ) ) ) ) ) |
37 |
15
|
negcld |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ - ( ๐ต / ๐ด ) โ โ ) |
38 |
|
simp22 |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ๐ต โ 0 ) |
39 |
4 2 38 3
|
divne0d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ต / ๐ด ) โ 0 ) |
40 |
15 39
|
negne0d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ - ( ๐ต / ๐ด ) โ 0 ) |
41 |
1 16 20 37 40
|
angvald |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) = ( โ โ ( log โ ( - ( ๐ต / ๐ด ) / ( 1 โ ( ๐ต / ๐ด ) ) ) ) ) ) |
42 |
36 41
|
eqtr4d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( โ โ ( log โ ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) ) |
43 |
21 24 42
|
3eqtrd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( 1 ๐น ( 1 โ ( ๐ต / ๐ด ) ) ) = ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) ) |
44 |
2
|
mulridd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท 1 ) = ๐ด ) |
45 |
2 12 15
|
subdid |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) = ( ( ๐ด ยท 1 ) โ ( ๐ด ยท ( ๐ต / ๐ด ) ) ) ) |
46 |
4 2 3
|
divcan2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท ( ๐ต / ๐ด ) ) = ๐ต ) |
47 |
44 46
|
oveq12d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด ยท 1 ) โ ( ๐ด ยท ( ๐ต / ๐ด ) ) ) = ( ๐ด โ ๐ต ) ) |
48 |
45 47
|
eqtrd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) = ( ๐ด โ ๐ต ) ) |
49 |
44 48
|
oveq12d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด ยท 1 ) ๐น ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( ๐ด ๐น ( ๐ด โ ๐ต ) ) ) |
50 |
1
|
angcan |
โข ( ( ( 1 โ โ โง 1 โ 0 ) โง ( ( 1 โ ( ๐ต / ๐ด ) ) โ โ โง ( 1 โ ( ๐ต / ๐ด ) ) โ 0 ) โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ( ๐ด ยท 1 ) ๐น ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( 1 ๐น ( 1 โ ( ๐ต / ๐ด ) ) ) ) |
51 |
12 14 16 20 2 3 50
|
syl222anc |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด ยท 1 ) ๐น ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ) = ( 1 ๐น ( 1 โ ( ๐ต / ๐ด ) ) ) ) |
52 |
49 51
|
eqtr3d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ๐น ( ๐ด โ ๐ต ) ) = ( 1 ๐น ( 1 โ ( ๐ต / ๐ด ) ) ) ) |
53 |
2 15
|
mulneg2d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท - ( ๐ต / ๐ด ) ) = - ( ๐ด ยท ( ๐ต / ๐ด ) ) ) |
54 |
46
|
negeqd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ - ( ๐ด ยท ( ๐ต / ๐ด ) ) = - ๐ต ) |
55 |
53 54
|
eqtrd |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ยท - ( ๐ต / ๐ด ) ) = - ๐ต ) |
56 |
48 55
|
oveq12d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ๐น ( ๐ด ยท - ( ๐ต / ๐ด ) ) ) = ( ( ๐ด โ ๐ต ) ๐น - ๐ต ) ) |
57 |
1
|
angcan |
โข ( ( ( ( 1 โ ( ๐ต / ๐ด ) ) โ โ โง ( 1 โ ( ๐ต / ๐ด ) ) โ 0 ) โง ( - ( ๐ต / ๐ด ) โ โ โง - ( ๐ต / ๐ด ) โ 0 ) โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ๐น ( ๐ด ยท - ( ๐ต / ๐ด ) ) ) = ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) ) |
58 |
16 20 37 40 2 3 57
|
syl222anc |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด ยท ( 1 โ ( ๐ต / ๐ด ) ) ) ๐น ( ๐ด ยท - ( ๐ต / ๐ด ) ) ) = ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) ) |
59 |
56 58
|
eqtr3d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ( ๐ด โ ๐ต ) ๐น - ๐ต ) = ( ( 1 โ ( ๐ต / ๐ด ) ) ๐น - ( ๐ต / ๐ด ) ) ) |
60 |
43 52 59
|
3eqtr4d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( ๐ด ๐น ( ๐ด โ ๐ต ) ) = ( ( ๐ด โ ๐ต ) ๐น - ๐ต ) ) |
61 |
9 11 60
|
3eqtr3d |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ด โ 0 โง ๐ต โ 0 โง ๐ด โ ๐ต ) โง ( abs โ ๐ด ) = ( abs โ ๐ต ) ) โ ( - ๐ด ๐น ( ๐ต โ ๐ด ) ) = ( ( ๐ด โ ๐ต ) ๐น - ๐ต ) ) |