3
$\begingroup$

Sorry if an improper question, looking into metamath and metamath-lamp and though it should be trivial to prove A = 2 -> ( A + 2 ) = 4, or the inverse.

But cant seem to get it right in metamath-lamp.

Starting with hypothesis H ( A + 2 ) = 4

it should (?) be possible, even simple, to get to:

G A = 2

Started with:

- H        |- ( A + 2 ) = 4
- P 2p2e4  |- ( 2 + 2 ) = 4 
- P eqtr4i |- ( A + 2 ) = ( 2 + 2 )

After this, I'm blocked, cant find the steps that get to the goal: A = 2

Wouldn't some existing simplification do the trick? Does it exists in set.mm? How do I apply it?

Improve this question
$\endgroup$
8
  • $\begingroup$ I don’t know much about metamath, but the rule you propose is clearly false. For example A * 0 = 0 * 0 does not imply A = 0. $\endgroup$
    – Jason Rute
    Commented Jul 23, 2023 at 22:40
  • $\begingroup$ Yes, true, thanks for ponting that. Don't know much about metamath also, but at some point when browsing metamath MPE I believe I saw some simplification theorems, that might do the trick, not that one for sure. Edited my question. $\endgroup$
    – Jorge Agra
    Commented Jul 24, 2023 at 3:01
  • 1
    $\begingroup$ addcan2? Or addcan2i which will be easier to use. $\endgroup$
    – Trebor ♦
    Commented Jul 24, 2023 at 3:51
  • $\begingroup$ Both look a good fit, will give it a try, thanks. $\endgroup$
    – Jorge Agra
    Commented Jul 24, 2023 at 9:54
  • $\begingroup$ In your question you say you are trying to prove A = 2 -> ( A + 2 ) = 4 but your proof looks like you are actually proving the converse (which is admittedly more interesting). $\endgroup$
    – Jason Rute
    Commented Jul 24, 2023 at 13:55

1 Answer 1

Reset to default
2
$\begingroup$

Here is a proof for the first direction: A = 2 -> ( A + 2 ) = 4

h1::jagra1.1         |- A = 2
2:1:oveq1i          |- ( A + 2 ) = ( 2 + 2 )
3::2p2e4            |- ( 2 + 2 ) = 4
qed:2,3:eqtri      |- ( A + 2 ) = 4

For the reverse direction, more proof steps are necessary. Especially, since A is an unknown, you'll need to specify you're looking for a complex number:

h1::jagra.1          |- A e. CC
h2::jagra.2          |- ( A + 2 ) = 4
3::2p2e4             |- ( 2 + 2 ) = 4
4::2cn               |- 2 e. CC
5:1,4,2:mvlraddi    |- A = ( 4 - 2 )
6:4,4,3:mvlraddi    |- 2 = ( 4 - 2 )
qed:5,6:eqtr4i     |- A = 2

It is also possible to prove both directions directly as an equivalence:

h1::jagra.1         |- A e. CC
2::2cn               |- 2 e. CC
3::2p2e4             |- ( 2 + 2 ) = 4
4:1,2,2:addcan2i    |- ( ( A + 2 ) = ( 2 + 2 ) <-> A = 2 )
5:3:eqeq2i          |- ( ( A + 2 ) = ( 2 + 2 ) <-> ( A + 2 ) = 4 )
qed:5,4:bitr3i     |- ( ( A + 2 ) = 4 <-> A = 2 )
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.