Metamath Proof Explorer

Theorem zn0subs

Description: The non-negative difference of surreal integers is a non-negative integer. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Assertion zn0subs 
|- ( ( M e. ZZ_s /\ N e. ZZ_s ) -> ( M <_s N <-> ( N -s M ) e. NN0_s ) )

Proof

Step Hyp Ref Expression
1 zno 
 |-  ( N e. ZZ_s -> N e. No )
2 1 adantr 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> N e. No )
3 zno 
 |-  ( M e. ZZ_s -> M e. No )
4 3 adantl 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> M e. No )
5 2 4 subsge0d 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> ( 0s <_s ( N -s M ) <-> M <_s N ) )
6 simpl 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> N e. ZZ_s )
7 simpr 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> M e. ZZ_s )
8 6 7 zsubscld 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> ( N -s M ) e. ZZ_s )
9 8 biantrurd 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> ( 0s <_s ( N -s M ) <-> ( ( N -s M ) e. ZZ_s /\ 0s <_s ( N -s M ) ) ) )
10 5 9 bitr3d 
 |-  ( ( N e. ZZ_s /\ M e. ZZ_s ) -> ( M <_s N <-> ( ( N -s M ) e. ZZ_s /\ 0s <_s ( N -s M ) ) ) )
11 10 ancoms 
 |-  ( ( M e. ZZ_s /\ N e. ZZ_s ) -> ( M <_s N <-> ( ( N -s M ) e. ZZ_s /\ 0s <_s ( N -s M ) ) ) )
12 eln0zs 
 |-  ( ( N -s M ) e. NN0_s <-> ( ( N -s M ) e. ZZ_s /\ 0s <_s ( N -s M ) ) )
13 11 12 bitr4di 
 |-  ( ( M e. ZZ_s /\ N e. ZZ_s ) -> ( M <_s N <-> ( N -s M ) e. NN0_s ) )