A Challenging Pair of Equations

Antti Valmari 2025-07-19

This web page illustrates how the reasoning operators, subproofs and assumption mechanism of MathCheck can be used to present non-trivial mathematical reasoning so that at each step, one may ask MathCheck to check what has been written so far. The reader is not assumed to have any earlier experience with MathCheck. Therefore, various tricks are introduced along the way. On the other hand, the reader is assumed to have an idea of what kind of difficulties students have with learning mathematical reasoning. While MathCheck is very far from a mathematical genius, it can help with learning the logic side of reasoning.

1. Getting Started and Using Implication

The task is to solve

6y − 8|x|

3 − x

= 4 ∧ |x + y − 5| = 2

One possible way of starting is to solve y from |x + y − 5| = 2. The original formula has been pre-programmed. We may use ⇒ to extract |x + y − 5| = 2 and then solve it as follows:

==> |x+y-5| = 2 <=> x+y-5 = 2 \/ x+y-5 = -2 <=> y = 7-x \/ y = 3-x

Please copy it to the answer box and click the “new tab” or “to below” button. The answer box is on the top right part of the screen. Much of the time “to below” is handier, but if the feedback does not fit in the box, then it may be worth clicking “new tab”.

The magenta “Implication was used without returning to the original” in the feedback is not a sign of an error. Instead, it notifies that what we have written is mathematically correct, but cannot be accepted as a final answer.

The light brown regionsYou found this hidden text! Congratulations! on the top right part of the screen contain instructions how to type non-trivial symbols, such as ≡. In general, each light brown region contains hidden text that becomes visible when the mouse pointer is moved over it.

To save typing, the part |x + y − 5| = 2 could have been copied from the original pair of equations. You may try! Paint and copy it, replace the corresponding text in the answer box by it, and click a button. Unfortunately, this will not work for everything.

To see what kind of feedback MathCheck gives on an error, please introduce an error by changing something in the answer and click a button. For instance, change some number, or change some − to +.

MathCheck does not need the intermediate results |x + y − 5| = 2 and x + y − 5 = 2 ∨ x + y − 5 = −2. However, writing intermediate results makes it easier to avoid and debug errors.

The subproof mechanism described next could have been used also on this step.

2. The First Subproof

Let us next solve the case y = 3 − x by writing a subproof where it is an assumption. We start by multiplying the divisor away. Please try the following.

subproof assume y = 3-x; (6y-3|x|) / 3-x = 4 <=> 6y-3|x| = 4(3-x) subend

MathCheck is not at all happy! By looking at the feedback it is easy to see what went wrong: “− x” is not in the divisor but after it. That is, we have forgotten the parentheses around the divisor. Please fix it and try again.

Now the feedback contains “The main proof ended unexpectedly” in magenta. It comes because we have not yet written anything in the main proof, we only have started writing a subproof. The important thing is that to the extent we have written the subproof, it is correct. Or is it?

It is internally correct, and that is why MathCheck accepts it. But where there should be 8, it has 3. It is thus not what we wanted to solve. The risk of this kind of problems can be reduced by starting the subproof with original <=>. It makes MathCheck check that within the limits of the assumption, the first new formula of the subproof matches the first formula of the whole proof. Please try it. Then fix the 8's.

Had we forgotten the parentheses around 6y − 8|x| instead of 3 − x, the red text in the feedback would have been “Too complicated claim or expression, or too big numbers”. This is because then multiplying the divisor away would have involved multiplying 6y by 3 − x, resulting in 18y − 6xy. In it, xy is a product of two variables, which is too difficult for the real logic mode of MathCheck. Of course, you are encouraged to try this, too!

To continue solving the case, please replace y by 3 − x in the last formula before subend. It is correct, because the prevailing assumptions guarantee y = 3 − x. Check that MathCheck is still happy. HintDo not forget parentheses around 3 − x.

You may want to split the answer to more than one line, to make it easier to read. The best places are immediately after ; and immediately before <=> and subend, but also many other places are okay. Please test the difference between splitting immediately after and immediately before <=>.

Then multiply out the parentheses. It is not necessary to write <=> and yet another formula. Instead, you may add = 12-4x to the end and do the corresponding thing with 6(3-x) at the opposite end of the formula. Check that MathCheck is still happy. HintThe left hand side needs a copy of − 8|x|.

Although not necessary, it promotes clarity to copy the last formula and its preceding <=>, and remove everything except the first and last expression and one = from the copy. Not taking a copy and doing the removal in the original would be okay for MathCheck, but it would make it more difficult for humans to understand how the answer was developed. The new part should look like this⇔ 18 − 6x − 8|x| = 12 − 4x.

Now continue until you have a formula of the form x = … ∨ x = …. The answer need not fit in the answer box. HintAny  equation( |term| )  can be replaced by  term < 0 ∧ equation( −term ) ∨ term ≥ 0 ∧ equation( term ) .

To complete the solution, make it of the form x = … ∧ y = … ∨ x = … ∧ y = …. HintThe value of y is determined by the assumption.

