Metamath Proof Explorer


Theorem nn0sub

Description: Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nn0sub
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 nn0re
 |-  ( M e. NN0 -> M e. RR )
2 nn0re
 |-  ( N e. NN0 -> N e. RR )
3 leloe
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> ( M < N \/ M = N ) ) )
4 1 2 3 syl2an
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( M < N \/ M = N ) ) )
5 elnn0
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
6 elnn0
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
7 nnsub
 |-  ( ( M e. NN /\ N e. NN ) -> ( M < N <-> ( N - M ) e. NN ) )
8 7 ex
 |-  ( M e. NN -> ( N e. NN -> ( M < N <-> ( N - M ) e. NN ) ) )
9 nngt0
 |-  ( N e. NN -> 0 < N )
10 nncn
 |-  ( N e. NN -> N e. CC )
11 10 subid1d
 |-  ( N e. NN -> ( N - 0 ) = N )
12 id
 |-  ( N e. NN -> N e. NN )
13 11 12 eqeltrd
 |-  ( N e. NN -> ( N - 0 ) e. NN )
14 9 13 2thd
 |-  ( N e. NN -> ( 0 < N <-> ( N - 0 ) e. NN ) )
15 breq1
 |-  ( M = 0 -> ( M < N <-> 0 < N ) )
16 oveq2
 |-  ( M = 0 -> ( N - M ) = ( N - 0 ) )
17 16 eleq1d
 |-  ( M = 0 -> ( ( N - M ) e. NN <-> ( N - 0 ) e. NN ) )
18 15 17 bibi12d
 |-  ( M = 0 -> ( ( M < N <-> ( N - M ) e. NN ) <-> ( 0 < N <-> ( N - 0 ) e. NN ) ) )
19 14 18 syl5ibr
 |-  ( M = 0 -> ( N e. NN -> ( M < N <-> ( N - M ) e. NN ) ) )
20 8 19 jaoi
 |-  ( ( M e. NN \/ M = 0 ) -> ( N e. NN -> ( M < N <-> ( N - M ) e. NN ) ) )
21 6 20 sylbi
 |-  ( M e. NN0 -> ( N e. NN -> ( M < N <-> ( N - M ) e. NN ) ) )
22 nn0nlt0
 |-  ( M e. NN0 -> -. M < 0 )
23 22 pm2.21d
 |-  ( M e. NN0 -> ( M < 0 -> ( 0 - M ) e. NN ) )
24 nngt0
 |-  ( ( 0 - M ) e. NN -> 0 < ( 0 - M ) )
25 0re
 |-  0 e. RR
26 posdif
 |-  ( ( M e. RR /\ 0 e. RR ) -> ( M < 0 <-> 0 < ( 0 - M ) ) )
27 1 25 26 sylancl
 |-  ( M e. NN0 -> ( M < 0 <-> 0 < ( 0 - M ) ) )
28 24 27 syl5ibr
 |-  ( M e. NN0 -> ( ( 0 - M ) e. NN -> M < 0 ) )
29 23 28 impbid
 |-  ( M e. NN0 -> ( M < 0 <-> ( 0 - M ) e. NN ) )
30 breq2
 |-  ( N = 0 -> ( M < N <-> M < 0 ) )
31 oveq1
 |-  ( N = 0 -> ( N - M ) = ( 0 - M ) )
32 31 eleq1d
 |-  ( N = 0 -> ( ( N - M ) e. NN <-> ( 0 - M ) e. NN ) )
33 30 32 bibi12d
 |-  ( N = 0 -> ( ( M < N <-> ( N - M ) e. NN ) <-> ( M < 0 <-> ( 0 - M ) e. NN ) ) )
34 29 33 syl5ibrcom
 |-  ( M e. NN0 -> ( N = 0 -> ( M < N <-> ( N - M ) e. NN ) ) )
35 21 34 jaod
 |-  ( M e. NN0 -> ( ( N e. NN \/ N = 0 ) -> ( M < N <-> ( N - M ) e. NN ) ) )
36 5 35 syl5bi
 |-  ( M e. NN0 -> ( N e. NN0 -> ( M < N <-> ( N - M ) e. NN ) ) )
37 36 imp
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( N - M ) e. NN ) )
38 nn0cn
 |-  ( N e. NN0 -> N e. CC )
39 nn0cn
 |-  ( M e. NN0 -> M e. CC )
40 subeq0
 |-  ( ( N e. CC /\ M e. CC ) -> ( ( N - M ) = 0 <-> N = M ) )
41 38 39 40 syl2anr
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( N - M ) = 0 <-> N = M ) )
42 eqcom
 |-  ( N = M <-> M = N )
43 41 42 bitr2di
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M = N <-> ( N - M ) = 0 ) )
44 37 43 orbi12d
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M < N \/ M = N ) <-> ( ( N - M ) e. NN \/ ( N - M ) = 0 ) ) )
45 4 44 bitrd
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( ( N - M ) e. NN \/ ( N - M ) = 0 ) ) )
46 elnn0
 |-  ( ( N - M ) e. NN0 <-> ( ( N - M ) e. NN \/ ( N - M ) = 0 ) )
47 45 46 bitr4di
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( N - M ) e. NN0 ) )