Metamath Proof Explorer

Theorem sltmul12ad

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

Ref Expression
Hypotheses sltmul12ad.1 ⊢ φ → A ∈ No
sltmul12ad.2 ⊢ φ → B ∈ No
sltmul12ad.3 ⊢ φ → C ∈ No
sltmul12ad.4 ⊢ φ → D ∈ No
sltmul12ad.5 ⊢ φ → 0 s ≤ s A
sltmul12ad.6 ⊢ φ → A < s B
sltmul12ad.7 ⊢ φ → 0 s ≤ s C
sltmul12ad.8 ⊢ φ → C < s D
Assertion sltmul12ad ⊢ φ → A ⋅ s C < s B ⋅ s D

Proof

Step Hyp Ref Expression
1 sltmul12ad.1 ⊢ φ → A ∈ No
2 sltmul12ad.2 ⊢ φ → B ∈ No
3 sltmul12ad.3 ⊢ φ → C ∈ No
4 sltmul12ad.4 ⊢ φ → D ∈ No
5 sltmul12ad.5 ⊢ φ → 0 s ≤ s A
6 sltmul12ad.6 ⊢ φ → A < s B
7 sltmul12ad.7 ⊢ φ → 0 s ≤ s C
8 sltmul12ad.8 ⊢ φ → C < s D
9 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
10 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
11 2 4 mulscld ⊢ φ → B ⋅ s D ∈ No
12 1 2 6 sltled ⊢ φ → A ≤ s B
13 1 2 3 7 12 slemul1ad ⊢ φ → A ⋅ s C ≤ s B ⋅ s C
14 0sno ⊢ 0 s ∈ No
15 14 a1i ⊢ φ → 0 s ∈ No
16 15 1 2 5 6 slelttrd ⊢ φ → 0 s < s B
17 3 4 2 16 sltmul2d ⊢ φ → C < s D ↔ B ⋅ s C < s B ⋅ s D
18 8 17 mpbid ⊢ φ → B ⋅ s C < s B ⋅ s D
19 9 10 11 13 18 slelttrd ⊢ φ → A ⋅ s C < s B ⋅ s D