Metamath Proof Explorer


Theorem sn-subeu

Description: negeu without ax-mulcom and complex number version of resubeu . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-subeu A B ∃! x A + x = B

Proof

Step Hyp Ref Expression
1 sn-negex A y A + y = 0
2 1 adantr A B y A + y = 0
3 simprl A B y A + y = 0 y
4 simplr A B y A + y = 0 B
5 3 4 addcld A B y A + y = 0 y + B
6 simplrr A B y A + y = 0 x A + y = 0
7 6 oveq1d A B y A + y = 0 x A + y + B = 0 + B
8 simplll A B y A + y = 0 x A
9 simplrl A B y A + y = 0 x y
10 simpllr A B y A + y = 0 x B
11 8 9 10 addassd A B y A + y = 0 x A + y + B = A + y + B
12 sn-addid2 B 0 + B = B
13 10 12 syl A B y A + y = 0 x 0 + B = B
14 7 11 13 3eqtr3rd A B y A + y = 0 x B = A + y + B
15 14 eqeq2d A B y A + y = 0 x A + x = B A + x = A + y + B
16 simpr A B y A + y = 0 x x
17 9 10 addcld A B y A + y = 0 x y + B
18 8 16 17 sn-addcand A B y A + y = 0 x A + x = A + y + B x = y + B
19 15 18 bitrd A B y A + y = 0 x A + x = B x = y + B
20 19 ralrimiva A B y A + y = 0 x A + x = B x = y + B
21 reu6i y + B x A + x = B x = y + B ∃! x A + x = B
22 5 20 21 syl2anc A B y A + y = 0 ∃! x A + x = B
23 2 22 rexlimddv A B ∃! x A + x = B