Theorem mulsproplem11

Description: Lemma for surreal multiplication. Under the inductive hypothesis, demonstrate closure of surreal multiplication. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	No typesetting found for |- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
	mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mulsproplem11	Could not format assertion : No typesetting found for |- ( ph -> ( A x.s B ) e. No ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	Could not format ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
2		mulsproplem9.1	$$⊢\phi \to A\in \mathrm{No}$$
3		mulsproplem9.2	$$⊢\phi \to B\in \mathrm{No}$$
4	1 2 3	mulsproplem10	Could not format ( ph -> ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) < ( ( A x.s B ) e. No /\ ( { g | E. p e. ( _Left ` A ) E. q e. ( _Left ` B ) g = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { h | E. r e. ( _Right ` A ) E. s e. ( _Right ` B ) h = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) <
5	4	simp1d	Could not format ( ph -> ( A x.s B ) e. No ) : No typesetting found for |- ( ph -> ( A x.s B ) e. No ) with typecode |-