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 oldssno Old bday B No
5 4 3 sselid φ Y 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 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
20 un0 bday A + bday Y = bday A + bday Y
21 19 20 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
22 oldbdayim Y Old bday B bday Y bday B
23 3 22 syl φ bday Y bday B
24 bdayelon bday Y On
25 bdayelon bday B On
26 bdayelon bday A On
27 naddel2 bday Y On bday B On bday A On bday Y bday B bday A + bday Y bday A + bday B
28 24 25 26 27 mp3an bday Y bday B bday A + bday Y bday A + bday B
29 23 28 sylib φ bday A + bday Y bday A + bday B
30 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
31 29 30 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
32 21 31 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
33 1 2 5 7 7 7 7 32 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
34 33 simpld φ A s Y No