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 mulid1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐴 ≠ 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 ‘ 𝐵 ) ) → ( - 𝐴 𝐹 ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 − 𝐵 ) 𝐹 - 𝐵 ) )