One possible correct complete subproof is heresubproof assume y = 3-x;
(6y-8|x|) / (3-x) = 4 <=> 18-6x - 8|x| = 6(3-x)-8|x| = 4(3-x) = 12-4x
<=> 18-6x - 8|x| = 12-4x <=> 6 - 8|x| = 2x
<=> x<0 /\ 6+8x = 2x \/ x>=0 /\ 6-8x = 2x
<=> x<0 /\ 6 = -6x \/ x>=0 /\ 6 = 10x <=> x = -1 \/ x = 6/10
<=> x = -1 /\ y = 4 \/ x = 6/10 /\ y = 2 4/10
subend.

3. The Second Subproof

We still have to solve the case y = 7 − x. Please try the following.

subproof assume y = 7-x; original <=> 6y-8|x| = 4(3-x) subend

MathCheck said that if y = 4 and x = 3, then the left hand side is undefined but the right hand side yields true. Indeed, then the left hand side contains division by 0, but the right hand side reduces to 0 = 0.

So we must rule out division by 0. Please try the following.

subproof assume y = 7-x; original <=> x != 3 /\ 6y-8|x| = 4(3-x) subend

Can you guess what MathCheck says if we continue like this?

subproof assume y = 7-x; original <=> x != 3 /\ 6y-8|x| = 4(3-x)
<=> 6(7-x)-8|x| = 4(3-x) subend

That is, if we rule x = 3 out in one formula, then we have to rule it out also in subsequent formulas. Writing “x ≠ 3 ∧” again and again does not sound attractive. One possibility would be to make 6y − 8|x| = 4(3 − x) ⇔ … ⇔ x = 3 ∨ x = … a subproof of the current subproof. However, there is a simpler optionMove “x ≠ 3 ∧” to the assumption..

This is a good place to illustrate the difference between <=> and ===. Please change the last <=> to === and click a button! The feedback tells that it is not okay for === that the left hand side is undefined and the right hand side is false. But it is okay for <=>. Now please change the === back to <=>.

The rest of this subproof can be developed similarly to the previous one. One possible correct complete subproof is heresubproof assume x != 3 /\ y = 7-x; original <=> 6y-8|x| = 4(3-x)
<=> 42-6x-8|x| = 6(7-x)-8|x| = 4(3-x) = 12-4x
<=> 30 = 2x + 8|x| <=> x < 0 /\ 30 = -6x \/ x >= 0 /\ 30 = 10x
<=> x = -5 \/ x = 3 <=> x = -5 /\ y = 12
subend.

4. Combining the Results

We are ready to write the final answer. It is just a disjunction of the last formulas of the subproofs — well, almost, because there is still one thing we would like to illustrate. Please add the following to the end of the answer. (It works also as the whole answer, and then original can be left out.)

original <=> x = -1 /\ y = 4 \/ x = 6/10 /\ y = 2 4/10 \/ x = -5 /\ y = 12

According to MathCheck, there is a small problem in the answer. This is because the teacher may ask MathCheck to insist that the final answer of the main proof obeys certain conventions. (Last formulas of subproofs need not obey them, because from the point of view of the main proof, they are intermediate results.) Please fix the problem and verify that MathCheck is now happy.

Here==> |x+y-5| = 2 <=> x+y-5 = 2 \/ x+y-5 = -2 <=> y = 7-x \/ y = 3-x
subproof assume y = 3-x;
(6y-8|x|) / (3-x) = 4 <=> 18-6x - 8|x| = 6(3-x)-8|x| = 4(3-x) = 12-4x
<=> 18-6x - 8|x| = 12-4x <=> 6 - 8|x| = 2x
<=> x<0 /\ 6+8x = 2x \/ x>=0 /\ 6-8x = 2x
<=> x<0 /\ 6 = -6x \/ x>=0 /\ 6 = 10x <=> x = -1 \/ x = 6/10
<=> x = -1 /\ y = 4 \/ x = 6/10 /\ y = 2 4/10
subend
subproof assume x != 3 /\ y = 7-x; original <=> 6y-8|x| = 4(3-x)
<=> 42-6x-8|x| = 6(7-x)-8|x| = 4(3-x) = 12-4x
<=> 30 = 2x + 8|x| <=> x < 0 /\ 30 = -6x \/ x >= 0 /\ 30 = 10x
<=> x = -5 \/ x = 3 <=> x = -5 /\ y = 12
subend
original <=> x = -1 /\ y = 4 \/ x = 3/5 /\ y = 2 2/5 \/ x = -5 /\ y = 12 is the full solution as developed above, with the last problem fixed.

5. Concluding Remarks

By default, for each incorrect answer, MathCheck replies with a counter-example. Therefore, if the student answers <=> FF, then MathCheck gives such values of x and y that make the original formula true. At the time of writing, MathCheck chose x = 3 / 5 and y = 12 / 5. If the student changes the reply to <=> x = 3 / 5 /\ y = 12 / 5, then MathCheck reveals another root in the counter-example.

However, the teacher can switch counter-examples off. The effect may be tried below. The answer already in the box can be replaced by other answers.

The solution developed above proceeds by first solving y from |x + y − 5| = 2 and then assigning the resulting expressions in the place of y in the other equation. Another well-working possibility starts by solving y from the first equation when x < 0 and when x ≥ 0. Then the resulting expressions are assigned to |x + y − 5| = 2. Altogether four cases arise, but each one can be solved briefly. This solution can be tried and played with below.