This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ0 ) )

Proof

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