John, I'm now certain that your proof of TRIANGLE_ANGLE_SUM_LEMMA is pretty much what I posted yesterday. I was confused about LAW_OF_COSINES, a vector triviality which I actually used. Here's a better proof that my son & I worked out today. Which is to say, I gave it to him as a guided exercise, and he came up with some simplifications I didn't expect. I think this is a really nice proof, and one I was completely unaware of, and it's due to you and HOL Light.
Let A, B & C be non-collinear points in R^2, with angles α, β & γ next to the vertices respectively, and opposite sides a, b & c resp. Let u, v & w be the vectors u = C - B v = A - C w = C - B Then w = u + v, |u| = a, |v| = b and |c| = |w|. By LAW_OF_COSINES, c^2 = a^2 + b^2 + 2(u dot v) and this is just the vector triviality, the distributivity of the dot product over addition, c^2 = |w|^2 = w dot w = (u + v) dot (u + v) = |u|^2 + 2(u dot v) + |v|^2 Then by ANGLE cos α = (v dot w) / (bc), cos β = (u dot w) / (ac), cos γ = - (u dot v) / (ab), since - v = C - A, and so cos α cos β cos γ = - (u dot v) (u dot w) (v dot w) / (a^2 b^2 c^2) . By LAW_OF_SINES and the above cos α sin β sin γ = (v dot w) (b^2 c^2 - (v dot w)^2) / (a^2 b^2 c^2) cos β sin α sin γ = (u dot w) (a^2 c^2 - (u dot w)^2) / (a^2 b^2 c^2) cos γ sin α sin β = - (u dot v) (a^2 b^2 - (u dot v)^2) / (a^2 b^2 c^2) By COS_ADD & SIN_ADD cos(α + β + γ) = cos(α) cos(β + γ) - sin(α) sin(β + γ) = cos α cos β cos γ - (cos α sin β sin γ + cos β sin α sin γ + cos γ sin α sin β) so a^2 b^2 c^2 cos(α + β + γ) = - (u dot v) (u dot w) (v dot w) + (u dot v) (a^2 b^2 - (u dot v)^2) - (v dot w) (b^2 c^2 - (v dot w)^2) - (u dot w) (a^2 c^2 - (u dot w)^2) The plan is to eliminate w and c, by w = u + v, c^2 = a^2 + b^2 + 2(u dot v). It's easier to read if we write d = u dot v. Then u dot w = a^2 + d v dot w = b^2 + d so a^2 b^2 c^2 cos(α + β + γ) = - d (a^2 + d) (b^2 + d) + d (a^2 b^2 - d^2) - (b^2 + d) (b^2 c^2 - (b^2 + d)^2) - (a^2 + d) (a^2 c^2 - (a^2 + d)^2) Now a^2 c^2 - (a^2 + d)^2 = a^2(a^2 + b^2 + 2d) - (a^4 + 2a^d + d^2) = a^2 b^2 - d^2 similarly b^2 c^2 - (b^2 + d)^2 = a^2 b^2 - d^2 Factoring the common a^2 b^2 - d^2 and using c^2 = b^2 + a^2 + 2d, we have a^2 b^2 c^2 cos(α + β + γ) = - d (a^2 + d) (b^2 + d) + d (a^2 b^2 - d^2) - c^2 (a^2 b^2 - d^2) = - a^2 b^2c^2 - d^2(a^2 + b^2) - 2d^3 + c^2 d^2 = - a^2 b^2c^2 - d^2(a^2 + b^2 + 2d - c^2) = - a^2 b^2c^2 Thus cos(α + β + γ) = -1. That's an amazing proof, John! Thanks for teaching it to me, through HOL Light! Now back to possible secret Hilbert betweenness. It would be no trouble to prove all the Hilbert betweenness in coordinate geometry, and you prove some later in e.g. ANGLES_ADD_BETWEEN, but I am curious. You defined e^z, sin(x), cos(x) by power series and therefore proved COS_ADD & SIN_ADD. ANGLE follows from the definition of angles, i.e. vector_angle which uses acs, arc-cos. So it's all Calculus so far, and that's great. The LAW_OF_COSINES is just vector properties, so all that's left, I think, is LAW_OF_SINES, which actually sounds geometric, and has a long interesting looking proof. -- Best, Bill ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_nov _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
