Metamath Proof Explorer

Theorem norecdiv

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

Ref Expression
Assertion norecdiv ⊢ 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 simprl ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → w ∈ No
2 simpl3 ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → B ∈ No
3 1 2 mulscld ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → w ⋅ s B ∈ No
4 oveq1 ⊢ A ⋅ s w = 1 s → A ⋅ s w ⋅ s B = 1 s ⋅ s B
5 4 adantl ⊢ w ∈ No ∧ A ⋅ s w = 1 s → A ⋅ s w ⋅ s B = 1 s ⋅ s B
6 5 adantl ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → A ⋅ s w ⋅ s B = 1 s ⋅ s B
7 simpl1 ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → A ∈ No
8 7 1 2 mulsassd ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → A ⋅ s w ⋅ s B = A ⋅ s w ⋅ s B
9 2 mulslidd ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → 1 s ⋅ s B = B
10 6 8 9 3eqtr3d ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → A ⋅ s w ⋅ s B = B
11 oveq2 ⊢ z = w ⋅ s B → A ⋅ s z = A ⋅ s w ⋅ s B
12 11 eqeq1d ⊢ z = w ⋅ s B → A ⋅ s z = B ↔ A ⋅ s w ⋅ s B = B
13 12 rspcev ⊢ w ⋅ s B ∈ No ∧ A ⋅ s w ⋅ s B = B → ∃ z ∈ No A ⋅ s z = B
14 3 10 13 syl2anc ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ w ∈ No ∧ A ⋅ s w = 1 s → ∃ z ∈ No A ⋅ s z = B
15 14 rexlimdvaa ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No → ∃ w ∈ No A ⋅ s w = 1 s → ∃ z ∈ No A ⋅ s z = B
16 15 imp ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ w ∈ No A ⋅ s w = 1 s → ∃ z ∈ No A ⋅ s z = B
17 oveq2 ⊢ x = w → A ⋅ s x = A ⋅ s w
18 17 eqeq1d ⊢ x = w → A ⋅ s x = 1 s ↔ A ⋅ s w = 1 s
19 18 cbvrexvw ⊢ ∃ x ∈ No A ⋅ s x = 1 s ↔ ∃ w ∈ No A ⋅ s w = 1 s
20 19 anbi2i ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s ↔ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ w ∈ No A ⋅ s w = 1 s
21 oveq2 ⊢ y = z → A ⋅ s y = A ⋅ s z
22 21 eqeq1d ⊢ y = z → A ⋅ s y = B ↔ A ⋅ s z = B
23 22 cbvrexvw ⊢ ∃ y ∈ No A ⋅ s y = B ↔ ∃ z ∈ No A ⋅ s z = B
24 16 20 23 3imtr4i ⊢ A ∈ No ∧ A ≠ 0 s ∧ B ∈ No ∧ ∃ x ∈ No A ⋅ s x = 1 s → ∃ y ∈ No A ⋅ s y = B