Metamath Proof Explorer

Theorem n0subs

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

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

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( x = 0s -> ( z <_s x <-> z <_s 0s ) )
2 oveq1 
 |-  ( x = 0s -> ( x -s z ) = ( 0s -s z ) )
3 2 eleq1d 
 |-  ( x = 0s -> ( ( x -s z ) e. NN0_s <-> ( 0s -s z ) e. NN0_s ) )
4 1 3 imbi12d 
 |-  ( x = 0s -> ( ( z <_s x -> ( x -s z ) e. NN0_s ) <-> ( z <_s 0s -> ( 0s -s z ) e. NN0_s ) ) )
5 4 ralbidv 
 |-  ( x = 0s -> ( A. z e. NN0_s ( z <_s x -> ( x -s z ) e. NN0_s ) <-> A. z e. NN0_s ( z <_s 0s -> ( 0s -s z ) e. NN0_s ) ) )
6 breq2 
 |-  ( x = y -> ( z <_s x <-> z <_s y ) )
7 oveq1 
 |-  ( x = y -> ( x -s z ) = ( y -s z ) )
8 7 eleq1d 
 |-  ( x = y -> ( ( x -s z ) e. NN0_s <-> ( y -s z ) e. NN0_s ) )
9 6 8 imbi12d 
 |-  ( x = y -> ( ( z <_s x -> ( x -s z ) e. NN0_s ) <-> ( z <_s y -> ( y -s z ) e. NN0_s ) ) )
10 9 ralbidv 
 |-  ( x = y -> ( A. z e. NN0_s ( z <_s x -> ( x -s z ) e. NN0_s ) <-> A. z e. NN0_s ( z <_s y -> ( y -s z ) e. NN0_s ) ) )
11 breq2 
 |-  ( x = ( y +s 1s ) -> ( z <_s x <-> z <_s ( y +s 1s ) ) )
12 oveq1 
 |-  ( x = ( y +s 1s ) -> ( x -s z ) = ( ( y +s 1s ) -s z ) )
13 12 eleq1d 
 |-  ( x = ( y +s 1s ) -> ( ( x -s z ) e. NN0_s <-> ( ( y +s 1s ) -s z ) e. NN0_s ) )
