Theorem ltmuls12ad

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

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

Proof

Step	Hyp	Ref	Expression
1		ltmuls12ad.1	|- ( ph -> A e. No )
2		ltmuls12ad.2	|- ( ph -> B e. No )
3		ltmuls12ad.3	|- ( ph -> C e. No )
4		ltmuls12ad.4	|- ( ph -> D e. No )
5		ltmuls12ad.5	|- ( ph -> 0s <_s A )
6		ltmuls12ad.6	|- ( ph -> A
7		ltmuls12ad.7	|- ( ph -> 0s <_s C )
8		ltmuls12ad.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	ltlesd	|- ( ph -> A <_s B )
13	1 2 3 7 12	lemuls1ad	|- ( ph -> ( A x.s C ) <_s ( B x.s C ) )
14		0no	|- 0s e. No
15	14	a1i	|- ( ph -> 0s e. No )
16	15 1 2 5 6	leltstrd	|- ( ph -> 0s
17	3 4 2 16	ltmuls2d	|- ( ph -> ( C ( B x.s C )
18	8 17	mpbid	|- ( ph -> ( B x.s C )
19	9 10 11 13 18	leltstrd	|- ( ph -> ( A x.s C )