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 0 N 0 M N N M 0

Proof

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