More thoughts - in a new thread as suggested by Benoît.
Have you thought what your final theorem statement would be?
I assume you're shooting for something like areacirc and arearect, in
the form of
( area ` S ) = ...
Where S is our triangle (as a subset of ( RR X. RR ) ), and what's after
the equal sign is the formula giving the area.
Like in Heron's formula, it would be interesting to start from three
complex numbers A, B, and C. Here is what I came up with:
|- ( ph -> A e. CC )
|- ( ph -> B e. CC )
|- ( ph -> C e. CC )
|- X = ( Re ` ( B - C ) )
|- Y = ( Im ` ( B - C ) )
|- Z = ( Re ` ( A - C ) )
|- T = ( Im ` ( A - C ) )
|- D = ( ( Z x. Y ) - ( T x. X ) )
|- U = ( x - ( Re ` C) )
|- V = ( y - ( Im ` C) )
|- E = ( ( Y x. U ) - ( X x. V ) )
|- F = ( ( T x. U ) - ( Z x. V ) )
|- S = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ ( E e. ( 0 [,] D
) /\ F e. ( 0 [,] D ) ) ) }
|- ( ph -> ( area ` S ) = ( ( abs ` D ) / 2 ) )
Or did you have something else in mind, e.g. where the "height" and
"base" of the triangle are explicit?
Here's a quote from Mario (from earlier on this thread), I think it's
still very valid here:
Here's a question for you, and I think that thinking carefully about
the answer will help a lot with learning how to formalize: What does
"Area of a Triangle = 1/2 base * height" mean? What even is a
triangle, and how do you define its area? Is this theorem true by
definition, and if not what are the relevant definitions? Depending on
the answers, you will get very different proofs overall.
BR,
_
Thierry
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0de08725-07d6-c345-2207-180ca11a1c71%40gmx.net.
