Metamath Proof Explorer


Theorem mulsproplem2

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and B itself 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
mulsproplem2.1 φ X Old bday A
mulsproplem2.2 φ B No
Assertion mulsproplem2 φ X 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 mulsproplem2.1 φ X Old bday A
3 mulsproplem2.2 φ B No
4 oldssno Old bday A No
5 4 2 sselid φ X No
6 0sno 0 s No
7 6 a1i φ 0 s No
8 bday0s bday 0 s =
9 8 8 oveq12i bday 0 s + bday 0 s = +
10 0elon On
11 naddrid On + =
12 10 11 ax-mp + =
13 9 12 eqtri bday 0 s + bday 0 s =
14 13 13 uneq12i bday 0 s + bday 0 s bday 0 s + bday 0 s =
15 un0 =
16 14 15 eqtri bday 0 s + bday 0 s bday 0 s + bday 0 s =
17 16 16 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 =
18 17 15 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 =
19 18 uneq2i bday X + bday B 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 B
20 un0 bday X + bday B = bday X + bday B
21 19 20 eqtri bday X + bday B 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 B
22 oldbdayim X Old bday A bday X bday A
23 2 22 syl φ bday X bday A
24 bdayelon bday X On
25 bdayelon bday A On
26 bdayelon bday B On
27 naddel1 bday X On bday A On bday B On bday X bday A bday X + bday B bday A + bday B
28 24 25 26 27 mp3an bday X bday A bday X + bday B bday A + bday B
29 23 28 sylib φ bday X + bday B bday A + bday B
30 elun1 bday X + bday B bday A + bday B bday X + bday B bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
31 29 30 syl φ bday X + bday B bday A + bday B bday C + bday E bday D + bday F bday C + bday F bday D + bday E
32 21 31 eqeltrid φ bday X + bday B 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
33 1 5 3 7 7 7 7 32 mulsproplem1 φ X s B 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
34 33 simpld φ X s B No