Metamath Proof Explorer

Theorem ltdivmulswd

Description: Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025)

Ref Expression
Hypotheses ltdivmulswd.1 ⊢ φ → A ∈ No
ltdivmulswd.2 ⊢ φ → B ∈ No
ltdivmulswd.3 ⊢ φ → C ∈ No
ltdivmulswd.4 ⊢ φ → 0 s < s C
ltdivmulswd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
Assertion ltdivmulswd ⊢ φ → A / su C < s B ↔ A < s C ⋅ s B

Proof

Step Hyp Ref Expression
1 ltdivmulswd.1 ⊢ φ → A ∈ No
2 ltdivmulswd.2 ⊢ φ → B ∈ No
3 ltdivmulswd.3 ⊢ φ → C ∈ No
4 ltdivmulswd.4 ⊢ φ → 0 s < s C
5 ltdivmulswd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
6 4 gt0ne0sd ⊢ φ → C ≠ 0 s
7 1 3 6 5 divsclwd ⊢ φ → A / su C ∈ No
8 7 2 3 4 ltmuls2d ⊢ φ → A / su C < s B ↔ C ⋅ s A / su C < s C ⋅ s B
9 1 3 6 5 divscan2wd ⊢ φ → C ⋅ s A / su C = A
10 9 breq1d ⊢ φ → C ⋅ s A / su C < s C ⋅ s B ↔ A < s C ⋅ s B
11 8 10 bitrd ⊢ φ → A / su C < s B ↔ A < s C ⋅ s B