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