14 11 13 imbi12d 
 |-  ( x = ( y +s 1s ) -> ( ( z <_s x -> ( x -s z ) e. NN0_s ) <-> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
15 14 ralbidv 
 |-  ( x = ( y +s 1s ) -> ( A. z e. NN0_s ( z <_s x -> ( x -s z ) e. NN0_s ) <-> A. z e. NN0_s ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
16 breq2 
 |-  ( x = N -> ( z <_s x <-> z <_s N ) )
17 oveq1 
 |-  ( x = N -> ( x -s z ) = ( N -s z ) )
18 17 eleq1d 
 |-  ( x = N -> ( ( x -s z ) e. NN0_s <-> ( N -s z ) e. NN0_s ) )
19 16 18 imbi12d 
 |-  ( x = N -> ( ( z <_s x -> ( x -s z ) e. NN0_s ) <-> ( z <_s N -> ( N -s z ) e. NN0_s ) ) )
20 19 ralbidv 
 |-  ( x = N -> ( A. z e. NN0_s ( z <_s x -> ( x -s z ) e. NN0_s ) <-> A. z e. NN0_s ( z <_s N -> ( N -s z ) e. NN0_s ) ) )
21 n0sge0 
 |-  ( z e. NN0_s -> 0s <_s z )
22 21 biantrud 
 |-  ( z e. NN0_s -> ( z <_s 0s <-> ( z <_s 0s /\ 0s <_s z ) ) )
23 n0sno 
 |-  ( z e. NN0_s -> z e. No )
24 0sno 
 |-  0s e. No
25 sletri3 
 |-  ( ( z e. No /\ 0s e. No ) -> ( z = 0s <-> ( z <_s 0s /\ 0s <_s z ) ) )
26 23 24 25 sylancl 
 |-  ( z e. NN0_s -> ( z = 0s <-> ( z <_s 0s /\ 0s <_s z ) ) )
27 22 26 bitr4d 
 |-  ( z e. NN0_s -> ( z <_s 0s <-> z = 0s ) )
28 oveq2 
 |-  ( z = 0s -> ( 0s -s z ) = ( 0s -s 0s ) )
29 subsid 
 |-  ( 0s e. No -> ( 0s -s 0s ) = 0s )
30 24 29 ax-mp 
 |-  ( 0s -s 0s ) = 0s
31 0n0s 
 |-  0s e. NN0_s
32 30 31 eqeltri 
 |-  ( 0s -s 0s ) e. NN0_s
33 28 32 eqeltrdi 
 |-  ( z = 0s -> ( 0s -s z ) e. NN0_s )
34 27 33 biimtrdi 
 |-  ( z e. NN0_s -> ( z <_s 0s -> ( 0s -s z ) e. NN0_s ) )
35 34 rgen 
 |-  A. z e. NN0_s ( z <_s 0s -> ( 0s -s z ) e. NN0_s )
36 breq1 
 |-  ( z = x -> ( z <_s y <-> x <_s y ) )
37 oveq2 
 |-  ( z = x -> ( y -s z ) = ( y -s x ) )
38 37 eleq1d 
 |-  ( z = x -> ( ( y -s z ) e. NN0_s <-> ( y -s x ) e. NN0_s ) )
39 36 38 imbi12d 
 |-  ( z = x -> ( ( z <_s y -> ( y -s z ) e. NN0_s ) <-> ( x <_s y -> ( y -s x ) e. NN0_s ) ) )
40 39 cbvralvw 
 |-  ( A. z e. NN0_s ( z <_s y -> ( y -s z ) e. NN0_s ) <-> A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) )
41 n0sno 
 |-  ( y e. NN0_s -> y e. No )
42 peano2no 
 |-  ( y e. No -> ( y +s 1s ) e. No )
43 subsid1 
 |-  ( ( y +s 1s ) e. No -> ( ( y +s 1s ) -s 0s ) = ( y +s 1s ) )
44 41 42 43 3syl 
 |-  ( y e. NN0_s -> ( ( y +s 1s ) -s 0s ) = ( y +s 1s ) )
45 peano2n0s 
 |-  ( y e. NN0_s -> ( y +s 1s ) e. NN0_s )
46 44 45 eqeltrd 
 |-  ( y e. NN0_s -> ( ( y +s 1s ) -s 0s ) e. NN0_s )
47 oveq2 
 |-  ( z = 0s -> ( ( y +s 1s ) -s z ) = ( ( y +s 1s ) -s 0s ) )
48 47 eleq1d 
 |-  ( z = 0s -> ( ( ( y +s 1s ) -s z ) e. NN0_s <-> ( ( y +s 1s ) -s 0s ) e. NN0_s ) )
49 46 48 syl5ibrcom 
 |-  ( y e. NN0_s -> ( z = 0s -> ( ( y +s 1s ) -s z ) e. NN0_s ) )
50 49 2a1dd 
 |-  ( y e. NN0_s -> ( z = 0s -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) ) )
51 50 adantr 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( z = 0s -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) ) )
52 breq1 
 |-  ( x = ( z -s 1s ) -> ( x <_s y <-> ( z -s 1s ) <_s y ) )
53 oveq2 
 |-  ( x = ( z -s 1s ) -> ( y -s x ) = ( y -s ( z -s 1s ) ) )
54 53 eleq1d 
 |-  ( x = ( z -s 1s ) -> ( ( y -s x ) e. NN0_s <-> ( y -s ( z -s 1s ) ) e. NN0_s ) )
55 52 54 imbi12d 
 |-  ( x = ( z -s 1s ) -> ( ( x <_s y -> ( y -s x ) e. NN0_s ) <-> ( ( z -s 1s ) <_s y -> ( y -s ( z -s 1s ) ) e. NN0_s ) ) )
