Metamath Proof Explorer

Theorem divmuldivsd

Description: Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Hypotheses divmuldivsd.1 ⊢ φ → A ∈ No
divmuldivsd.2 ⊢ φ → B ∈ No
divmuldivsd.3 ⊢ φ → C ∈ No
divmuldivsd.4 ⊢ φ → D ∈ No
divmuldivsd.5 ⊢ φ → B ≠ 0 s
divmuldivsd.6 ⊢ φ → D ≠ 0 s
Assertion divmuldivsd ⊢ φ → A / su B ⋅ s C / su D = A ⋅ s C / su B ⋅ s D

Proof

Step Hyp Ref Expression
1 divmuldivsd.1 ⊢ φ → A ∈ No
2 divmuldivsd.2 ⊢ φ → B ∈ No
3 divmuldivsd.3 ⊢ φ → C ∈ No
4 divmuldivsd.4 ⊢ φ → D ∈ No
5 divmuldivsd.5 ⊢ φ → B ≠ 0 s
6 divmuldivsd.6 ⊢ φ → D ≠ 0 s
7 1 2 5 divscld ⊢ φ → A / su B ∈ No
8 3 4 6 divscld ⊢ φ → C / su D ∈ No
9 2 4 7 8 muls4d ⊢ φ → B ⋅ s D ⋅ s A / su B ⋅ s C / su D = B ⋅ s A / su B ⋅ s D ⋅ s C / su D
10 1 2 5 divscan2d ⊢ φ → B ⋅ s A / su B = A
11 3 4 6 divscan2d ⊢ φ → D ⋅ s C / su D = C
12 10 11 oveq12d ⊢ φ → B ⋅ s A / su B ⋅ s D ⋅ s C / su D = A ⋅ s C
13 9 12 eqtrd ⊢ φ → B ⋅ s D ⋅ s A / su B ⋅ s C / su D = A ⋅ s C
14 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
15 7 8 mulscld ⊢ φ → A / su B ⋅ s C / su D ∈ No
16 2 4 mulscld ⊢ φ → B ⋅ s D ∈ No
17 2 4 mulsne0bd ⊢ φ → B ⋅ s D ≠ 0 s ↔ B ≠ 0 s ∧ D ≠ 0 s
18 5 6 17 mpbir2and ⊢ φ → B ⋅ s D ≠ 0 s
19 14 15 16 18 divsmuld ⊢ φ → A ⋅ s C / su B ⋅ s D = A / su B ⋅ s C / su D ↔ B ⋅ s D ⋅ s A / su B ⋅ s C / su D = A ⋅ s C
20 13 19 mpbird ⊢ φ → A ⋅ s C / su B ⋅ s D = A / su B ⋅ s C / su D
21 20 eqcomd ⊢ φ → A / su B ⋅ s C / su D = A ⋅ s C / su B ⋅ s D