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 1sne0s 
 |-  1s =/= 0s
4 2 3 pm3.2i 
 |-  ( 1s e. No /\ 1s =/= 0s )
5 mulslid 
 |-  ( 1s e. No -> ( 1s x.s 1s ) = 1s )
6 2 5 ax-mp 
 |-  ( 1s x.s 1s ) = 1s
7 oveq2 
 |-  ( x = 1s -> ( 1s x.s x ) = ( 1s x.s 1s ) )
8 7 eqeq1d 
 |-  ( x = 1s -> ( ( 1s x.s x ) = 1s <-> ( 1s x.s 1s ) = 1s ) )
9 8 rspcev 
 |-  ( ( 1s e. No /\ ( 1s x.s 1s ) = 1s ) -> E. x e. No ( 1s x.s x ) = 1s )
10 2 6 9 mp2an 
 |-  E. x e. No ( 1s x.s x ) = 1s
11 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 ) )
12 10 11 mpan2 
 |-  ( ( A e. No /\ A e. No /\ ( 1s e. No /\ 1s =/= 0s ) ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
13 4 12 mp3an3 
 |-  ( ( A e. No /\ A e. No ) -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
14 13 anidms 
 |-  ( A e. No -> ( ( A /su 1s ) = A <-> ( 1s x.s A ) = A ) )
15 1 14 mpbird 
 |-  ( A e. No -> ( A /su 1s ) = A )