Metamath Proof Explorer

Theorem lesubaddsd

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

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

Proof

Step Hyp Ref Expression
1 ltsubadds.1 ⊢ φ → A ∈ No
2 ltsubadds.2 ⊢ φ → B ∈ No
3 ltsubadds.3 ⊢ φ → C ∈ No
4 3 2 1 ltaddsubsd ⊢ φ → 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 lenlts ⊢ 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 lenlts ⊢ 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