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	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
	heron.x	$$⊢X=\left|B-C\right|$$
	heron.y	$$⊢Y=\left|A-C\right|$$
	heron.z	$$⊢Z=\left|A-B\right|$$
	heron.o	$$⊢O=\left(B-C\right)F\left(A-C\right)$$
	heron.s	$$⊢S=\frac{X+Y+Z}{2}$$
	heron.a	$$⊢\phi \to A\in ℂ$$
	heron.b	$$⊢\phi \to B\in ℂ$$
	heron.c	$$⊢\phi \to C\in ℂ$$
	heron.ac	$$⊢\phi \to A\ne C$$
	heron.bc	$$⊢\phi \to B\ne C$$
Assertion	heron	$$⊢\phi \to \left(\frac{1}{2}\right)XY\left|\sin O\right|=\sqrt{S\left(S-X\right)\left(S-Y\right)\left(S-Z\right)}$$

Proof

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