Metamath Proof Explorer

Theorem divdivs1d

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

Ref Expression
Hypotheses divdivs1d.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
divdivs1d.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
divdivs1d.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
divdivs1d.4 ⊢ ( 𝜑 → 𝐵 ≠ 0s )
divdivs1d.5 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
Assertion divdivs1d ( 𝜑 → ( ( 𝐴 /su 𝐵 ) /su 𝐶 ) = ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 divdivs1d.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 divdivs1d.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 divdivs1d.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 divdivs1d.4 ⊢ ( 𝜑 → 𝐵 ≠ 0s )
5 divdivs1d.5 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
6 2 3 mulscld ⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
7 2 3 mulsne0bd ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) ≠ 0s ↔ ( 𝐵 ≠ 0s ∧ 𝐶 ≠ 0s ) ) )
8 4 5 7 mpbir2and ⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ≠ 0s )
9 1 6 8 divscld ⊢ ( 𝜑 → ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ∈ No )
10 2 3 9 mulsassd ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) = ( 𝐵 ·s ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) ) )
11 1 6 8 divscan2d ⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) = 𝐴 )
12 10 11 eqtr3d ⊢ ( 𝜑 → ( 𝐵 ·s ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) ) = 𝐴 )
13 3 9 mulscld ⊢ ( 𝜑 → ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) ∈ No )
14 1 13 2 4 divmulsd ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐵 ) = ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) ↔ ( 𝐵 ·s ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) ) = 𝐴 ) )
15 12 14 mpbird ⊢ ( 𝜑 → ( 𝐴 /su 𝐵 ) = ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) )
16 15 eqcomd ⊢ ( 𝜑 → ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) = ( 𝐴 /su 𝐵 ) )
17 1 2 4 divscld ⊢ ( 𝜑 → ( 𝐴 /su 𝐵 ) ∈ No )
18 17 9 3 5 divmulsd ⊢ ( 𝜑 → ( ( ( 𝐴 /su 𝐵 ) /su 𝐶 ) = ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ↔ ( 𝐶 ·s ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) ) = ( 𝐴 /su 𝐵 ) ) )
19 16 18 mpbird ⊢ ( 𝜑 → ( ( 𝐴 /su 𝐵 ) /su 𝐶 ) = ( 𝐴 /su ( 𝐵 ·s 𝐶 ) ) )