Metamath Proof Explorer

Theorem divs1

Description: A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Assertion divs1 
|- ( A e. No -> ( A /su 1s ) = A )

Proof

Step Hyp Ref Expression
1 mulslid 
 |-  ( A e. No -> ( 1s x.s A ) = A )
2 1sno 
 |-  1s e. No
3 0slt1s 
 |-  0s
4 sgt0ne0 
 |-  ( 0s  1s =/= 0s )
5 3 4 ax-mp 
 |-  1s =/= 0s
6 2 5 pm3.2i 
 |-  ( 1s e. No /\ 1s =/= 0s )
7 mulslid 
 |-  ( 1s e. No -> ( 1s x.s 1s ) = 1s )
8 2 7 ax-mp 
 |-  ( 1s x.s 1s ) = 1s
9 oveq2 
 |-  ( x = 1s -> ( 1s x.s x ) = ( 1s x.s 1s ) )
10 9 eqeq1d 
 |-  ( x = 1s -> ( ( 1s x.s x ) = 1s <-> ( 1s x.s 1s ) = 1s ) )
11 10 rspcev 
 |-  ( ( 1s e. No /\ ( 1s x.s 1s ) = 1s ) -> E. x e. No ( 1s x.s x ) = 1s )
12 2 8 11 mp2an 
 |-  E. x e. No ( 1s x.s x ) = 1s
13 divsmulw 
 |-  ( ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) /\ E. x e. No ( 1s x.s x ) = 1s ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
14 12 13 mpan2 
 |-  ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
15 6 14 mp3an3 
 |-  ( ( A e. No /\ A e. No ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
16 15 anidms 
 |-  ( A e. No -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
17 1 16 mpbird 
 |-  ( A e. No -> ( A /su 1s ) = A )