Metamath Proof Explorer

Theorem noreceuw

Description: If a surreal has a reciprocal, then it has unique division. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Assertion noreceuw ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s → ∃! y ∈ No A ⋅ s y = B

Proof

Step Hyp Ref Expression
1 norecdiv ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s → ∃ y ∈ No A ⋅ s y = B
2 divsmo ⊢ A ∈ No ∧ A ≠ 0 s → ∃* y ∈ No A ⋅ s y = B
3 2 3adant3 ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No → ∃* y ∈ No A ⋅ s y = B
4 3 adantr ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s → ∃* y ∈ No A ⋅ s y = B
5 reu5 ⊢ ∃! y ∈ No A ⋅ s y = B ↔ ∃ y ∈ No A ⋅ s y = B ∧ ∃* y ∈ No A ⋅ s y = B
6 1 4 5 sylanbrc ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s → ∃! y ∈ No A ⋅ s y = B