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