Metamath Proof Explorer

Theorem fzonnsub

Description: If K < N then N - K is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015) (Revised by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion fzonnsub ⊢ K ∈ M ..^ N → N − K ∈ ℕ

Proof

Step Hyp Ref Expression
1 elfzolt2 ⊢ K ∈ M ..^ N → K < N
2 elfzoelz ⊢ K ∈ M ..^ N → K ∈ ℤ
3 elfzoel2 ⊢ K ∈ M ..^ N → N ∈ ℤ
4 znnsub ⊢ K ∈ ℤ ∧ N ∈ ℤ → K < N ↔ N − K ∈ ℕ
5 2 3 4 syl2anc ⊢ K ∈ M ..^ N → K < N ↔ N − K ∈ ℕ
6 1 5 mpbid ⊢ K ∈ M ..^ N → N − K ∈ ℕ