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≠0s∧B∈No∧∃x∈NoA⋅sx=1s→∃y∈NoA⋅sy=B

Proof

Step Hyp Ref Expression
1 simprl ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→w∈No
2 simpl3 ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→B∈No
3 1 2 mulscld ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→w⋅sB∈No
4 oveq1 ⊢A⋅sw=1s→A⋅sw⋅sB=1s⋅sB
5 4 adantl ⊢w∈No∧A⋅sw=1s→A⋅sw⋅sB=1s⋅sB
6 5 adantl ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→A⋅sw⋅sB=1s⋅sB
7 simpl1 ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→A∈No
8 7 1 2 mulsassd ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→A⋅sw⋅sB=A⋅sw⋅sB
9 2 mulslidd ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→1s⋅sB=B
10 6 8 9 3eqtr3d ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→A⋅sw⋅sB=B
11 oveq2 ⊢z=w⋅sB→A⋅sz=A⋅sw⋅sB
12 11 eqeq1d ⊢z=w⋅sB→A⋅sz=B↔A⋅sw⋅sB=B
13 12 rspcev ⊢w⋅sB∈No∧A⋅sw⋅sB=B→∃z∈NoA⋅sz=B
14 3 10 13 syl2anc ⊢A∈No∧A≠0s∧B∈No∧w∈No∧A⋅sw=1s→∃z∈NoA⋅sz=B
15 14 rexlimdvaa ⊢A∈No∧A≠0s∧B∈No→∃w∈NoA⋅sw=1s→∃z∈NoA⋅sz=B
16 15 imp ⊢A∈No∧A≠0s∧B∈No∧∃w∈NoA⋅sw=1s→∃z∈NoA⋅sz=B
17 oveq2 ⊢x=w→A⋅sx=A⋅sw
18 17 eqeq1d ⊢x=w→A⋅sx=1s↔A⋅sw=1s
19 18 cbvrexvw ⊢∃x∈NoA⋅sx=1s↔∃w∈NoA⋅sw=1s
20 19 anbi2i ⊢A∈No∧A≠0s∧B∈No∧∃x∈NoA⋅sx=1s↔A∈No∧A≠0s∧B∈No∧∃w∈NoA⋅sw=1s
21 oveq2 ⊢y=z→A⋅sy=A⋅sz
22 21 eqeq1d ⊢y=z→A⋅sy=B↔A⋅sz=B
23 22 cbvrexvw ⊢∃y∈NoA⋅sy=B↔∃z∈NoA⋅sz=B
24 16 20 23 3imtr4i ⊢A∈No∧A≠0s∧B∈No∧∃x∈NoA⋅sx=1s→∃y∈NoA⋅sy=B