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

Metamath Proof Explorer

Theorem 0mnnnnn0

Description: The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018)

Ref Expression
Assertion 0mnnnnn0 ⊢ N ∈ ℕ → 0 − N ∉ ℕ 0

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 nnel ⊢ ¬ 0 − N ∉ ℕ 0 ↔ 0 − N ∈ ℕ 0
3 df-neg ⊢ − N = 0 − N
4 3 eqcomi ⊢ 0 − N = − N
5 4 eleq1i ⊢ 0 − N ∈ ℕ 0 ↔ − N ∈ ℕ 0
6 nn0ge0 ⊢ − N ∈ ℕ 0 → 0 ≤ − N
7 nnre ⊢ N ∈ ℕ → N ∈ ℝ
8 7 le0neg1d ⊢ N ∈ ℕ → N ≤ 0 ↔ 0 ≤ − N
9 nngt0 ⊢ N ∈ ℕ → 0 < N
10 0red ⊢ N ∈ ℕ → 0 ∈ ℝ
11 10 7 ltnled ⊢ N ∈ ℕ → 0 < N ↔ ¬ N ≤ 0
12 pm2.21 ⊢ ¬ N ≤ 0 → N ≤ 0 → ¬ 0 ∈ ℝ
13 11 12 biimtrdi ⊢ N ∈ ℕ → 0 < N → N ≤ 0 → ¬ 0 ∈ ℝ
14 9 13 mpd ⊢ N ∈ ℕ → N ≤ 0 → ¬ 0 ∈ ℝ
15 8 14 sylbird ⊢ N ∈ ℕ → 0 ≤ − N → ¬ 0 ∈ ℝ
16 6 15 syl5 ⊢ N ∈ ℕ → − N ∈ ℕ 0 → ¬ 0 ∈ ℝ
17 5 16 biimtrid ⊢ N ∈ ℕ → 0 − N ∈ ℕ 0 → ¬ 0 ∈ ℝ
18 2 17 biimtrid ⊢ N ∈ ℕ → ¬ 0 − N ∉ ℕ 0 → ¬ 0 ∈ ℝ
19 1 18 mt4i ⊢ N ∈ ℕ → 0 − N ∉ ℕ 0