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
|- 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 syl5eq
 |-  ( 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 ) ) ) ) )