56 55 rspcv 
 |-  ( ( z -s 1s ) e. NN0_s -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> ( ( z -s 1s ) <_s y -> ( y -s ( z -s 1s ) ) e. NN0_s ) ) )
57 23 adantl 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> z e. No )
58 1sno 
 |-  1s e. No
59 58 a1i 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> 1s e. No )
60 41 adantr 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> y e. No )
61 57 59 60 slesubaddd 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( z -s 1s ) <_s y <-> z <_s ( y +s 1s ) ) )
62 60 57 59 subsubs2d 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( y -s ( z -s 1s ) ) = ( y +s ( 1s -s z ) ) )
63 60 59 57 addsubsassd 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( y +s 1s ) -s z ) = ( y +s ( 1s -s z ) ) )
64 62 63 eqtr4d 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( y -s ( z -s 1s ) ) = ( ( y +s 1s ) -s z ) )
65 64 eleq1d 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( y -s ( z -s 1s ) ) e. NN0_s <-> ( ( y +s 1s ) -s z ) e. NN0_s ) )
66 61 65 imbi12d 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( ( z -s 1s ) <_s y -> ( y -s ( z -s 1s ) ) e. NN0_s ) <-> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
67 66 biimpd 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( ( z -s 1s ) <_s y -> ( y -s ( z -s 1s ) ) e. NN0_s ) -> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
68 56 67 syl9r 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( ( z -s 1s ) e. NN0_s -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) ) )
69 n0s0m1 
 |-  ( z e. NN0_s -> ( z = 0s \/ ( z -s 1s ) e. NN0_s ) )
70 69 adantl 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( z = 0s \/ ( z -s 1s ) e. NN0_s ) )
71 51 68 70 mpjaod 
 |-  ( ( y e. NN0_s /\ z e. NN0_s ) -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
72 71 ralrimdva 
 |-  ( y e. NN0_s -> ( A. x e. NN0_s ( x <_s y -> ( y -s x ) e. NN0_s ) -> A. z e. NN0_s ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
73 40 72 biimtrid 
 |-  ( y e. NN0_s -> ( A. z e. NN0_s ( z <_s y -> ( y -s z ) e. NN0_s ) -> A. z e. NN0_s ( z <_s ( y +s 1s ) -> ( ( y +s 1s ) -s z ) e. NN0_s ) ) )
74 5 10 15 20 35 73 n0sind 
 |-  ( N e. NN0_s -> A. z e. NN0_s ( z <_s N -> ( N -s z ) e. NN0_s ) )
75 breq1 
 |-  ( z = M -> ( z <_s N <-> M <_s N ) )
76 oveq2 
 |-  ( z = M -> ( N -s z ) = ( N -s M ) )
77 76 eleq1d 
 |-  ( z = M -> ( ( N -s z ) e. NN0_s <-> ( N -s M ) e. NN0_s ) )
78 75 77 imbi12d 
 |-  ( z = M -> ( ( z <_s N -> ( N -s z ) e. NN0_s ) <-> ( M <_s N -> ( N -s M ) e. NN0_s ) ) )
79 78 rspcva 
 |-  ( ( M e. NN0_s /\ A. z e. NN0_s ( z <_s N -> ( N -s z ) e. NN0_s ) ) -> ( M <_s N -> ( N -s M ) e. NN0_s ) )
80 74 79 sylan2 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N -> ( N -s M ) e. NN0_s ) )
81 n0sge0 
 |-  ( ( N -s M ) e. NN0_s -> 0s <_s ( N -s M ) )
82 n0sno 
 |-  ( N e. NN0_s -> N e. No )
83 82 adantl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. No )
84 n0sno 
 |-  ( M e. NN0_s -> M e. No )
85 84 adantr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> M e. No )
86 83 85 subsge0d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( 0s <_s ( N -s M ) <-> M <_s N ) )
87 81 86 imbitrid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N -s M ) e. NN0_s -> M <_s N ) )
88 80 87 impbid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> ( N -s M ) e. NN0_s ) )