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