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 ‘ 𝐵 ) ) → ( - 𝐴 𝐹 ( 𝐵 − 𝐴 ) ) = ( ( 𝐴 − 𝐵 ) 𝐹 - 𝐵 ) )