Metamath Proof Explorer

Theorem elzn0s

Description: A surreal integer is a surreal that is a non-negative integer or whose negative is a non-negative integer. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion elzn0s 
|- ( A e. ZZ_s <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )

Proof

Step Hyp Ref Expression
1 elzs 
 |-  ( A e. ZZ_s <-> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
2 nnsno 
 |-  ( n e. NN_s -> n e. No )
3 nnsno 
 |-  ( m e. NN_s -> m e. No )
4 subscl 
 |-  ( ( n e. No /\ m e. No ) -> ( n -s m ) e. No )
5 2 3 4 syl2an 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( n -s m ) e. No )
6 sletric 
 |-  ( ( m e. No /\ n e. No ) -> ( m <_s n \/ n <_s m ) )
7 3 2 6 syl2anr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( m <_s n \/ n <_s m ) )
8 nnn0s 
 |-  ( m e. NN_s -> m e. NN0_s )
9 nnn0s 
 |-  ( n e. NN_s -> n e. NN0_s )
10 n0subs 
 |-  ( ( m e. NN0_s /\ n e. NN0_s ) -> ( m <_s n <-> ( n -s m ) e. NN0_s ) )
11 8 9 10 syl2anr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( m <_s n <-> ( n -s m ) e. NN0_s ) )
12 n0subs 
 |-  ( ( n e. NN0_s /\ m e. NN0_s ) -> ( n <_s m <-> ( m -s n ) e. NN0_s ) )
13 9 8 12 syl2an 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( n <_s m <-> ( m -s n ) e. NN0_s ) )
14 2 adantr 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> n e. No )
15 3 adantl 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> m e. No )
16 14 15 negsubsdi2d 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( -us ` ( n -s m ) ) = ( m -s n ) )
17 16 eleq1d 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( ( -us ` ( n -s m ) ) e. NN0_s <-> ( m -s n ) e. NN0_s ) )
18 13 17 bitr4d 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( n <_s m <-> ( -us ` ( n -s m ) ) e. NN0_s ) )
19 11 18 orbi12d 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( ( m <_s n \/ n <_s m ) <-> ( ( n -s m ) e. NN0_s \/ ( -us ` ( n -s m ) ) e. NN0_s ) ) )
20 7 19 mpbid 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( ( n -s m ) e. NN0_s \/ ( -us ` ( n -s m ) ) e. NN0_s ) )
21 5 20 jca 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( ( n -s m ) e. No /\ ( ( n -s m ) e. NN0_s \/ ( -us ` ( n -s m ) ) e. NN0_s ) ) )
22 eleq1 
 |-  ( A = ( n -s m ) -> ( A e. No <-> ( n -s m ) e. No ) )
23 eleq1 
 |-  ( A = ( n -s m ) -> ( A e. NN0_s <-> ( n -s m ) e. NN0_s ) )
24 fveq2 
 |-  ( A = ( n -s m ) -> ( -us ` A ) = ( -us ` ( n -s m ) ) )
25 24 eleq1d 
 |-  ( A = ( n -s m ) -> ( ( -us ` A ) e. NN0_s <-> ( -us ` ( n -s m ) ) e. NN0_s ) )
26 23 25 orbi12d 
 |-  ( A = ( n -s m ) -> ( ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) <-> ( ( n -s m ) e. NN0_s \/ ( -us ` ( n -s m ) ) e. NN0_s ) ) )
27 22 26 anbi12d 
 |-  ( A = ( n -s m ) -> ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) <-> ( ( n -s m ) e. No /\ ( ( n -s m ) e. NN0_s \/ ( -us ` ( n -s m ) ) e. NN0_s ) ) ) )
28 21 27 syl5ibrcom 
 |-  ( ( n e. NN_s /\ m e. NN_s ) -> ( A = ( n -s m ) -> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) ) )
29 28 rexlimivv 
 |-  ( E. n e. NN_s E. m e. NN_s A = ( n -s m ) -> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )
30 n0p1nns 
 |-  ( A e. NN0_s -> ( A +s 1s ) e. NN_s )
31 1nns 
 |-  1s e. NN_s
32 31 a1i 
 |-  ( A e. NN0_s -> 1s e. NN_s )
33 n0sno 
 |-  ( A e. NN0_s -> A e. No )
34 1sno 
 |-  1s e. No
35 pncans 
 |-  ( ( A e. No /\ 1s e. No ) -> ( ( A +s 1s ) -s 1s ) = A )
36 33 34 35 sylancl 
 |-  ( A e. NN0_s -> ( ( A +s 1s ) -s 1s ) = A )
37 36 eqcomd 
 |-  ( A e. NN0_s -> A = ( ( A +s 1s ) -s 1s ) )
38 rspceov 
 |-  ( ( ( A +s 1s ) e. NN_s /\ 1s e. NN_s /\ A = ( ( A +s 1s ) -s 1s ) ) -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
39 30 32 37 38 syl3anc 
 |-  ( A e. NN0_s -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
40 39 adantl 
 |-  ( ( A e. No /\ A e. NN0_s ) -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
41 31 a1i 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> 1s e. NN_s )
42 34 a1i 
 |-  ( A e. No -> 1s e. No )
43 id 
 |-  ( A e. No -> A e. No )
44 42 43 subsvald 
 |-  ( A e. No -> ( 1s -s A ) = ( 1s +s ( -us ` A ) ) )
45 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
46 42 45 addscomd 
 |-  ( A e. No -> ( 1s +s ( -us ` A ) ) = ( ( -us ` A ) +s 1s ) )
47 44 46 eqtrd 
 |-  ( A e. No -> ( 1s -s A ) = ( ( -us ` A ) +s 1s ) )
48 47 adantr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( 1s -s A ) = ( ( -us ` A ) +s 1s ) )
49 n0p1nns 
 |-  ( ( -us ` A ) e. NN0_s -> ( ( -us ` A ) +s 1s ) e. NN_s )
50 49 adantl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( ( -us ` A ) +s 1s ) e. NN_s )
51 48 50 eqeltrd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( 1s -s A ) e. NN_s )
52 42 43 nncansd 
 |-  ( A e. No -> ( 1s -s ( 1s -s A ) ) = A )
53 52 eqcomd 
 |-  ( A e. No -> A = ( 1s -s ( 1s -s A ) ) )
54 53 adantr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> A = ( 1s -s ( 1s -s A ) ) )
55 rspceov 
 |-  ( ( 1s e. NN_s /\ ( 1s -s A ) e. NN_s /\ A = ( 1s -s ( 1s -s A ) ) ) -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
56 41 51 54 55 syl3anc 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
57 40 56 jaodan 
 |-  ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) -> E. n e. NN_s E. m e. NN_s A = ( n -s m ) )
58 29 57 impbii 
 |-  ( E. n e. NN_s E. m e. NN_s A = ( n -s m ) <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )
59 1 58 bitri 
 |-  ( A e. ZZ_s <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )