Theorem sltmul12ad

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

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

Proof

Step	Hyp	Ref	Expression
1		sltmul12ad.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltmul12ad.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		sltmul12ad.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		sltmul12ad.4	⊢ ( 𝜑 → 𝐷 ∈ No )
5		sltmul12ad.5	⊢ ( 𝜑 → 0s ≤s 𝐴 )
6		sltmul12ad.6	⊢ ( 𝜑 → 𝐴 <s 𝐵 )
7		sltmul12ad.7	⊢ ( 𝜑 → 0s ≤s 𝐶 )
8		sltmul12ad.8	⊢ ( 𝜑 → 𝐶 <s 𝐷 )
9	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
10	2 3	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
11	2 4	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐷 ) ∈ No )
12	1 2 6	sltled	⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )
13	1 2 3 7 12	slemul1ad	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ≤s ( 𝐵 ·s 𝐶 ) )
14		0sno	⊢ 0s ∈ No
15	14	a1i	⊢ ( 𝜑 → 0s ∈ No )
16	15 1 2 5 6	slelttrd	⊢ ( 𝜑 → 0s <s 𝐵 )
17	3 4 2 16	sltmul2d	⊢ ( 𝜑 → ( 𝐶 <s 𝐷 ↔ ( 𝐵 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) ) )
18	8 17	mpbid	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) )
19	9 10 11 13 18	slelttrd	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) <s ( 𝐵 ·s 𝐷 ) )