Metamath Proof Explorer

Theorem addscl

Description: Surreal numbers are closed under addition. Theorem 6(iii) of [Conway[ p. 18. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addscl ⊢ A ∈ No ∧ B ∈ No → A + s B ∈ No

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ No ∧ B ∈ No → A ∈ No
2 simpr ⊢ A ∈ No ∧ B ∈ No → B ∈ No
3 1 2 addscld ⊢ A ∈ No ∧ B ∈ No → A + s B ∈ No