Metamath Proof Explorer

Theorem n0subs2

Description: Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion n0subs2 
|- ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( N -s M ) e. NN_s ) )

Proof

Step Hyp Ref Expression
1 n0subs 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> ( N -s M ) e. NN0_s ) )
2 n0sno 
 |-  ( N e. NN0_s -> N e. No )
3 2 adantl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. No )
4 n0sno 
 |-  ( M e. NN0_s -> M e. No )
5 4 adantr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> M e. No )
6 3 5 subseq0d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N -s M ) = 0s <-> N = M ) )
7 6 necon3bid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N -s M ) =/= 0s <-> N =/= M ) )
8 7 bicomd 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( N =/= M <-> ( N -s M ) =/= 0s ) )
9 1 8 anbi12d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( M <_s N /\ N =/= M ) <-> ( ( N -s M ) e. NN0_s /\ ( N -s M ) =/= 0s ) ) )
10 5 3 sltlend 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( M <_s N /\ N =/= M ) ) )
11 elnns 
 |-  ( ( N -s M ) e. NN_s <-> ( ( N -s M ) e. NN0_s /\ ( N -s M ) =/= 0s ) )
12 11 a1i 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N -s M ) e. NN_s <-> ( ( N -s M ) e. NN0_s /\ ( N -s M ) =/= 0s ) ) )
13 9 10 12 3bitr4d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( N -s M ) e. NN_s ) )