Metamath Proof Explorer


Theorem sigardiv

Description: If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017)

Ref Expression
Hypotheses sigar 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
sigardiv.a ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
sigardiv.b ( 𝜑 → ¬ 𝐶 = 𝐴 )
sigardiv.c ( 𝜑 → ( ( 𝐵𝐴 ) 𝐺 ( 𝐶𝐴 ) ) = 0 )
Assertion sigardiv ( 𝜑 → ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 sigar 𝐺 = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( ℑ ‘ ( ( ∗ ‘ 𝑥 ) · 𝑦 ) ) )
2 sigardiv.a ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) )
3 sigardiv.b ( 𝜑 → ¬ 𝐶 = 𝐴 )
4 sigardiv.c ( 𝜑 → ( ( 𝐵𝐴 ) 𝐺 ( 𝐶𝐴 ) ) = 0 )
5 2 simp2d ( 𝜑𝐵 ∈ ℂ )
6 2 simp1d ( 𝜑𝐴 ∈ ℂ )
7 5 6 subcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℂ )
8 2 simp3d ( 𝜑𝐶 ∈ ℂ )
9 8 6 subcld ( 𝜑 → ( 𝐶𝐴 ) ∈ ℂ )
10 3 neqned ( 𝜑𝐶𝐴 )
11 8 6 10 subne0d ( 𝜑 → ( 𝐶𝐴 ) ≠ 0 )
12 7 9 11 cjdivd ( 𝜑 → ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵𝐴 ) ) / ( ∗ ‘ ( 𝐶𝐴 ) ) ) )
13 7 cjcld ( 𝜑 → ( ∗ ‘ ( 𝐵𝐴 ) ) ∈ ℂ )
14 9 cjcld ( 𝜑 → ( ∗ ‘ ( 𝐶𝐴 ) ) ∈ ℂ )
15 9 11 cjne0d ( 𝜑 → ( ∗ ‘ ( 𝐶𝐴 ) ) ≠ 0 )
16 13 14 9 15 11 divcan5rd ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) / ( ( ∗ ‘ ( 𝐶𝐴 ) ) · ( 𝐶𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵𝐴 ) ) / ( ∗ ‘ ( 𝐶𝐴 ) ) ) )
17 13 9 mulcld ( 𝜑 → ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) ∈ ℂ )
18 1 sigarval ( ( ( 𝐵𝐴 ) ∈ ℂ ∧ ( 𝐶𝐴 ) ∈ ℂ ) → ( ( 𝐵𝐴 ) 𝐺 ( 𝐶𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) ) )
19 7 9 18 syl2anc ( 𝜑 → ( ( 𝐵𝐴 ) 𝐺 ( 𝐶𝐴 ) ) = ( ℑ ‘ ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) ) )
20 19 4 eqtr3d ( 𝜑 → ( ℑ ‘ ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) ) = 0 )
21 17 20 reim0bd ( 𝜑 → ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) ∈ ℝ )
22 9 14 mulcomd ( 𝜑 → ( ( 𝐶𝐴 ) · ( ∗ ‘ ( 𝐶𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐶𝐴 ) ) · ( 𝐶𝐴 ) ) )
23 9 cjmulrcld ( 𝜑 → ( ( 𝐶𝐴 ) · ( ∗ ‘ ( 𝐶𝐴 ) ) ) ∈ ℝ )
24 22 23 eqeltrrd ( 𝜑 → ( ( ∗ ‘ ( 𝐶𝐴 ) ) · ( 𝐶𝐴 ) ) ∈ ℝ )
25 14 9 15 11 mulne0d ( 𝜑 → ( ( ∗ ‘ ( 𝐶𝐴 ) ) · ( 𝐶𝐴 ) ) ≠ 0 )
26 21 24 25 redivcld ( 𝜑 → ( ( ( ∗ ‘ ( 𝐵𝐴 ) ) · ( 𝐶𝐴 ) ) / ( ( ∗ ‘ ( 𝐶𝐴 ) ) · ( 𝐶𝐴 ) ) ) ∈ ℝ )
27 16 26 eqeltrrd ( 𝜑 → ( ( ∗ ‘ ( 𝐵𝐴 ) ) / ( ∗ ‘ ( 𝐶𝐴 ) ) ) ∈ ℝ )
28 12 27 eqeltrd ( 𝜑 → ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) ∈ ℝ )
29 28 cjred ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) ) = ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) )
30 7 9 11 divcld ( 𝜑 → ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ∈ ℂ )
31 30 cjcjd ( 𝜑 → ( ∗ ‘ ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) ) = ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) )
32 29 31 eqtr3d ( 𝜑 → ( ∗ ‘ ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ) = ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) )
33 32 28 eqeltrrd ( 𝜑 → ( ( 𝐵𝐴 ) / ( 𝐶𝐴 ) ) ∈ ℝ )