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 ( 𝑁 ∈ ℕ → ( 0 − 𝑁 ) ∉ ℕ0 )

Proof

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