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	mulridd	⊢ ( 𝜑 → ( ( ( 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	eqtrid	⊢ ( 𝜑 → ( 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 ‘ 𝑂 ) ) ) = ( √ ‘ ( ( 𝑆 · ( 𝑆 − 𝑋 ) ) · ( ( 𝑆 − 𝑌 ) · ( 𝑆 − 𝑍 ) ) ) ) )