Metamath Proof Explorer


Theorem mulsproplem11

Description: Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypotheses mulsproplem.1 φ a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
mulsproplem9.1 φ A No
mulsproplem9.2 φ B No
Assertion mulsproplem11 φ A s B No

Proof

Step Hyp Ref Expression
1 mulsproplem.1 φ a No b No c No d No e No f No bday a + bday b bday c + bday e bday d + bday f bday c + bday f bday d + bday e bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E a s b No c < s d e < s f c s f - s c s e < s d s f - s d s e
2 mulsproplem9.1 φ A No
3 mulsproplem9.2 φ B No
4 1 2 3 mulsproplem10 φ A s B No g | p L A q L B g = p s B + s A s q - s p s q h | r R A s R B h = r s B + s A s s - s r s s s A s B A s B s i | t L A u R B i = t s B + s A s u - s t s u j | v R A w L B j = v s B + s A s w - s v s w
5 4 simp1d φ A s B No