Metamath Proof Explorer

Theorem ltadds2

Description: Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion ltadds2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ C + s A < s C + s B

Proof

Step Hyp Ref Expression
1 leadds2 ⊢ B ∈ No ∧ A ∈ No ∧ C ∈ No → B ≤ s A ↔ C + s B ≤ s C + s A
2 1 3com12 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B ≤ s A ↔ C + s B ≤ s C + s A
3 2 notbid ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → ¬ B ≤ s A ↔ ¬ C + s B ≤ s C + s A
4 ltnles ⊢ A ∈ No ∧ B ∈ No → A < s B ↔ ¬ B ≤ s A
5 4 3adant3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ ¬ B ≤ s A
6 simp3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C ∈ No
7 simp1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ∈ No
8 6 7 addscld ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C + s A ∈ No
9 simp2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B ∈ No
10 6 9 addscld ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C + s B ∈ No
11 ltnles ⊢ C + s A ∈ No ∧ C + s B ∈ No → C + s A < s C + s B ↔ ¬ C + s B ≤ s C + s A
12 8 10 11 syl2anc ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C + s A < s C + s B ↔ ¬ C + s B ≤ s C + s A
13 3 5 12 3bitr4d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B ↔ C + s A < s C + s B