Theorem angpieqvdlem2

Description: Equivalence used in angpieqvd . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	angpieqvd.angdef	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	angpieqvd.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	angpieqvd.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	angpieqvd.C	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	angpieqvd.AneB	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	angpieqvd.BneC	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion	angpieqvdlem2	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )

Proof

Step	Hyp	Ref	Expression
1		angpieqvd.angdef	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		angpieqvd.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
3		angpieqvd.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4		angpieqvd.C	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		angpieqvd.AneB	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
6		angpieqvd.BneC	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
7	4 3	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
8	2 3	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
9	2 3 5	subne0d	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≠ 0 )
10	7 8 9	divcld	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )
11	6	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
12	4 3 11	subne0d	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ 0 )
13	7 8 12 9	divne0d	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ≠ 0 )
14		lognegb	⊢ ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ ∧ ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ≠ 0 ) → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) = π ) )
15	10 13 14	syl2anc	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ℑ ‘ ( log ‘ ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) = π ) )
16	1 8 9 7 12	angvald	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = ( ℑ ‘ ( log ‘ ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) )
17	16	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ↔ ( ℑ ‘ ( log ‘ ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) = π ) )
18	15 17	bitr4d	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )