Metamath Proof Explorer

Theorem ltmuls12ad

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

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

Proof

Step Hyp Ref Expression
1 ltmuls12ad.1 ⊢ φ → A ∈ No
2 ltmuls12ad.2 ⊢ φ → B ∈ No
3 ltmuls12ad.3 ⊢ φ → C ∈ No
4 ltmuls12ad.4 ⊢ φ → D ∈ No
5 ltmuls12ad.5 ⊢ φ → 0 s ≤ s A
6 ltmuls12ad.6 ⊢ φ → A < s B
7 ltmuls12ad.7 ⊢ φ → 0 s ≤ s C
8 ltmuls12ad.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 ltlesd ⊢ φ → A ≤ s B
13 1 2 3 7 12 lemuls1ad ⊢ φ → A ⋅ s C ≤ s B ⋅ s C
14 0no ⊢ 0 s ∈ No
15 14 a1i ⊢ φ → 0 s ∈ No
16 15 1 2 5 6 leltstrd ⊢ φ → 0 s < s B
17 3 4 2 16 ltmuls2d ⊢ φ → 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 leltstrd ⊢ φ → A ⋅ s C < s B ⋅ s D