Metamath Proof Explorer


Theorem negsdi

Description: Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Assertion negsdi A No B No + s A + s B = + s A + s + s B

Proof

Step Hyp Ref Expression
1 addscl A No B No A + s B No
2 1 negsidd A No B No A + s B + s + s A + s B = 0 s
3 negsid A No A + s + s A = 0 s
4 negsid B No B + s + s B = 0 s
5 3 4 oveqan12d A No B No A + s + s A + s B + s + s B = 0 s + s 0 s
6 0sno 0 s No
7 addslid 0 s No 0 s + s 0 s = 0 s
8 6 7 ax-mp 0 s + s 0 s = 0 s
9 5 8 eqtr2di A No B No 0 s = A + s + s A + s B + s + s B
10 simpl A No B No A No
11 10 negscld A No B No + s A No
12 simpr A No B No B No
13 12 negscld A No B No + s B No
14 10 11 12 13 adds4d A No B No A + s + s A + s B + s + s B = A + s B + s + s A + s + s B
15 2 9 14 3eqtrd A No B No A + s B + s + s A + s B = A + s B + s + s A + s + s B
16 1 negscld A No B No + s A + s B No
17 negscl A No + s A No
18 negscl B No + s B No
19 addscl + s A No + s B No + s A + s + s B No
20 17 18 19 syl2an A No B No + s A + s + s B No
21 16 20 1 addscan1d A No B No A + s B + s + s A + s B = A + s B + s + s A + s + s B + s A + s B = + s A + s + s B
22 15 21 mpbid A No B No + s A + s B = + s A + s + s B