Metamath Proof Explorer

Theorem sharhght

Description: Let A B C be a triangle, and let D lie on the line A B . Then (doubled) areas of triangles A D C and C D B relate as lengths of corresponding bases A D and D B . (Contributed by Saveliy Skresanov, 23-Sep-2017)

Ref Expression
Hypotheses sharhght.sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
sharhght.a ⊢ φ → A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ
sharhght.b ⊢ φ → D ∈ ℂ ∧ A − D G B − D = 0
Assertion sharhght ⊢ φ → C − A G D − A ⁢ B − D = C − B G D − B ⁢ A − D

Proof

Step Hyp Ref Expression
1 sharhght.sigar ⊢ G = x ∈ ℂ , y ∈ ℂ ⟼ ℑ ⁡ x ‾ ⁢ y
2 sharhght.a ⊢ φ → A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ
3 sharhght.b ⊢ φ → D ∈ ℂ ∧ A − D G B − D = 0
4 2 simp3d ⊢ φ → C ∈ ℂ
5 2 simp1d ⊢ φ → A ∈ ℂ
6 4 5 subcld ⊢ φ → C − A ∈ ℂ
7 6 adantr ⊢ φ ∧ B = D → C − A ∈ ℂ
8 3 simpld ⊢ φ → D ∈ ℂ
9 8 5 subcld ⊢ φ → D − A ∈ ℂ
10 9 adantr ⊢ φ ∧ B = D → D − A ∈ ℂ
11 1 sigarim ⊢ C − A ∈ ℂ ∧ D − A ∈ ℂ → C − A G D − A ∈ ℝ
12 7 10 11 syl2anc ⊢ φ ∧ B = D → C − A G D − A ∈ ℝ
13 12 recnd ⊢ φ ∧ B = D → C − A G D − A ∈ ℂ
14 13 mul01d ⊢ φ ∧ B = D → C − A G D − A ⋅ 0 = 0
15 2 simp2d ⊢ φ → B ∈ ℂ
16 15 adantr ⊢ φ ∧ B = D → B ∈ ℂ
17 simpr ⊢ φ ∧ B = D → B = D
18 16 17 subeq0bd ⊢ φ ∧ B = D → B − D = 0
19 18 oveq2d ⊢ φ ∧ B = D → C − A G D − A ⁢ B − D = C − A G D − A ⋅ 0
20 4 15 subcld ⊢ φ → C − B ∈ ℂ
21 20 adantr ⊢ φ ∧ B = D → C − B ∈ ℂ
22 8 15 subcld ⊢ φ → D − B ∈ ℂ
23 22 adantr ⊢ φ ∧ B = D → D − B ∈ ℂ
24 1 sigarval ⊢ C − B ∈ ℂ ∧ D − B ∈ ℂ → C − B G D − B = ℑ ⁡ C − B ‾ ⁢ D − B
25 21 23 24 syl2anc ⊢ φ ∧ B = D → C − B G D − B = ℑ ⁡ C − B ‾ ⁢ D − B
26 8 adantr ⊢ φ ∧ B = D → D ∈ ℂ
27 17 eqcomd ⊢ φ ∧ B = D → D = B
28 26 27 subeq0bd ⊢ φ ∧ B = D → D − B = 0
29 28 oveq2d ⊢ φ ∧ B = D → C − B ‾ ⁢ D − B = C − B ‾ ⋅ 0
30 21 cjcld ⊢ φ ∧ B = D → C − B ‾ ∈ ℂ
31 30 mul01d ⊢ φ ∧ B = D → C − B ‾ ⋅ 0 = 0
32 29 31 eqtrd ⊢ φ ∧ B = D → C − B ‾ ⁢ D − B = 0
33 32 fveq2d ⊢ φ ∧ B = D → ℑ ⁡ C − B ‾ ⁢ D − B = ℑ ⁡ 0
34 0red ⊢ φ ∧ B = D → 0 ∈ ℝ
35 34 reim0d ⊢ φ ∧ B = D → ℑ ⁡ 0 = 0
36 25 33 35 3eqtrd ⊢ φ ∧ B = D → C − B G D − B = 0
37 36 oveq1d ⊢ φ ∧ B = D → C − B G D − B ⁢ A − D = 0 ⋅ A − D
38 5 adantr ⊢ φ ∧ B = D → A ∈ ℂ
39 38 26 subcld ⊢ φ ∧ B = D → A − D ∈ ℂ
40 39 mul02d ⊢ φ ∧ B = D → 0 ⋅ A − D = 0
41 37 40 eqtrd ⊢ φ ∧ B = D → C − B G D − B ⁢ A − D = 0
42 14 19 41 3eqtr4d ⊢ φ ∧ B = D → C − A G D − A ⁢ B − D = C − B G D − B ⁢ A − D
43 4 adantr ⊢ φ ∧ ¬ B = D → C ∈ ℂ
44 15 adantr ⊢ φ ∧ ¬ B = D → B ∈ ℂ
45 5 adantr ⊢ φ ∧ ¬ B = D → A ∈ ℂ
46 43 44 45 npncand ⊢ φ ∧ ¬ B = D → C − B + B - A = C − A
47 46 oveq1d ⊢ φ ∧ ¬ B = D → C − B + B - A G D − A = C − A G D − A
48 43 44 subcld ⊢ φ ∧ ¬ B = D → C − B ∈ ℂ
49 9 adantr ⊢ φ ∧ ¬ B = D → D − A ∈ ℂ
50 44 45 subcld ⊢ φ ∧ ¬ B = D → B − A ∈ ℂ
51 1 sigaraf ⊢ C − B ∈ ℂ ∧ D − A ∈ ℂ ∧ B − A ∈ ℂ → C − B + B - A G D − A = C − B G D − A + B − A G D − A
52 48 49 50 51 syl3anc ⊢ φ ∧ ¬ B = D → C − B + B - A G D − A = C − B G D − A + B − A G D − A
53 47 52 eqtr3d ⊢ φ ∧ ¬ B = D → C − A G D − A = C − B G D − A + B − A G D − A
54 3 simprd ⊢ φ → A − D G B − D = 0
55 54 adantr ⊢ φ ∧ ¬ B = D → A − D G B − D = 0
56 8 adantr ⊢ φ ∧ ¬ B = D → D ∈ ℂ
57 1 sigarperm ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A − D G B − D = B − A G D − A
58 45 44 56 57 syl3anc ⊢ φ ∧ ¬ B = D → A − D G B − D = B − A G D − A
59 55 58 eqtr3d ⊢ φ ∧ ¬ B = D → 0 = B − A G D − A
60 59 oveq2d ⊢ φ ∧ ¬ B = D → C − B G D − A + 0 = C − B G D − A + B − A G D − A
61 1 sigarim ⊢ C − B ∈ ℂ ∧ D − A ∈ ℂ → C − B G D − A ∈ ℝ
62 48 49 61 syl2anc ⊢ φ ∧ ¬ B = D → C − B G D − A ∈ ℝ
63 62 recnd ⊢ φ ∧ ¬ B = D → C − B G D − A ∈ ℂ
64 63 addid1d ⊢ φ ∧ ¬ B = D → C − B G D − A + 0 = C − B G D − A
65 53 60 64 3eqtr2d ⊢ φ ∧ ¬ B = D → C − A G D − A = C − B G D − A
66 44 56 negsubdi2d ⊢ φ ∧ ¬ B = D → − B − D = D − B
67 66 eqcomd ⊢ φ ∧ ¬ B = D → D − B = − B − D
68 67 oveq1d ⊢ φ ∧ ¬ B = D → D − B B − D = − B − D B − D
69 44 56 subcld ⊢ φ ∧ ¬ B = D → B − D ∈ ℂ
70 simpr ⊢ φ ∧ ¬ B = D → ¬ B = D
71 70 neqned ⊢ φ ∧ ¬ B = D → B ≠ D
72 44 56 71 subne0d ⊢ φ ∧ ¬ B = D → B − D ≠ 0
73 69 69 72 divnegd ⊢ φ ∧ ¬ B = D → − B − D B − D = − B − D B − D
74 69 72 dividd ⊢ φ ∧ ¬ B = D → B − D B − D = 1
75 74 negeqd ⊢ φ ∧ ¬ B = D → − B − D B − D = − 1
76 68 73 75 3eqtr2d ⊢ φ ∧ ¬ B = D → D − B B − D = − 1
77 76 oveq1d ⊢ φ ∧ ¬ B = D → D − B B − D ⁢ A − D = -1 ⁢ A − D
78 45 56 subcld ⊢ φ ∧ ¬ B = D → A − D ∈ ℂ
79 78 mulm1d ⊢ φ ∧ ¬ B = D → -1 ⁢ A − D = − A − D
80 45 56 negsubdi2d ⊢ φ ∧ ¬ B = D → − A − D = D − A
81 77 79 80 3eqtrd ⊢ φ ∧ ¬ B = D → D − B B − D ⁢ A − D = D − A
82 56 44 subcld ⊢ φ ∧ ¬ B = D → D − B ∈ ℂ
83 82 69 78 72 div32d ⊢ φ ∧ ¬ B = D → D − B B − D ⁢ A − D = D − B ⁢ A − D B − D
84 81 83 eqtr3d ⊢ φ ∧ ¬ B = D → D − A = D − B ⁢ A − D B − D
85 84 oveq2d ⊢ φ ∧ ¬ B = D → C − B G D − A = C − B G D − B ⁢ A − D B − D
86 56 45 44 3jca ⊢ φ ∧ ¬ B = D → D ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ
87 1 86 70 55 sigardiv ⊢ φ ∧ ¬ B = D → A − D B − D ∈ ℝ
88 1 sigarls ⊢ C − B ∈ ℂ ∧ D − B ∈ ℂ ∧ A − D B − D ∈ ℝ → C − B G D − B ⁢ A − D B − D = C − B G D − B ⁢ A − D B − D
89 48 82 87 88 syl3anc ⊢ φ ∧ ¬ B = D → C − B G D − B ⁢ A − D B − D = C − B G D − B ⁢ A − D B − D
90 65 85 89 3eqtrd ⊢ φ ∧ ¬ B = D → C − A G D − A = C − B G D − B ⁢ A − D B − D
91 90 oveq1d ⊢ φ ∧ ¬ B = D → C − A G D − A ⁢ B − D = C − B G D − B ⁢ A − D B − D ⁢ B − D
92 1 sigarim ⊢ C − B ∈ ℂ ∧ D − B ∈ ℂ → C − B G D − B ∈ ℝ
93 92 recnd ⊢ C − B ∈ ℂ ∧ D − B ∈ ℂ → C − B G D − B ∈ ℂ
94 48 82 93 syl2anc ⊢ φ ∧ ¬ B = D → C − B G D − B ∈ ℂ
95 78 69 72 divcld ⊢ φ ∧ ¬ B = D → A − D B − D ∈ ℂ
96 94 95 69 mulassd ⊢ φ ∧ ¬ B = D → C − B G D − B ⁢ A − D B − D ⁢ B − D = C − B G D − B ⁢ A − D B − D ⁢ B − D
97 78 69 72 divcan1d ⊢ φ ∧ ¬ B = D → A − D B − D ⁢ B − D = A − D
98 97 oveq2d ⊢ φ ∧ ¬ B = D → C − B G D − B ⁢ A − D B − D ⁢ B − D = C − B G D − B ⁢ A − D
99 91 96 98 3eqtrd ⊢ φ ∧ ¬ B = D → C − A G D − A ⁢ B − D = C − B G D − B ⁢ A − D
100 42 99 pm2.61dan ⊢ φ → C − A G D − A ⁢ B − D = C − B G D − B ⁢ A − D