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 ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
angpieqvd.A ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
angpieqvd.B ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
angpieqvd.C ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
angpieqvd.AneB ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
angpieqvd.BneC ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion angpieqvd ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ↔ ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) ) )

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 7 biimpar ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )
9 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐴 ∈ ℂ )
10 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐵 ∈ ℂ )
11 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐶 ∈ ℂ )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐴 ≠ 𝐵 )
13 1 2 3 4 5 6 angpined ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π → 𝐴 ≠ 𝐶 ) )
14 13 imp ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐴 ≠ 𝐶 )
15 9 10 11 12 14 angpieqvdlem ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ) )
16 8 15 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) )
17 4 3 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
19 4 2 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ ℂ )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
21 14 necomd ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐶 ≠ 𝐴 )
22 11 9 21 subne0d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( 𝐶 − 𝐴 ) ≠ 0 )
23 18 20 22 divcan1d ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) = ( 𝐶 − 𝐵 ) )
24 23 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( 𝐶 − 𝐵 ) = ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) )
25 18 20 22 divcld ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ℂ )
26 9 10 11 25 affineequiv ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ( 𝐵 = ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · 𝐴 ) + ( ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) · 𝐶 ) ) ↔ ( 𝐶 − 𝐵 ) = ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · ( 𝐶 − 𝐴 ) ) ) )
27 24 26 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → 𝐵 = ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · 𝐴 ) + ( ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) · 𝐶 ) ) )
28 oveq1 ⊢ ( 𝑤 = ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) → ( 𝑤 · 𝐴 ) = ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · 𝐴 ) )
29 oveq2 ⊢ ( 𝑤 = ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) → ( 1 − 𝑤 ) = ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) )
30 29 oveq1d ⊢ ( 𝑤 = ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) → ( ( 1 − 𝑤 ) · 𝐶 ) = ( ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) · 𝐶 ) )
31 28 30 oveq12d ⊢ ( 𝑤 = ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) → ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) = ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · 𝐴 ) + ( ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) · 𝐶 ) ) )
32 31 rspceeqv ⊢ ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ∧ 𝐵 = ( ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) · 𝐴 ) + ( ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ) · 𝐶 ) ) ) → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) )
33 16 27 32 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) )
34 33 ex ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π → ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) ) )
35 2 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → 𝐴 ∈ ℂ )
36 3 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → 𝐵 ∈ ℂ )
37 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → 𝐶 ∈ ℂ )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → 𝑤 ∈ ( 0 (,) 1 ) )
39 elioore ⊢ ( 𝑤 ∈ ( 0 (,) 1 ) → 𝑤 ∈ ℝ )
40 recn ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
41 38 39 40 3syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → 𝑤 ∈ ℂ )
42 35 36 37 41 affineequiv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → ( 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) ↔ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) )
43 simp3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) )
44 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐵 ) ∈ ℂ )
45 41 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝑤 ∈ ℂ )
46 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐴 ) ∈ ℂ )
47 6 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
48 4 3 47 subne0d ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ 0 )
49 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐵 ) ≠ 0 )
50 43 49 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝑤 · ( 𝐶 − 𝐴 ) ) ≠ 0 )
51 45 46 50 mulne0bbd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( 𝐶 − 𝐴 ) ≠ 0 )
52 44 45 46 51 divmul3d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) = 𝑤 ↔ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) )
53 43 52 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) = 𝑤 )
54 simp2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝑤 ∈ ( 0 (,) 1 ) )
55 53 54 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) )
56 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐴 ∈ ℂ )
57 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐵 ∈ ℂ )
58 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐶 ∈ ℂ )
59 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐴 ≠ 𝐵 )
60 58 56 51 subne0ad ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐶 ≠ 𝐴 )
61 60 necomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐴 ≠ 𝐶 )
62 56 57 58 59 61 angpieqvdlem ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ) )
63 55 62 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )
64 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → 𝐵 ≠ 𝐶 )
65 1 56 57 58 59 64 angpieqvdlem2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )
66 63 65 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ∧ ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) ) → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π )
67 66 3expia ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → ( ( 𝐶 − 𝐵 ) = ( 𝑤 · ( 𝐶 − 𝐴 ) ) → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )
68 42 67 sylbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 0 (,) 1 ) ) → ( 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )
69 68 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) → ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ) )
70 34 69 impbid ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) 𝐹 ( 𝐶 − 𝐵 ) ) = π ↔ ∃ 𝑤 ∈ ( 0 (,) 1 ) 𝐵 = ( ( 𝑤 · 𝐴 ) + ( ( 1 − 𝑤 ) · 𝐶 ) ) ) )