Metamath Proof Explorer

Theorem ltdivmuls2d

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

Ref Expression
Hypotheses ltdivmulsd.1 ⊢ φ → A ∈ No
ltdivmulsd.2 ⊢ φ → B ∈ No
ltdivmulsd.3 ⊢ φ → C ∈ No
ltdivmulsd.4 ⊢ φ → 0 s < s C
Assertion ltdivmuls2d ⊢ φ → A / su C < s B ↔ A < s B ⋅ s C

Proof

Step Hyp Ref Expression
1 ltdivmulsd.1 ⊢ φ → A ∈ No
2 ltdivmulsd.2 ⊢ φ → B ∈ No
3 ltdivmulsd.3 ⊢ φ → C ∈ No
4 ltdivmulsd.4 ⊢ φ → 0 s < s C
5 4 gt0ne0sd ⊢ φ → C ≠ 0 s
6 3 5 recsexd ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
7 1 2 3 4 6 ltdivmuls2wd ⊢ φ → A / su C < s B ↔ A < s B ⋅ s C