Metamath Proof Explorer

Theorem addscan2

Description: Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addscan2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C = B + s C ↔ A = B

Proof

Step Hyp Ref Expression
1 leadds1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ≤ s B ↔ A + s C ≤ s B + s C
2 leadds1 ⊢ B ∈ No ∧ A ∈ No ∧ C ∈ No → B ≤ s A ↔ B + s C ≤ s A + s C
3 2 3com12 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B ≤ s A ↔ B + s C ≤ s A + s C
4 1 3 anbi12d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ≤ s B ∧ B ≤ s A ↔ A + s C ≤ s B + s C ∧ B + s C ≤ s A + s C
5 lestri3 ⊢ A ∈ No ∧ B ∈ No → A = B ↔ A ≤ s B ∧ B ≤ s A
6 5 3adant3 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A = B ↔ A ≤ s B ∧ B ≤ s A
7 addscl ⊢ A ∈ No ∧ C ∈ No → A + s C ∈ No
8 7 3adant2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C ∈ No
9 addscl ⊢ B ∈ No ∧ C ∈ No → B + s C ∈ No
10 9 3adant1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B + s C ∈ No
11 lestri3 ⊢ A + s C ∈ No ∧ B + s C ∈ No → A + s C = B + s C ↔ A + s C ≤ s B + s C ∧ B + s C ≤ s A + s C
12 8 10 11 syl2anc ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C = B + s C ↔ A + s C ≤ s B + s C ∧ B + s C ≤ s A + s C
13 4 6 12 3bitr4rd ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C = B + s C ↔ A = B