Metamath Proof Explorer

Theorem ltsubs2

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

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

Proof

Step Hyp Ref Expression
1 negscl ⊢ B ∈ No → + s ⁡ B ∈ No
2 1 3ad2ant2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → + s ⁡ B ∈ No
3 negscl ⊢ A ∈ No → + s ⁡ A ∈ No
4 3 3ad2ant1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → + s ⁡ A ∈ No
5 simp3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C ∈ No
6 2 4 5 ltadds2d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → + s ⁡ B < s + s ⁡ A ↔ C + s + s ⁡ B < s C + s + s ⁡ A
7 ltnegs ⊢ A ∈ No ∧ B ∈ No → A < s B ↔ + s ⁡ B < s + s ⁡ A
8 7 3adant3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ + s ⁡ B < s + s ⁡ A
9 simp2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B ∈ No
10 5 9 subsvald ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C - s B = C + s + s ⁡ B
11 simp1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ∈ No
12 5 11 subsvald ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C - s A = C + s + s ⁡ A
13 10 12 breq12d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C - s B < s C - s A ↔ C + s + s ⁡ B < s C + s + s ⁡ A
14 6 8 13 3bitr4d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ C - s B < s C - s A