Metamath Proof Explorer

Theorem nnzs

Description: A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion nnzs 
|- ( A e. NN_s -> A e. ZZ_s )

Proof

Step Hyp Ref Expression
1 peano2nns 
 |-  ( A e. NN_s -> ( A +s 1s ) e. NN_s )
2 nnsno 
 |-  ( A e. NN_s -> A e. No )
3 1sno 
 |-  1s e. No
4 pncans 
 |-  ( ( A e. No /\ 1s e. No ) -> ( ( A +s 1s ) -s 1s ) = A )
5 2 3 4 sylancl 
 |-  ( A e. NN_s -> ( ( A +s 1s ) -s 1s ) = A )
6 5 eqcomd 
 |-  ( A e. NN_s -> A = ( ( A +s 1s ) -s 1s ) )
7 1nns 
 |-  1s e. NN_s
8 rspceov 
 |-  ( ( ( A +s 1s ) e. NN_s /\ 1s e. NN_s /\ A = ( ( A +s 1s ) -s 1s ) ) -> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
9 7 8 mp3an2 
 |-  ( ( ( A +s 1s ) e. NN_s /\ A = ( ( A +s 1s ) -s 1s ) ) -> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
10 1 6 9 syl2anc 
 |-  ( A e. NN_s -> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
11 elzs 
 |-  ( A e. ZZ_s <-> E. x e. NN_s E. y e. NN_s A = ( x -s y ) )
12 10 11 sylibr 
 |-  ( A e. NN_s -> A e. ZZ_s )