Metamath Proof Explorer

Theorem mulsproplem4

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and a member of the old set of B is a surreal number. (Contributed by Scott Fenton, 4-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
mulsproplem4.1 ⊢ φ → X ∈ Old ⁡ bday ⁡ A
mulsproplem4.2 ⊢ φ → Y ∈ Old ⁡ bday ⁡ B
Assertion mulsproplem4 ⊢ φ → X ⋅ s Y ∈ 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 mulsproplem4.1 ⊢ φ → X ∈ Old ⁡ bday ⁡ A
3 mulsproplem4.2 ⊢ φ → Y ∈ Old ⁡ bday ⁡ B
4 oldssno ⊢ Old ⁡ bday ⁡ A ⊆ No
5 4 2 sselid ⊢ φ → X ∈ No
6 oldssno ⊢ Old ⁡ bday ⁡ B ⊆ No
7 6 3 sselid ⊢ φ → Y ∈ No
8 0sno ⊢ 0 s ∈ No
9 8 a1i ⊢ φ → 0 s ∈ No
10 bday0s ⊢ bday ⁡ 0 s = ∅
11 10 10 oveq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅ + ∅
12 0elon ⊢ ∅ ∈ On
13 naddrid ⊢ ∅ ∈ On → ∅ + ∅ = ∅
14 12 13 ax-mp ⊢ ∅ + ∅ = ∅
15 11 14 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅
16 15 15 uneq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅ ∪ ∅
17 un0 ⊢ ∅ ∪ ∅ = ∅
18 16 17 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅
19 18 18 uneq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅ ∪ ∅
20 19 17 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅
21 20 uneq2i ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = bday ⁡ X + bday ⁡ Y ∪ ∅
22 un0 ⊢ bday ⁡ X + bday ⁡ Y ∪ ∅ = bday ⁡ X + bday ⁡ Y
23 21 22 eqtri ⊢ bday ⁡ X + bday ⁡ Y ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = bday ⁡ X + bday ⁡ Y
24 oldbdayim ⊢ X ∈ Old ⁡ bday ⁡ A → bday ⁡ X ∈ bday ⁡ A
25 2 24 syl ⊢ φ → bday ⁡ X ∈ bday ⁡ A
26 oldbdayim ⊢ Y ∈ Old ⁡ bday ⁡ B → bday ⁡ Y ∈ bday ⁡ B
27 3 26 syl ⊢ φ → bday ⁡ Y ∈ bday ⁡ B
28 bdayelon ⊢ bday ⁡ A ∈ On
29 bdayelon ⊢ bday ⁡ B ∈ On
30 naddel12 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ X ∈ bday ⁡ A ∧ bday ⁡ Y ∈ bday ⁡ B → bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
31 28 29 30 mp2an ⊢ bday ⁡ X ∈ bday ⁡ A ∧ bday ⁡ Y ∈ bday ⁡ B → bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
32 25 27 31 syl2anc ⊢ φ → bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
33 elun1 ⊢ bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B → bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
34 32 33 syl ⊢ φ → bday ⁡ X + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
35 23 34 eqeltrid ⊢ φ → bday ⁡ X + bday ⁡ Y ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
36 1 5 7 9 9 9 9 35 mulsproplem1 ⊢ φ → X ⋅ s Y ∈ No ∧ 0 s < s 0 s ∧ 0 s < s 0 s → 0 s ⋅ s 0 s - s 0 s ⋅ s 0 s < s 0 s ⋅ s 0 s - s 0 s ⋅ s 0 s
37 36 simpld ⊢ φ → X ⋅ s Y ∈ No