ProveDetails Command
 ProveDetails( <Boolean Expression> )

Returns some details of the result of the automated proof.
Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the ProveDetails command uses symbolic methods to determine whether a statement is true or false in general. This command works like the Prove command, but also returns some details of the result as a list:

An empty list {} if GeoGebra cannot determine the answer.

A list with one element: {false}, if the statement is not true in general.

A list with one element: {true}, if the statement is always true (in all cases when the diagram can be constructed).

A list with more elements, containing the boolean value true and another list for some socalled nondegeneracy conditions, if the statement is true under certain conditions, e.g. {true, {"AreCollinear(A,B,C),AreEqual(C,D)"}}. This means that if none of the conditions are true (and the diagram can be constructed), then the statement will be true.

A list {true,{"…"}}, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.
Let us define a triangle with vertices A, B and C, and define D=MidPoint(B,C)
, E=MidPoint(A,C)
,
p=Line(A,B)
, q=Line(D,E)
. Now ProveDetails(p∥q)
returns {true}, which means that if the diagram can
be constructed, then the midline DE of the triangle is parallel to the side AB.
Let AB be the segment a, and define C=MidPoint(A,B)
, b=PerpendicularBisector(A,B)
,
D=Intersect(a,b)
. Now ProveDetails(C==D)
returns {true,{"AreEqual(A,B)"}}: it means that if the points A
and B differ, then the points C and D will coincide.
Let AB be the segment a, and define l=Line(A,B)
. Let C be an arbitrary point on line l, moreover let
b=Segment(B,C)
, c=Segment(A,C)
. Now ProveDetails(a==b+c)
returns {true,{"a+b==c", "b==a+c"}}: it
means that if neither \(a+b=c\), nor \(b=a+c\), then \(a=b+c\).
It is possible that the list of the nondegeneracy conditions is not the simplest possible set. For the above example, the simplest set would be the empty set.
See also Prove command, Boolean values, GeoGebra Automated Reasoning Tools: A Tutorial and technical details of the algorithms. 