Metamath Proof Explorer

Theorem 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∈ℂ∖0,y∈ℂ∖0⟼ℑ⁡log⁡yx
angpieqvd.A ⊢φ→A∈ℂ
angpieqvd.B ⊢φ→B∈ℂ
angpieqvd.C ⊢φ→C∈ℂ
angpieqvd.AneB ⊢φ→A≠B
angpieqvd.BneC ⊢φ→B≠C
Assertion angpieqvd ⊢φ→A−BFC−B=π↔∃w∈01B=w⁢A+1−w⁢C

Proof

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