Metamath Proof Explorer


Theorem subadds

Description: Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion subadds A No B No C No A - s B = C B + s C = A

Proof

Step Hyp Ref Expression
1 subsval A No B No A - s B = A + s + s B
2 1 3adant3 A No B No C No A - s B = A + s + s B
3 2 eqeq1d A No B No C No A - s B = C A + s + s B = C
4 simpl B No C No B No
5 simpr B No C No C No
6 negscl B No + s B No
7 6 adantr B No C No + s B No
8 4 5 7 adds32d B No C No B + s C + s + s B = B + s + s B + s C
9 negsid B No B + s + s B = 0 s
10 9 adantr B No C No B + s + s B = 0 s
11 10 oveq1d B No C No B + s + s B + s C = 0 s + s C
12 addslid C No 0 s + s C = C
13 12 adantl B No C No 0 s + s C = C
14 8 11 13 3eqtrd B No C No B + s C + s + s B = C
15 14 3adant1 A No B No C No B + s C + s + s B = C
16 15 eqeq1d A No B No C No B + s C + s + s B = A + s + s B C = A + s + s B
17 eqcom C = A + s + s B A + s + s B = C
18 16 17 bitrdi A No B No C No B + s C + s + s B = A + s + s B A + s + s B = C
19 addscl B No C No B + s C No
20 19 3adant1 A No B No C No B + s C No
21 simp1 A No B No C No A No
22 simp2 A No B No C No B No
23 22 negscld A No B No C No + s B No
24 20 21 23 addscan2d A No B No C No B + s C + s + s B = A + s + s B B + s C = A
25 3 18 24 3bitr2d A No B No C No A - s B = C B + s C = A