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 = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) \|-> ( Im ` ( log ` ( y / x ) ) ) )
	heron.x	\|- X = ( abs ` ( B - C ) )
	heron.y	\|- Y = ( abs ` ( A - C ) )
	heron.z	\|- Z = ( abs ` ( A - B ) )
	heron.o	\|- O = ( ( B - C ) F ( A - C ) )
	heron.s	\|- S = ( ( ( X + Y ) + Z ) / 2 )
	heron.a	\|- ( ph -> A e. CC )
	heron.b	\|- ( ph -> B e. CC )
	heron.c	\|- ( ph -> C e. CC )
	heron.ac	\|- ( ph -> A =/= C )
	heron.bc	\|- ( ph -> B =/= C )
Assertion	heron	\|- ( ph -> ( ( ( 1 / 2 ) x. ( X x. Y ) ) x. ( abs ` ( sin ` O ) ) ) = ( sqrt ` ( ( S x. ( S - X ) ) x. ( ( S - Y ) x. ( S - Z ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem heron

Proof