Metamath Proof Explorer

Theorem slesubaddd

Description: Surreal less-than or equal relationship between subtraction and addition. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Hypotheses sltsubadd.1 ⊢ φ → A ∈ No
sltsubadd.2 ⊢ φ → B ∈ No
sltsubadd.3 ⊢ φ → C ∈ No
Assertion slesubaddd ⊢ φ → A - s B ≤ s C ↔ A ≤ s C + s B

Proof

Step Hyp Ref Expression
1 sltsubadd.1 ⊢ φ → A ∈ No
2 sltsubadd.2 ⊢ φ → B ∈ No
3 sltsubadd.3 ⊢ φ → C ∈ No
4 3 2 1 sltaddsubd ⊢ φ → C + s B < s A ↔ C < s A - s B
5 4 notbid ⊢ φ → ¬ C + s B < s A ↔ ¬ C < s A - s B
6 3 2 addscld ⊢ φ → C + s B ∈ No
7 slenlt ⊢ A ∈ No ∧ C + s B ∈ No → A ≤ s C + s B ↔ ¬ C + s B < s A
8 1 6 7 syl2anc ⊢ φ → A ≤ s C + s B ↔ ¬ C + s B < s A
9 1 2 subscld ⊢ φ → A - s B ∈ No
10 slenlt ⊢ A - s B ∈ No ∧ C ∈ No → A - s B ≤ s C ↔ ¬ C < s A - s B
11 9 3 10 syl2anc ⊢ φ → A - s B ≤ s C ↔ ¬ C < s A - s B
12 5 8 11 3bitr4rd ⊢ φ → A - s B ≤ s C ↔ A ≤ s C + s B