Theorem angpieqvdlem2

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

	Ref	Expression
Hypotheses	angpieqvd.angdef	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
	angpieqvd.A	$$⊢\phi \to A\in ℂ$$
	angpieqvd.B	$$⊢\phi \to B\in ℂ$$
	angpieqvd.C	$$⊢\phi \to C\in ℂ$$
	angpieqvd.AneB	$$⊢\phi \to A\ne B$$
	angpieqvd.BneC	$$⊢\phi \to B\ne C$$
Assertion	angpieqvdlem2	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\right)$$

Proof

Step	Hyp	Ref	Expression
1		angpieqvd.angdef	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
2		angpieqvd.A	$$⊢\phi \to A\in ℂ$$
3		angpieqvd.B	$$⊢\phi \to B\in ℂ$$
4		angpieqvd.C	$$⊢\phi \to C\in ℂ$$
5		angpieqvd.AneB	$$⊢\phi \to A\ne B$$
6		angpieqvd.BneC	$$⊢\phi \to B\ne C$$
7	4 3	subcld	$$⊢\phi \to C-B\in ℂ$$
8	2 3	subcld	$$⊢\phi \to A-B\in ℂ$$
9	2 3 5	subne0d	$$⊢\phi \to A-B\ne 0$$
10	7 8 9	divcld	$$⊢\phi \to \frac{C-B}{A-B}\in ℂ$$
11	6	necomd	$$⊢\phi \to C\ne B$$
12	4 3 11	subne0d	$$⊢\phi \to C-B\ne 0$$
13	7 8 12 9	divne0d	$$⊢\phi \to \frac{C-B}{A-B}\ne 0$$
14		lognegb	$$⊢\left(\frac{C-B}{A-B}\in ℂ\wedge \frac{C-B}{A-B}\ne 0\right)\to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \Im \left(\log \left(\frac{C-B}{A-B}\right)\right)=\mathrm{\pi }\right)$$
15	10 13 14	syl2anc	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \Im \left(\log \left(\frac{C-B}{A-B}\right)\right)=\mathrm{\pi }\right)$$
16	1 8 9 7 12	angvald	$$⊢\phi \to \left(A-B\right)F\left(C-B\right)=\Im \left(\log \left(\frac{C-B}{A-B}\right)\right)$$
17	16	eqeq1d	$$⊢\phi \to \left(\left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\leftrightarrow \Im \left(\log \left(\frac{C-B}{A-B}\right)\right)=\mathrm{\pi }\right)$$
18	15 17	bitr4d	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \left(A-B\right)F\left(C-B\right)=\mathrm{\pi }\right)$$