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 )