Metamath Proof Explorer

Theorem divsrecd

Description: Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 divsrecd.1 ⊢ φ → A ∈ No
2 divsrecd.2 ⊢ φ → B ∈ No
3 divsrecd.3 ⊢ φ → B ≠ 0 s
4 1sno ⊢ 1 s ∈ No
5 4 a1i ⊢ φ → 1 s ∈ No
6 5 2 3 divscld ⊢ φ → 1 s / su B ∈ No
7 2 1 6 muls12d ⊢ φ → B ⋅ s A ⋅ s 1 s / su B = A ⋅ s B ⋅ s 1 s / su B
8 5 2 3 divscan2d ⊢ φ → B ⋅ s 1 s / su B = 1 s
9 8 oveq2d ⊢ φ → A ⋅ s B ⋅ s 1 s / su B = A ⋅ s 1 s
10 1 mulsridd ⊢ φ → A ⋅ s 1 s = A
11 7 9 10 3eqtrd ⊢ φ → B ⋅ s A ⋅ s 1 s / su B = A
12 1 6 mulscld ⊢ φ → A ⋅ s 1 s / su B ∈ No
13 1 12 2 3 divsmuld ⊢ φ → A / su B = A ⋅ s 1 s / su B ↔ B ⋅ s A ⋅ s 1 s / su B = A
14 11 13 mpbird ⊢ φ → A / su B = A ⋅ s 1 s / su B