Database
SURREAL NUMBERS
Surreal arithmetic
Multiplication
mulsproplem11
Metamath Proof Explorer
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