Metamath Proof Explorer

Theorem divscl

Description: Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025)

Ref Expression
Assertion divscl ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B ∈ No

Proof

Step Hyp Ref Expression
1 recsex ⊢ B ∈ No ∧ B ≠ 0 s → ∃ x ∈ No B ⋅ s x = 1 s
2 1 3adant1 ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → ∃ x ∈ No B ⋅ s x = 1 s
3 divsclw ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s ∧ ∃ x ∈ No B ⋅ s x = 1 s → A / su B ∈ No
4 2 3 mpdan ⊢ A ∈ No ∧ B ∈ No ∧ B ≠ 0 s → A / su B ∈ No