Theorem angpined

Description: If the angle at ABC is _pi , then A is not equal to C. (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	angpined	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π → 𝐴 ≠ 𝐶 ) )

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	1 2 3 4 5 6	angpieqvdlem2	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )
8		1rp	⊢ 1 ∈ ℝ+
9		1re	⊢ 1 ∈ ℝ
10		ax-1ne0	⊢ 1 ≠ 0
11		rpneg	⊢ ( ( 1 ∈ ℝ ∧ 1 ≠ 0 ) → ( 1 ∈ ℝ+ ↔ ¬ - 1 ∈ ℝ+ ) )
12	9 10 11	mp2an	⊢ ( 1 ∈ ℝ+ ↔ ¬ - 1 ∈ ℝ+ )
13	8 12	mpbi	⊢ ¬ - 1 ∈ ℝ+
14	2 3	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐴 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
16	2 3 5	subne0d	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≠ 0 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐴 ) → ( 𝐴 − 𝐵 ) ≠ 0 )
18		simpr	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐴 ) → 𝐶 = 𝐴 )
19	18	oveq1d	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐴 ) → ( 𝐶 − 𝐵 ) = ( 𝐴 − 𝐵 ) )
20	15 17 19	diveq1bd	⊢ ( ( 𝜑 ∧ 𝐶 = 𝐴 ) → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = 1 )
21	20	adantlr	⊢ ( ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) ∧ 𝐶 = 𝐴 ) → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = 1 )
22	21	negeqd	⊢ ( ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) ∧ 𝐶 = 𝐴 ) → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = - 1 )
23		simplr	⊢ ( ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) ∧ 𝐶 = 𝐴 ) → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )
24	22 23	eqeltrrd	⊢ ( ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) ∧ 𝐶 = 𝐴 ) → - 1 ∈ ℝ+ )
25	24	ex	⊢ ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) → ( 𝐶 = 𝐴 → - 1 ∈ ℝ+ ) )
26	25	necon3bd	⊢ ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) → ( ¬ - 1 ∈ ℝ+ → 𝐶 ≠ 𝐴 ) )
27	13 26	mpi	⊢ ( ( 𝜑 ∧ - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ) → 𝐶 ≠ 𝐴 )
28	27	ex	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ → 𝐶 ≠ 𝐴 ) )
29		necom	⊢ ( 𝐶 ≠ 𝐴 ↔ 𝐴 ≠ 𝐶 )
30	28 29	syl6ib	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ → 𝐴 ≠ 𝐶 ) )
31	7 30	sylbird	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π → 𝐴 ≠ 𝐶 ) )