Metamath Proof Explorer

Theorem ltsubs1

Description: Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion ltsubs1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ A - s C < s B - s C

Proof

Step Hyp Ref Expression
1 negscl ⊢ C ∈ No → + s ⁡ C ∈ No
2 ltadds1 ⊢ A ∈ No ∧ B ∈ No ∧ + s ⁡ C ∈ No → A < s B ↔ A + s + s ⁡ C < s B + s + s ⁡ C
3 1 2 syl3an3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ A + s + s ⁡ C < s B + s + s ⁡ C
4 subsval ⊢ A ∈ No ∧ C ∈ No → A - s C = A + s + s ⁡ C
5 4 3adant2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A - s C = A + s + s ⁡ C
6 subsval ⊢ B ∈ No ∧ C ∈ No → B - s C = B + s + s ⁡ C
7 6 3adant1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B - s C = B + s + s ⁡ C
8 5 7 breq12d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A - s C < s B - s C ↔ A + s + s ⁡ C < s B + s + s ⁡ C
9 3 8 bitr4d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ A - s C < s B - s C