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 imbitrrid ⊢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 imbitrrid ⊢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 biimtrid ⊢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