angpieqvd

Description: The angle ABC is _pi iff B is a nontrivial convex combination of A and C , i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	angpieqvd.angdef	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	angpieqvd.A	$⊢ φ \to A \in ℂ$
	angpieqvd.B	$⊢ φ \to B \in ℂ$
	angpieqvd.C	$⊢ φ \to C \in ℂ$
	angpieqvd.AneB	$⊢ φ \to A \neq B$
	angpieqvd.BneC	$⊢ φ \to B \neq C$
Assertion	angpieqvd	$⊢ φ \to ((A - B) F (C - B) = π \leftrightarrow \exists w \in (0, 1) B = w A + (1 - w) C)$

Proof

Step	Hyp	Ref	Expression
1		angpieqvd.angdef	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		angpieqvd.A	$⊢ φ \to A \in ℂ$
3		angpieqvd.B	$⊢ φ \to B \in ℂ$
4		angpieqvd.C	$⊢ φ \to C \in ℂ$
5		angpieqvd.AneB	$⊢ φ \to A \neq B$
6		angpieqvd.BneC	$⊢ φ \to B \neq C$
7	1 2 3 4 5 6	angpieqvdlem2	$⊢ φ \to (- \frac{C - B}{A - B} \in ℝ^{+} \leftrightarrow (A - B) F (C - B) = π)$
8	7	biimpar	$⊢ (φ \land (A - B) F (C - B) = π) \to - \frac{C - B}{A - B} \in ℝ^{+}$
9	2	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to A \in ℂ$
10	3	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to B \in ℂ$
11	4	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to C \in ℂ$
12	5	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to A \neq B$
13	1 2 3 4 5 6	angpined	$⊢ φ \to ((A - B) F (C - B) = π \to A \neq C)$
14	13	imp	$⊢ (φ \land (A - B) F (C - B) = π) \to A \neq C$
15	9 10 11 12 14	angpieqvdlem	$⊢ (φ \land (A - B) F (C - B) = π) \to (- \frac{C - B}{A - B} \in ℝ^{+} \leftrightarrow \frac{C - B}{C - A} \in (0, 1))$
16	8 15	mpbid	$⊢ (φ \land (A - B) F (C - B) = π) \to \frac{C - B}{C - A} \in (0, 1)$
17	4 3	subcld	$⊢ φ \to C - B \in ℂ$
18	17	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to C - B \in ℂ$
19	4 2	subcld	$⊢ φ \to C - A \in ℂ$
20	19	adantr	$⊢ (φ \land (A - B) F (C - B) = π) \to C - A \in ℂ$
21	14	necomd	$⊢ (φ \land (A - B) F (C - B) = π) \to C \neq A$
22	11 9 21	subne0d	$⊢ (φ \land (A - B) F (C - B) = π) \to C - A \neq 0$
23	18 20 22	divcan1d	$⊢ (φ \land (A - B) F (C - B) = π) \to (\frac{C - B}{C - A}) (C - A) = C - B$
24	23	eqcomd	$⊢ (φ \land (A - B) F (C - B) = π) \to C - B = (\frac{C - B}{C - A}) (C - A)$
25	18 20 22	divcld	$⊢ (φ \land (A - B) F (C - B) = π) \to \frac{C - B}{C - A} \in ℂ$
26	9 10 11 25	affineequiv	$⊢ (φ \land (A - B) F (C - B) = π) \to (B = (\frac{C - B}{C - A}) A + (1 - (\frac{C - B}{C - A})) C \leftrightarrow C - B = (\frac{C - B}{C - A}) (C - A))$
27	24 26	mpbird	$⊢ (φ \land (A - B) F (C - B) = π) \to B = (\frac{C - B}{C - A}) A + (1 - (\frac{C - B}{C - A})) C$
28		oveq1	$⊢ w = \frac{C - B}{C - A} \to w A = (\frac{C - B}{C - A}) A$
29		oveq2	$⊢ w = \frac{C - B}{C - A} \to 1 - w = 1 - (\frac{C - B}{C - A})$
30	29	oveq1d	$⊢ w = \frac{C - B}{C - A} \to (1 - w) C = (1 - (\frac{C - B}{C - A})) C$
31	28 30	oveq12d	$⊢ w = \frac{C - B}{C - A} \to w A + (1 - w) C = (\frac{C - B}{C - A}) A + (1 - (\frac{C - B}{C - A})) C$
32	31	rspceeqv	$⊢ (\frac{C - B}{C - A} \in (0, 1) \land B = (\frac{C - B}{C - A}) A + (1 - (\frac{C - B}{C - A})) C) \to \exists w \in (0, 1) B = w A + (1 - w) C$
33	16 27 32	syl2anc	$⊢ (φ \land (A - B) F (C - B) = π) \to \exists w \in (0, 1) B = w A + (1 - w) C$
34	33	ex	$⊢ φ \to ((A - B) F (C - B) = π \to \exists w \in (0, 1) B = w A + (1 - w) C)$
35	2	adantr	$⊢ (φ \land w \in (0, 1)) \to A \in ℂ$
36	3	adantr	$⊢ (φ \land w \in (0, 1)) \to B \in ℂ$
37	4	adantr	$⊢ (φ \land w \in (0, 1)) \to C \in ℂ$
38		simpr	$⊢ (φ \land w \in (0, 1)) \to w \in (0, 1)$
39		elioore	$⊢ w \in (0, 1) \to w \in ℝ$
40		recn	$⊢ w \in ℝ \to w \in ℂ$
41	38 39 40	3syl	$⊢ (φ \land w \in (0, 1)) \to w \in ℂ$
42	35 36 37 41	affineequiv	$⊢ (φ \land w \in (0, 1)) \to (B = w A + (1 - w) C \leftrightarrow C - B = w (C - A))$
43		simp3	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C - B = w (C - A)$
44	17	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C - B \in ℂ$
45	41	3adant3	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to w \in ℂ$
46	19	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C - A \in ℂ$
47	6	necomd	$⊢ φ \to C \neq B$
48	4 3 47	subne0d	$⊢ φ \to C - B \neq 0$
49	48	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C - B \neq 0$
50	43 49	eqnetrrd	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to w (C - A) \neq 0$
51	45 46 50	mulne0bbd	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C - A \neq 0$
52	44 45 46 51	divmul3d	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to (\frac{C - B}{C - A} = w \leftrightarrow C - B = w (C - A))$
53	43 52	mpbird	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to \frac{C - B}{C - A} = w$
54		simp2	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to w \in (0, 1)$
55	53 54	eqeltrd	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to \frac{C - B}{C - A} \in (0, 1)$
56	2	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to A \in ℂ$
57	3	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to B \in ℂ$
58	4	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C \in ℂ$
59	5	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to A \neq B$
60	58 56 51	subne0ad	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to C \neq A$
61	60	necomd	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to A \neq C$
62	56 57 58 59 61	angpieqvdlem	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to (- \frac{C - B}{A - B} \in ℝ^{+} \leftrightarrow \frac{C - B}{C - A} \in (0, 1))$
63	55 62	mpbird	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to - \frac{C - B}{A - B} \in ℝ^{+}$
64	6	3ad2ant1	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to B \neq C$
65	1 56 57 58 59 64	angpieqvdlem2	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to (- \frac{C - B}{A - B} \in ℝ^{+} \leftrightarrow (A - B) F (C - B) = π)$
66	63 65	mpbid	$⊢ (φ \land w \in (0, 1) \land C - B = w (C - A)) \to (A - B) F (C - B) = π$
67	66	3expia	$⊢ (φ \land w \in (0, 1)) \to (C - B = w (C - A) \to (A - B) F (C - B) = π)$
68	42 67	sylbid	$⊢ (φ \land w \in (0, 1)) \to (B = w A + (1 - w) C \to (A - B) F (C - B) = π)$
69	68	rexlimdva	$⊢ φ \to (\exists w \in (0, 1) B = w A + (1 - w) C \to (A - B) F (C - B) = π)$
70	34 69	impbid	$⊢ φ \to ((A - B) F (C - B) = π \leftrightarrow \exists w \in (0, 1) B = w A + (1 - w) C)$

Metamath Proof Explorer

Theorem angpieqvd

Proof