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 y x
angpieqvd.A φ A
angpieqvd.B φ B
angpieqvd.C φ C
angpieqvd.AneB φ A B
angpieqvd.BneC φ B C
Assertion angpieqvd φ A B F C B = π w 0 1 B = w A + 1 w C

Proof

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