Metamath Proof Explorer


Theorem isosctrlem3

Description: Lemma for isosctr . Corresponds to the case where one vertex is at 0. (Contributed by Saveliy Skresanov, 1-Jan-2017)

Ref Expression
Hypothesis isosctrlem3.1 โŠข ๐น = ( ๐‘ฅ โˆˆ ( โ„‚ โˆ– { 0 } ) , ๐‘ฆ โˆˆ ( โ„‚ โˆ– { 0 } ) โ†ฆ ( โ„‘ โ€˜ ( log โ€˜ ( ๐‘ฆ / ๐‘ฅ ) ) ) )
Assertion isosctrlem3 ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐ด โ‰  0 โˆง ๐ต โ‰  0 โˆง ๐ด โ‰  ๐ต ) โˆง ( abs โ€˜ ๐ด ) = ( abs โ€˜ ๐ต ) ) โ†’ ( - ๐ด ๐น ( ๐ต โˆ’ ๐ด ) ) = ( ( ๐ด โˆ’ ๐ต ) ๐น - ๐ต ) )

Proof

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 โ€˜ ๐ต ) ) โ†’ ( - ๐ด ๐น ( ๐ต โˆ’ ๐ด ) ) = ( ( ๐ด โˆ’ ๐ต ) ๐น - ๐ต ) )