Metamath Proof Explorer

Theorem sltmuldivwd

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

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

Proof

Step Hyp Ref Expression
1 sltdivmulwd.1 ⊢ φ → A ∈ No
2 sltdivmulwd.2 ⊢ φ → B ∈ No
3 sltdivmulwd.3 ⊢ φ → C ∈ No
4 sltdivmulwd.4 ⊢ φ → 0 s < s C
5 sltdivmulwd.5 ⊢ φ → ∃ x ∈ No C ⋅ s x = 1 s
6 4 sgt0ne0d ⊢ φ → C ≠ 0 s
7 2 3 6 5 divsclwd ⊢ φ → B / su C ∈ No
8 1 7 3 4 sltmul1d ⊢ φ → A < s B / su C ↔ A ⋅ s C < s B / su C ⋅ s C
9 2 3 6 5 divscan1wd ⊢ φ → B / su C ⋅ s C = B
10 9 breq2d ⊢ φ → A ⋅ s C < s B / su C ⋅ s C ↔ A ⋅ s C < s B
11 8 10 bitr2d ⊢ φ → A ⋅ s C < s B ↔ A < s B / su C