# Metamath - simple equation solution / proof

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?

• 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. Commented Jul 23, 2023 at 22:40
• 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. Commented Jul 24, 2023 at 3:01
– Trebor
Commented Jul 24, 2023 at 3:51
• Both look a good fit, will give it a try, thanks. Commented Jul 24, 2023 at 9:54
• 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). Commented Jul 24, 2023 at 13:55

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 )