Metamath Proof Explorer

Theorem mulsproplem3

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of A itself 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
mulsproplem3.1 ⊢ φ → A ∈ No
mulsproplem3.2 ⊢ φ → Y ∈ Old ⁡ bday ⁡ B
Assertion mulsproplem3 ⊢ φ → A ⋅ 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 mulsproplem3.1 ⊢ φ → A ∈ No
3 mulsproplem3.2 ⊢ φ → Y ∈ Old ⁡ bday ⁡ B
4 3 oldnod ⊢ φ → Y ∈ No
5 0no ⊢ 0 s ∈ No
6 5 a1i ⊢ φ → 0 s ∈ No
7 bday0 ⊢ bday ⁡ 0 s = ∅
8 7 7 oveq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅ + ∅
9 0elon ⊢ ∅ ∈ On
10 naddrid ⊢ ∅ ∈ On → ∅ + ∅ = ∅
11 9 10 ax-mp ⊢ ∅ + ∅ = ∅
12 8 11 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s = ∅
13 12 12 uneq12i ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅ ∪ ∅
14 un0 ⊢ ∅ ∪ ∅ = ∅
15 13 14 eqtri ⊢ bday ⁡ 0 s + bday ⁡ 0 s ∪ bday ⁡ 0 s + bday ⁡ 0 s = ∅
16 15 15 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 = ∅ ∪ ∅
17 16 14 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 = ∅
18 17 uneq2i ⊢ bday ⁡ A + 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 ⁡ Y ∪ ∅
19 un0 ⊢ bday ⁡ A + bday ⁡ Y ∪ ∅ = bday ⁡ A + bday ⁡ Y
20 18 19 eqtri ⊢ bday ⁡ A + 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 ⁡ Y
21 oldbdayim ⊢ Y ∈ Old ⁡ bday ⁡ B → bday ⁡ Y ∈ bday ⁡ B
22 3 21 syl ⊢ φ → bday ⁡ Y ∈ bday ⁡ B
23 bdayon ⊢ bday ⁡ Y ∈ On
24 bdayon ⊢ bday ⁡ B ∈ On
25 bdayon ⊢ bday ⁡ A ∈ On
26 naddel2 ⊢ bday ⁡ Y ∈ On ∧ bday ⁡ B ∈ On ∧ bday ⁡ A ∈ On → bday ⁡ Y ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
27 23 24 25 26 mp3an ⊢ bday ⁡ Y ∈ bday ⁡ B ↔ bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
28 22 27 sylib ⊢ φ → bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B
29 elun1 ⊢ bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B → bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
30 28 29 syl ⊢ φ → bday ⁡ A + bday ⁡ Y ∈ bday ⁡ A + bday ⁡ B ∪ bday ⁡ C + bday ⁡ E ∪ bday ⁡ D + bday ⁡ F ∪ bday ⁡ C + bday ⁡ F ∪ bday ⁡ D + bday ⁡ E
31 20 30 eqeltrid ⊢ φ → bday ⁡ A + 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
32 1 2 4 6 6 6 6 31 mulsproplem1 ⊢ φ → A ⋅ 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
33 32 simpld ⊢ φ → A ⋅ s Y ∈ No