Metamath Proof Explorer

Theorem divsdird

Description: Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 divsdird.1 ⊢ φ → A ∈ No
2 divsdird.2 ⊢ φ → B ∈ No
3 divsdird.3 ⊢ φ → C ∈ No
4 divsdird.4 ⊢ φ → C ≠ 0 s
5 1sno ⊢ 1 s ∈ No
6 5 a1i ⊢ φ → 1 s ∈ No
7 6 3 4 divscld ⊢ φ → 1 s / su C ∈ No
8 1 2 7 addsdird ⊢ φ → A + s B ⋅ s 1 s / su C = A ⋅ s 1 s / su C + s B ⋅ s 1 s / su C
9 1 2 addscld ⊢ φ → A + s B ∈ No
10 9 3 4 divsrecd ⊢ φ → A + s B / su C = A + s B ⋅ s 1 s / su C
11 1 3 4 divsrecd ⊢ φ → A / su C = A ⋅ s 1 s / su C
12 2 3 4 divsrecd ⊢ φ → B / su C = B ⋅ s 1 s / su C
13 11 12 oveq12d ⊢ φ → A / su C + s B / su C = A ⋅ s 1 s / su C + s B ⋅ s 1 s / su C
14 8 10 13 3eqtr4d ⊢ φ → A + s B / su C = A / su C + s B / su C