Metamath Proof Explorer


Theorem fzonnsub2

Description: If M < N then N - M is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion fzonnsub2 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁𝑀 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 elfzolt3b ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
2 fzonnsub ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁𝑀 ) ∈ ℕ )
3 1 2 syl ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁𝑀 ) ∈ ℕ )