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 imbitrrid 
 |-  ( 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 imbitrrid 
 |-  ( 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 biimtrid 
 |-  ( 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 ) )