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	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
	mulsproplem3.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulsproplem3.2	⊢ ( 𝜑 → 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
Assertion	mulsproplem3	⊢ ( 𝜑 → ( 𝐴 ·s 𝑌 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ No ∀ 𝑏 ∈ No ∀ 𝑐 ∈ No ∀ 𝑑 ∈ No ∀ 𝑒 ∈ No ∀ 𝑓 ∈ No ( ( ( ( bday ‘ 𝑎 ) +no ( bday ‘ 𝑏 ) ) ∪ ( ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑒 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑓 ) ) ) ∪ ( ( ( bday ‘ 𝑐 ) +no ( bday ‘ 𝑓 ) ) ∪ ( ( bday ‘ 𝑑 ) +no ( bday ‘ 𝑒 ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) → ( ( 𝑎 ·s 𝑏 ) ∈ No ∧ ( ( 𝑐 <s 𝑑 ∧ 𝑒 <s 𝑓 ) → ( ( 𝑐 ·s 𝑓 ) -s ( 𝑐 ·s 𝑒 ) ) <s ( ( 𝑑 ·s 𝑓 ) -s ( 𝑑 ·s 𝑒 ) ) ) ) ) )
2		mulsproplem3.1	⊢ ( 𝜑 → 𝐴 ∈ No )
3		mulsproplem3.2	⊢ ( 𝜑 → 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
4	3	oldnod	⊢ ( 𝜑 → 𝑌 ∈ No )
5		0no	⊢ 0s ∈ No
6	5	a1i	⊢ ( 𝜑 → 0s ∈ No )
7		bday0	⊢ ( bday ‘ 0s ) = ∅
8	7 7	oveq12i	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ( ∅ +no ∅ )
9		0elon	⊢ ∅ ∈ On
10		naddrid	⊢ ( ∅ ∈ On → ( ∅ +no ∅ ) = ∅ )
11	9 10	ax-mp	⊢ ( ∅ +no ∅ ) = ∅
12	8 11	eqtri	⊢ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) = ∅
13	12 12	uneq12i	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ( ∅ ∪ ∅ )
14		un0	⊢ ( ∅ ∪ ∅ ) = ∅
15	13 14	eqtri	⊢ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) = ∅
16	15 15	uneq12i	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ( ∅ ∪ ∅ )
17	16 14	eqtri	⊢ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) = ∅
18	17	uneq2i	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) = ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∪ ∅ )
19		un0	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∪ ∅ ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) )
20	18 19	eqtri	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) )
21		oldbdayim	⊢ ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) )
22	3 21	syl	⊢ ( 𝜑 → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) )
23		bdayon	⊢ ( bday ‘ 𝑌 ) ∈ On
24		bdayon	⊢ ( bday ‘ 𝐵 ) ∈ On
25		bdayon	⊢ ( bday ‘ 𝐴 ) ∈ On
26		naddel2	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
27	23 24 25 26	mp3an	⊢ ( ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
28	22 27	sylib	⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
29		elun1	⊢ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
30	28 29	syl	⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
31	20 30	eqeltrid	⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ∪ ( ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ∪ ( ( bday ‘ 0s ) +no ( bday ‘ 0s ) ) ) ) ) ∈ ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∪ ( ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐸 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐹 ) ) ) ∪ ( ( ( bday ‘ 𝐶 ) +no ( bday ‘ 𝐹 ) ) ∪ ( ( bday ‘ 𝐷 ) +no ( bday ‘ 𝐸 ) ) ) ) ) )
32	1 2 4 6 6 6 6 31	mulsproplem1	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝑌 ) ∈ No ∧ ( ( 0s <s 0s ∧ 0s <s 0s ) → ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) <s ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) ) ) )
33	32	simpld	⊢ ( 𝜑 → ( 𝐴 ·s 𝑌 ) ∈ No )