Theorem sltmul12ad

Description: Comparison of the product of two positive surreals. (Contributed by Scott Fenton, 17-Apr-2025)

	Ref	Expression
Hypotheses	sltmul12ad.1	|- ( ph -> A e. No )
	sltmul12ad.2	|- ( ph -> B e. No )
	sltmul12ad.3	|- ( ph -> C e. No )
	sltmul12ad.4	|- ( ph -> D e. No )
	sltmul12ad.5	|- ( ph -> 0s <_s A )
	sltmul12ad.6	|- ( ph -> A
	sltmul12ad.7	|- ( ph -> 0s <_s C )
	sltmul12ad.8	|- ( ph -> C
Assertion	sltmul12ad	|- ( ph -> ( A x.s C )

Proof

Step	Hyp	Ref	Expression
1		sltmul12ad.1	|- ( ph -> A e. No )
2		sltmul12ad.2	|- ( ph -> B e. No )
3		sltmul12ad.3	|- ( ph -> C e. No )
4		sltmul12ad.4	|- ( ph -> D e. No )
5		sltmul12ad.5	|- ( ph -> 0s <_s A )
6		sltmul12ad.6	|- ( ph -> A
7		sltmul12ad.7	|- ( ph -> 0s <_s C )
8		sltmul12ad.8	|- ( ph -> C
9	1 3	mulscld	|- ( ph -> ( A x.s C ) e. No )
10	2 3	mulscld	|- ( ph -> ( B x.s C ) e. No )
11	2 4	mulscld	|- ( ph -> ( B x.s D ) e. No )
12	1 2 6	sltled	|- ( ph -> A <_s B )
13	1 2 3 7 12	slemul1ad	|- ( ph -> ( A x.s C ) <_s ( B x.s C ) )
14		0sno	|- 0s e. No
15	14	a1i	|- ( ph -> 0s e. No )
16	15 1 2 5 6	slelttrd	|- ( ph -> 0s
17	3 4 2 16	sltmul2d	|- ( ph -> ( C ( B x.s C )
18	8 17	mpbid	|- ( ph -> ( B x.s C )
19	9 10 11 13 18	slelttrd	|- ( ph -> ( A x.s C )