Metamath Proof Explorer

Theorem divdivs1d

Description: Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025)

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

Proof

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