Metamath Proof Explorer

Theorem heron

Description: Heron's formula gives the area of a triangle given only the side lengths. If points A, B, C form a triangle, then the area of the triangle, represented here as ( 1 / 2 ) x. X x. Y x. abs ( sin O ) , is equal to the square root of S x. ( S - X ) x. ( S - Y ) x. ( S - Z ) , where S = ( X + Y + Z ) / 2 is half the perimeter of the triangle. Based on work by Jon Pennant. This is Metamath 100 proof #57. (Contributed by Mario Carneiro, 10-Mar-2019)

Ref Expression
Hypotheses heron.f ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
heron.x ⊢ 𝑋 = ( abs ‘ ( 𝐵 − 𝐶 ) )
heron.y ⊢ 𝑌 = ( abs ‘ ( 𝐴 − 𝐶 ) )
heron.z ⊢ 𝑍 = ( abs ‘ ( 𝐴 − 𝐵 ) )
heron.o ⊢ 𝑂 = ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) )
heron.s ⊢ 𝑆 = ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 2 )
heron.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
heron.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
heron.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
heron.ac ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
heron.bc ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion heron ( 𝜑 → ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) = ( √ ‘ ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 heron.f ⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 heron.x ⊢ 𝑋 = ( abs ‘ ( 𝐵 − 𝐶 ) )
3 heron.y ⊢ 𝑌 = ( abs ‘ ( 𝐴 − 𝐶 ) )
4 heron.z ⊢ 𝑍 = ( abs ‘ ( 𝐴 − 𝐵 ) )
5 heron.o ⊢ 𝑂 = ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) )
6 heron.s ⊢ 𝑆 = ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 2 )
7 heron.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8 heron.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
9 heron.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
10 heron.ac ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
11 heron.bc ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
12 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
13 12 rehalfcld ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
14 8 9 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
15 14 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐵 − 𝐶 ) ) ∈ ℝ )
16 2 15 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
17 7 9 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
18 17 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐶 ) ) ∈ ℝ )
19 3 18 eqeltrid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
20 16 19 remulcld ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ℝ )
21 13 20 remulcld ⊢ ( 𝜑 → ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ∈ ℝ )
22 negpitopissre ⊢ ( - π (,] π ) ⊆ ℝ
23 8 9 11 subne0d ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ≠ 0 )
24 7 9 10 subne0d ⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ≠ 0 )
25 1 14 23 17 24 angcld ⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) ∈ ( - π (,] π ) )
26 22 25 sselid ⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) ∈ ℝ )
27 26 recnd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) 𝐹 ( 𝐴 − 𝐶 ) ) ∈ ℂ )
28 5 27 eqeltrid ⊢ ( 𝜑 → 𝑂 ∈ ℂ )
29 28 sincld ⊢ ( 𝜑 → ( sin ‘ 𝑂 ) ∈ ℂ )
30 29 abscld ⊢ ( 𝜑 → ( abs ‘ ( sin ‘ 𝑂 ) ) ∈ ℝ )
31 21 30 remulcld ⊢ ( 𝜑 → ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) ∈ ℝ )
32 halfge0 ⊢ 0 ≤ ( 1 / 2 )
33 32 a1i ⊢ ( 𝜑 → 0 ≤ ( 1 / 2 ) )
34 14 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐵 − 𝐶 ) ) )
35 34 2 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑋 )
36 17 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 𝐴 − 𝐶 ) ) )
37 36 3 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑌 )
38 16 19 35 37 mulge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑋 · 𝑌 ) )
39 13 20 33 38 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) )
40 29 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( sin ‘ 𝑂 ) ) )
41 21 30 39 40 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) )
42 31 41 sqrtsqd ⊢ ( 𝜑 → ( √ ‘ ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) ↑ 2 ) ) = ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) )
43 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
44 43 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
45 16 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
46 19 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
47 45 46 mulcld ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ ℂ )
48 44 47 mulcld ⊢ ( 𝜑 → ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ∈ ℂ )
49 30 recnd ⊢ ( 𝜑 → ( abs ‘ ( sin ‘ 𝑂 ) ) ∈ ℂ )
50 48 49 sqmuld ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) ↑ 2 ) = ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( abs ‘ ( sin ‘ 𝑂 ) ) ↑ 2 ) ) )
51 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
52 2ne0 ⊢ 2 ≠ 0
53 52 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
54 47 51 53 sqdivd ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) / 2 ) ↑ 2 ) = ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / ( 2 ↑ 2 ) ) )
55 47 51 53 divrec2d ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) / 2 ) = ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) )
56 55 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) / 2 ) ↑ 2 ) = ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ↑ 2 ) )
57 sq2 ⊢ ( 2 ↑ 2 ) = 4
58 57 a1i ⊢ ( 𝜑 → ( 2 ↑ 2 ) = 4 )
59 58 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / 4 ) )
60 54 56 59 3eqtr3d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / 4 ) )
61 5 26 eqeltrid ⊢ ( 𝜑 → 𝑂 ∈ ℝ )
62 61 resincld ⊢ ( 𝜑 → ( sin ‘ 𝑂 ) ∈ ℝ )
63 absresq ⊢ ( ( sin ‘ 𝑂 ) ∈ ℝ → ( ( abs ‘ ( sin ‘ 𝑂 ) ) ↑ 2 ) = ( ( sin ‘ 𝑂 ) ↑ 2 ) )
64 62 63 syl ⊢ ( 𝜑 → ( ( abs ‘ ( sin ‘ 𝑂 ) ) ↑ 2 ) = ( ( sin ‘ 𝑂 ) ↑ 2 ) )
65 60 64 oveq12d ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( abs ‘ ( sin ‘ 𝑂 ) ) ↑ 2 ) ) = ( ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / 4 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) )
66 47 sqcld ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ↑ 2 ) ∈ ℂ )
67 29 sqcld ⊢ ( 𝜑 → ( ( sin ‘ 𝑂 ) ↑ 2 ) ∈ ℂ )
68 66 67 mulcld ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) ∈ ℂ )
69 4cn ⊢ 4 ∈ ℂ
70 69 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
71 16 19 readdcld ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ℝ )
72 7 8 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
73 72 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
74 4 73 eqeltrid ⊢ ( 𝜑 → 𝑍 ∈ ℝ )
75 71 74 readdcld ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℝ )
76 75 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 2 ) ∈ ℝ )
77 6 76 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
78 77 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
79 78 45 subcld ⊢ ( 𝜑 → ( 𝑆 − 𝑋 ) ∈ ℂ )
80 78 79 mulcld ⊢ ( 𝜑 → ( 𝑆 · ( 𝑆 − 𝑋 ) ) ∈ ℂ )
81 78 46 subcld ⊢ ( 𝜑 → ( 𝑆 − 𝑌 ) ∈ ℂ )
82 74 recnd ⊢ ( 𝜑 → 𝑍 ∈ ℂ )
83 78 82 subcld ⊢ ( 𝜑 → ( 𝑆 − 𝑍 ) ∈ ℂ )
84 81 83 mulcld ⊢ ( 𝜑 → ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ∈ ℂ )
85 80 84 mulcld ⊢ ( 𝜑 → ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ∈ ℂ )
86 70 85 mulcld ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ∈ ℂ )
87 4ne0 ⊢ 4 ≠ 0
88 87 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
89 51 47 sqmuld ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) )
90 58 oveq1d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) = ( 4 · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) )
91 89 90 eqtr2d ⊢ ( 𝜑 → ( 4 · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) = ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) )
92 91 oveq1d ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) )
93 70 66 67 mulassd ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( 4 · ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) ) )
94 51 47 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝑋 · 𝑌 ) ) ∈ ℂ )
95 94 sqcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ∈ ℂ )
96 95 67 mulcld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) ∈ ℂ )
97 46 82 mulcld ⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) ∈ ℂ )
98 51 97 mulcld ⊢ ( 𝜑 → ( 2 · ( 𝑌 · 𝑍 ) ) ∈ ℂ )
99 98 sqcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) ∈ ℂ )
100 46 sqcld ⊢ ( 𝜑 → ( 𝑌 ↑ 2 ) ∈ ℂ )
101 82 sqcld ⊢ ( 𝜑 → ( 𝑍 ↑ 2 ) ∈ ℂ )
102 45 sqcld ⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
103 101 102 subcld ⊢ ( 𝜑 → ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ∈ ℂ )
104 100 103 addcld ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
105 104 sqcld ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ∈ ℂ )
106 99 105 subcld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) ∈ ℂ )
107 28 coscld ⊢ ( 𝜑 → ( cos ‘ 𝑂 ) ∈ ℂ )
108 107 sqcld ⊢ ( 𝜑 → ( ( cos ‘ 𝑂 ) ↑ 2 ) ∈ ℂ )
109 95 108 mulcld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ∈ ℂ )
110 sincossq ⊢ ( 𝑂 ∈ ℂ → ( ( ( sin ‘ 𝑂 ) ↑ 2 ) + ( ( cos ‘ 𝑂 ) ↑ 2 ) ) = 1 )
111 28 110 syl ⊢ ( 𝜑 → ( ( ( sin ‘ 𝑂 ) ↑ 2 ) + ( ( cos ‘ 𝑂 ) ↑ 2 ) ) = 1 )
112 111 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( ( sin ‘ 𝑂 ) ↑ 2 ) + ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) = ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · 1 ) )
113 95 67 108 adddid ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( ( sin ‘ 𝑂 ) ↑ 2 ) + ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) = ( ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) + ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) )
114 100 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝑌 ↑ 2 ) ) = ( ( 𝑌 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
115 100 103 100 ppncand ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) + ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( 𝑌 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) )
116 114 115 eqtr4d ⊢ ( 𝜑 → ( 2 · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) + ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
117 103 2timesd ⊢ ( 𝜑 → ( 2 · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) )
118 100 103 103 pnncand ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) − ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) )
119 117 118 eqtr4d ⊢ ( 𝜑 → ( 2 · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) − ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
120 116 119 oveq12d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 ↑ 2 ) ) · ( 2 · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) + ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) − ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) )
121 2t2e4 ⊢ ( 2 · 2 ) = 4
122 121 70 eqeltrid ⊢ ( 𝜑 → ( 2 · 2 ) ∈ ℂ )
123 122 100 103 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
124 122 100 mulcld ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ )
125 124 101 102 subdid ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑍 ↑ 2 ) ) − ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) ) )
126 51 sqvald ⊢ ( 𝜑 → ( 2 ↑ 2 ) = ( 2 · 2 ) )
127 46 82 sqmuld ⊢ ( 𝜑 → ( ( 𝑌 · 𝑍 ) ↑ 2 ) = ( ( 𝑌 ↑ 2 ) · ( 𝑍 ↑ 2 ) ) )
128 126 127 oveq12d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝑌 · 𝑍 ) ↑ 2 ) ) = ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( 𝑍 ↑ 2 ) ) ) )
129 51 97 sqmuld ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑌 · 𝑍 ) ↑ 2 ) ) )
130 122 100 101 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑍 ↑ 2 ) ) = ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( 𝑍 ↑ 2 ) ) ) )
131 128 129 130 3eqtr4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) = ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑍 ↑ 2 ) ) )
132 45 46 sqmuld ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ↑ 2 ) = ( ( 𝑋 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) )
133 102 100 mulcomd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) = ( ( 𝑌 ↑ 2 ) · ( 𝑋 ↑ 2 ) ) )
134 132 133 eqtrd ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ↑ 2 ) = ( ( 𝑌 ↑ 2 ) · ( 𝑋 ↑ 2 ) ) )
135 126 134 oveq12d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝑋 · 𝑌 ) ↑ 2 ) ) = ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( 𝑋 ↑ 2 ) ) ) )
136 122 100 102 mulassd ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) = ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( 𝑋 ↑ 2 ) ) ) )
137 135 89 136 3eqtr4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) = ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) )
138 131 137 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) = ( ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑍 ↑ 2 ) ) − ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( 𝑋 ↑ 2 ) ) ) )
139 125 138 eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · 2 ) · ( 𝑌 ↑ 2 ) ) · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) )
140 51 51 100 103 mul4d ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( ( 𝑌 ↑ 2 ) · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( 2 · ( 𝑌 ↑ 2 ) ) · ( 2 · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
141 123 139 140 3eqtr3d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) = ( ( 2 · ( 𝑌 ↑ 2 ) ) · ( 2 · ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
142 100 103 subcld ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ∈ ℂ )
143 subsq ⊢ ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ∈ ℂ ∧ ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) + ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) − ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) )
144 104 142 143 syl2anc ⊢ ( 𝜑 → ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) = ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) + ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) − ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) )
145 120 141 144 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) = ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) )
146 145 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) ) )
147 99 95 nncand ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) ) ) = ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) )
148 142 sqcld ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ∈ ℂ )
149 99 105 148 subsubd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) ) = ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) )
150 146 147 149 3eqtr3d ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) = ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) )
151 95 mulid1d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · 1 ) = ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) )
152 102 100 addcld ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ∈ ℂ )
153 47 107 mulcld ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ∈ ℂ )
154 51 153 mulcld ⊢ ( 𝜑 → ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ∈ ℂ )
155 152 154 nncand ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) ) = ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) )
156 100 101 subcld ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( 𝑍 ↑ 2 ) ) ∈ ℂ )
157 156 102 addcomd ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) − ( 𝑍 ↑ 2 ) ) + ( 𝑋 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 𝑌 ↑ 2 ) − ( 𝑍 ↑ 2 ) ) ) )
158 100 101 102 subsubd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 𝑌 ↑ 2 ) − ( 𝑍 ↑ 2 ) ) + ( 𝑋 ↑ 2 ) ) )
159 102 100 101 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 𝑍 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 𝑌 ↑ 2 ) − ( 𝑍 ↑ 2 ) ) ) )
160 157 158 159 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 𝑍 ↑ 2 ) ) )
161 1 2 3 4 5 lawcos ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( 𝑍 ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) )
162 7 8 9 10 11 161 syl32anc ⊢ ( 𝜑 → ( 𝑍 ↑ 2 ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) )
163 162 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 𝑍 ↑ 2 ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) ) )
164 160 163 eqtrd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) − ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) ) ) )
165 51 47 107 mulassd ⊢ ( 𝜑 → ( ( 2 · ( 𝑋 · 𝑌 ) ) · ( cos ‘ 𝑂 ) ) = ( 2 · ( ( 𝑋 · 𝑌 ) · ( cos ‘ 𝑂 ) ) ) )
166 155 164 165 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) = ( ( 2 · ( 𝑋 · 𝑌 ) ) · ( cos ‘ 𝑂 ) ) )
167 166 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) = ( ( ( 2 · ( 𝑋 · 𝑌 ) ) · ( cos ‘ 𝑂 ) ) ↑ 2 ) )
168 94 107 sqmuld ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) · ( cos ‘ 𝑂 ) ) ↑ 2 ) = ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) )
169 167 168 eqtr2d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) = ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) )
170 169 oveq2d ⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) = ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 𝑌 ↑ 2 ) − ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) )
171 150 151 170 3eqtr4d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · 1 ) = ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) )
172 112 113 171 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) + ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) = ( ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) + ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( cos ‘ 𝑂 ) ↑ 2 ) ) ) )
173 96 106 109 172 addcan2ad ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) )
174 subsq ⊢ ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ∈ ℂ ∧ ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) )
175 98 104 174 syl2anc ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ↑ 2 ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) )
176 100 101 addcld ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ∈ ℂ )
177 98 176 102 addsubassd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) − ( 𝑋 ↑ 2 ) ) = ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 𝑋 ↑ 2 ) ) ) )
178 100 101 102 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 𝑋 ↑ 2 ) ) = ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) )
179 178 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 𝑋 ↑ 2 ) ) ) = ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
180 177 179 eqtr2d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) − ( 𝑋 ↑ 2 ) ) )
181 binom2 ⊢ ( ( 𝑌 ∈ ℂ ∧ 𝑍 ∈ ℂ ) → ( ( 𝑌 + 𝑍 ) ↑ 2 ) = ( ( ( 𝑌 ↑ 2 ) + ( 2 · ( 𝑌 · 𝑍 ) ) ) + ( 𝑍 ↑ 2 ) ) )
182 46 82 181 syl2anc ⊢ ( 𝜑 → ( ( 𝑌 + 𝑍 ) ↑ 2 ) = ( ( ( 𝑌 ↑ 2 ) + ( 2 · ( 𝑌 · 𝑍 ) ) ) + ( 𝑍 ↑ 2 ) ) )
183 100 98 101 add32d ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 2 · ( 𝑌 · 𝑍 ) ) ) + ( 𝑍 ↑ 2 ) ) = ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) + ( 2 · ( 𝑌 · 𝑍 ) ) ) )
184 176 98 addcomd ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) + ( 2 · ( 𝑌 · 𝑍 ) ) ) = ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) )
185 182 183 184 3eqtrd ⊢ ( 𝜑 → ( ( 𝑌 + 𝑍 ) ↑ 2 ) = ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) )
186 185 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 + 𝑍 ) ↑ 2 ) − ( 𝑋 ↑ 2 ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) − ( 𝑋 ↑ 2 ) ) )
187 46 82 addcld ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ ℂ )
188 subsq ⊢ ( ( ( 𝑌 + 𝑍 ) ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( ( 𝑌 + 𝑍 ) ↑ 2 ) − ( 𝑋 ↑ 2 ) ) = ( ( ( 𝑌 + 𝑍 ) + 𝑋 ) · ( ( 𝑌 + 𝑍 ) − 𝑋 ) ) )
189 187 45 188 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑌 + 𝑍 ) ↑ 2 ) − ( 𝑋 ↑ 2 ) ) = ( ( ( 𝑌 + 𝑍 ) + 𝑋 ) · ( ( 𝑌 + 𝑍 ) − 𝑋 ) ) )
190 6 oveq2i ⊢ ( 2 · 𝑆 ) = ( 2 · ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 2 ) )
191 75 recnd ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∈ ℂ )
192 191 51 53 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) / 2 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
193 190 192 syl5eq ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
194 45 46 82 addassd ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
195 45 187 addcomd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑌 + 𝑍 ) + 𝑋 ) )
196 193 194 195 3eqtrd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( ( 𝑌 + 𝑍 ) + 𝑋 ) )
197 51 78 45 subdid ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑋 ) ) = ( ( 2 · 𝑆 ) − ( 2 · 𝑋 ) ) )
198 193 194 eqtrd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
199 45 2timesd ⊢ ( 𝜑 → ( 2 · 𝑋 ) = ( 𝑋 + 𝑋 ) )
200 198 199 oveq12d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) − ( 2 · 𝑋 ) ) = ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) − ( 𝑋 + 𝑋 ) ) )
201 45 187 45 pnpcand ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) − ( 𝑋 + 𝑋 ) ) = ( ( 𝑌 + 𝑍 ) − 𝑋 ) )
202 197 200 201 3eqtrd ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑋 ) ) = ( ( 𝑌 + 𝑍 ) − 𝑋 ) )
203 196 202 oveq12d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) · ( 2 · ( 𝑆 − 𝑋 ) ) ) = ( ( ( 𝑌 + 𝑍 ) + 𝑋 ) · ( ( 𝑌 + 𝑍 ) − 𝑋 ) ) )
204 189 203 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑌 + 𝑍 ) ↑ 2 ) − ( 𝑋 ↑ 2 ) ) = ( ( 2 · 𝑆 ) · ( 2 · ( 𝑆 − 𝑋 ) ) ) )
205 51 78 51 79 mul4d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) · ( 2 · ( 𝑆 − 𝑋 ) ) ) = ( ( 2 · 2 ) · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) )
206 121 a1i ⊢ ( 𝜑 → ( 2 · 2 ) = 4 )
207 206 oveq1d ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) = ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) )
208 204 205 207 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 + 𝑍 ) ↑ 2 ) − ( 𝑋 ↑ 2 ) ) = ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) )
209 180 186 208 3eqtr2d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) )
210 98 176 subcld ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) ∈ ℂ )
211 210 102 addcomd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) + ( 𝑋 ↑ 2 ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) ) )
212 178 oveq2d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 𝑋 ↑ 2 ) ) ) = ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) )
213 98 176 102 subsubd ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 𝑋 ↑ 2 ) ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) + ( 𝑋 ↑ 2 ) ) )
214 212 213 eqtr3d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) + ( 𝑋 ↑ 2 ) ) )
215 102 176 98 subsub2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ) = ( ( 𝑋 ↑ 2 ) + ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) ) ) )
216 211 214 215 3eqtr4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ) )
217 100 101 98 addsubassd ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) = ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ) )
218 101 98 subcld ⊢ ( 𝜑 → ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ∈ ℂ )
219 100 218 addcomd ⊢ ( 𝜑 → ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ) = ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) + ( 𝑌 ↑ 2 ) ) )
220 46 82 mulcomd ⊢ ( 𝜑 → ( 𝑌 · 𝑍 ) = ( 𝑍 · 𝑌 ) )
221 220 oveq2d ⊢ ( 𝜑 → ( 2 · ( 𝑌 · 𝑍 ) ) = ( 2 · ( 𝑍 · 𝑌 ) ) )
222 221 oveq2d ⊢ ( 𝜑 → ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) = ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑍 · 𝑌 ) ) ) )
223 222 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) + ( 𝑌 ↑ 2 ) ) = ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑍 · 𝑌 ) ) ) + ( 𝑌 ↑ 2 ) ) )
224 217 219 223 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) = ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑍 · 𝑌 ) ) ) + ( 𝑌 ↑ 2 ) ) )
225 binom2sub ⊢ ( ( 𝑍 ∈ ℂ ∧ 𝑌 ∈ ℂ ) → ( ( 𝑍 − 𝑌 ) ↑ 2 ) = ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑍 · 𝑌 ) ) ) + ( 𝑌 ↑ 2 ) ) )
226 82 46 225 syl2anc ⊢ ( 𝜑 → ( ( 𝑍 − 𝑌 ) ↑ 2 ) = ( ( ( 𝑍 ↑ 2 ) − ( 2 · ( 𝑍 · 𝑌 ) ) ) + ( 𝑌 ↑ 2 ) ) )
227 224 226 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) = ( ( 𝑍 − 𝑌 ) ↑ 2 ) )
228 227 oveq2d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( ( ( 𝑌 ↑ 2 ) + ( 𝑍 ↑ 2 ) ) − ( 2 · ( 𝑌 · 𝑍 ) ) ) ) = ( ( 𝑋 ↑ 2 ) − ( ( 𝑍 − 𝑌 ) ↑ 2 ) ) )
229 82 46 subcld ⊢ ( 𝜑 → ( 𝑍 − 𝑌 ) ∈ ℂ )
230 subsq ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑍 − 𝑌 ) ∈ ℂ ) → ( ( 𝑋 ↑ 2 ) − ( ( 𝑍 − 𝑌 ) ↑ 2 ) ) = ( ( 𝑋 + ( 𝑍 − 𝑌 ) ) · ( 𝑋 − ( 𝑍 − 𝑌 ) ) ) )
231 45 229 230 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( ( 𝑍 − 𝑌 ) ↑ 2 ) ) = ( ( 𝑋 + ( 𝑍 − 𝑌 ) ) · ( 𝑋 − ( 𝑍 − 𝑌 ) ) ) )
232 51 78 46 subdid ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑌 ) ) = ( ( 2 · 𝑆 ) − ( 2 · 𝑌 ) ) )
233 45 46 82 add32d ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑍 ) + 𝑌 ) )
234 193 233 eqtrd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( ( 𝑋 + 𝑍 ) + 𝑌 ) )
235 46 2timesd ⊢ ( 𝜑 → ( 2 · 𝑌 ) = ( 𝑌 + 𝑌 ) )
236 234 235 oveq12d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) − ( 2 · 𝑌 ) ) = ( ( ( 𝑋 + 𝑍 ) + 𝑌 ) − ( 𝑌 + 𝑌 ) ) )
237 45 82 addcld ⊢ ( 𝜑 → ( 𝑋 + 𝑍 ) ∈ ℂ )
238 237 46 46 pnpcan2d ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑍 ) + 𝑌 ) − ( 𝑌 + 𝑌 ) ) = ( ( 𝑋 + 𝑍 ) − 𝑌 ) )
239 45 82 46 238 assraddsubd ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑍 ) + 𝑌 ) − ( 𝑌 + 𝑌 ) ) = ( 𝑋 + ( 𝑍 − 𝑌 ) ) )
240 232 236 239 3eqtrd ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑌 ) ) = ( 𝑋 + ( 𝑍 − 𝑌 ) ) )
241 51 78 82 subdid ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑍 ) ) = ( ( 2 · 𝑆 ) − ( 2 · 𝑍 ) ) )
242 82 2timesd ⊢ ( 𝜑 → ( 2 · 𝑍 ) = ( 𝑍 + 𝑍 ) )
243 193 242 oveq12d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) − ( 2 · 𝑍 ) ) = ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) − ( 𝑍 + 𝑍 ) ) )
244 45 46 addcld ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ℂ )
245 244 82 82 pnpcan2d ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) − ( 𝑍 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) − 𝑍 ) )
246 45 82 46 subsub3d ⊢ ( 𝜑 → ( 𝑋 − ( 𝑍 − 𝑌 ) ) = ( ( 𝑋 + 𝑌 ) − 𝑍 ) )
247 245 246 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) − ( 𝑍 + 𝑍 ) ) = ( 𝑋 − ( 𝑍 − 𝑌 ) ) )
248 241 243 247 3eqtrd ⊢ ( 𝜑 → ( 2 · ( 𝑆 − 𝑍 ) ) = ( 𝑋 − ( 𝑍 − 𝑌 ) ) )
249 240 248 oveq12d ⊢ ( 𝜑 → ( ( 2 · ( 𝑆 − 𝑌 ) ) · ( 2 · ( 𝑆 − 𝑍 ) ) ) = ( ( 𝑋 + ( 𝑍 − 𝑌 ) ) · ( 𝑋 − ( 𝑍 − 𝑌 ) ) ) )
250 231 249 eqtr4d ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( ( 𝑍 − 𝑌 ) ↑ 2 ) ) = ( ( 2 · ( 𝑆 − 𝑌 ) ) · ( 2 · ( 𝑆 − 𝑍 ) ) ) )
251 51 81 51 83 mul4d ⊢ ( 𝜑 → ( ( 2 · ( 𝑆 − 𝑌 ) ) · ( 2 · ( 𝑆 − 𝑍 ) ) ) = ( ( 2 · 2 ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
252 206 oveq1d ⊢ ( 𝜑 → ( ( 2 · 2 ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) = ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
253 250 251 252 3eqtrd ⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) − ( ( 𝑍 − 𝑌 ) ↑ 2 ) ) = ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
254 216 228 253 3eqtrd ⊢ ( 𝜑 → ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) = ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
255 209 254 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑌 · 𝑍 ) ) + ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) · ( ( 2 · ( 𝑌 · 𝑍 ) ) − ( ( 𝑌 ↑ 2 ) + ( ( 𝑍 ↑ 2 ) − ( 𝑋 ↑ 2 ) ) ) ) ) = ( ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )
256 173 175 255 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )
257 70 84 mulcld ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ∈ ℂ )
258 70 80 257 mulassd ⊢ ( 𝜑 → ( ( 4 · ( 𝑆 · ( 𝑆 − 𝑋 ) ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) = ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ) )
259 80 70 84 mul12d ⊢ ( 𝜑 → ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) = ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )
260 259 oveq2d ⊢ ( 𝜑 → ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( 4 · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ) = ( 4 · ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ) )
261 256 258 260 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · ( 𝑋 · 𝑌 ) ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( 4 · ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ) )
262 92 93 261 3eqtr3d ⊢ ( 𝜑 → ( 4 · ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) ) = ( 4 · ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) ) )
263 68 86 70 88 262 mulcanad ⊢ ( 𝜑 → ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )
264 263 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) / 4 ) = ( ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) / 4 ) )
265 66 67 70 88 div23d ⊢ ( 𝜑 → ( ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) / 4 ) = ( ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / 4 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) )
266 77 16 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑋 ) ∈ ℝ )
267 77 266 remulcld ⊢ ( 𝜑 → ( 𝑆 · ( 𝑆 − 𝑋 ) ) ∈ ℝ )
268 77 19 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑌 ) ∈ ℝ )
269 77 74 resubcld ⊢ ( 𝜑 → ( 𝑆 − 𝑍 ) ∈ ℝ )
270 268 269 remulcld ⊢ ( 𝜑 → ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ∈ ℝ )
271 267 270 remulcld ⊢ ( 𝜑 → ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ∈ ℝ )
272 271 recnd ⊢ ( 𝜑 → ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ∈ ℂ )
273 272 70 88 divcan3d ⊢ ( 𝜑 → ( ( 4 · ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) / 4 ) = ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
274 264 265 273 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝑋 · 𝑌 ) ↑ 2 ) / 4 ) · ( ( sin ‘ 𝑂 ) ↑ 2 ) ) = ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
275 50 65 274 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) ↑ 2 ) = ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) )
276 275 fveq2d ⊢ ( 𝜑 → ( √ ‘ ( ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) ↑ 2 ) ) = ( √ ‘ ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )
277 42 276 eqtr3d ⊢ ( 𝜑 → ( ( ( 1 / 2 ) · ( 𝑋 · 𝑌 ) ) · ( abs ‘ ( sin ‘ 𝑂 ) ) ) = ( √ ‘ ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )