Theorem ltmuls12ad

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

	Ref	Expression
Hypotheses	ltmuls12ad.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	ltmuls12ad.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	ltmuls12ad.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	ltmuls12ad.4	⊢ ( 𝜑 → 𝐷 ∈ No )
	ltmuls12ad.5	⊢ ( 𝜑 → 0s ≤s 𝐴 )
	ltmuls12ad.6	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
	ltmuls12ad.7	⊢ ( 𝜑 → 0s ≤s 𝐶 )
	ltmuls12ad.8	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
Assertion	ltmuls12ad	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		ltmuls12ad.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		ltmuls12ad.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		ltmuls12ad.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		ltmuls12ad.4	⊢ ( 𝜑 → 𝐷 ∈ No )
5		ltmuls12ad.5	⊢ ( 𝜑 → 0s ≤s 𝐴 )
6		ltmuls12ad.6	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
7		ltmuls12ad.7	⊢ ( 𝜑 → 0s ≤s 𝐶 )
8		ltmuls12ad.8	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
9	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
10	2 3	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
11	2 4	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐷 ) ∈ No )
12	1 2 6	ltlesd	⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )
13	1 2 3 7 12	lemuls1ad	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) )
14		0no	⊢ 0s ∈ No
15	14	a1i	⊢ ( 𝜑 → 0s ∈ No )
16	15 1 2 5 6	leltstrd	⊢ ( 𝜑 → 0s <s 𝐵 )
17	3 4 2 16	ltmuls2d	⊢ ( 𝜑 → ( 𝐶 <s 𝐷 ↔ ( 𝐵 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) ) )
18	8 17	mpbid	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) )
19	9 10 11 13 18	leltstrd	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) )