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