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

Metamath Proof Explorer

Theorem subne0nn

Description: A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023)

Ref Expression
Hypotheses subne0nn.1 ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
subne0nn.2 ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
subne0nn.3 ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ0 )
subne0nn.4 ⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
Assertion subne0nn ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 subne0nn.1 ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
2 subne0nn.2 ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
3 subne0nn.3 ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ0 )
4 subne0nn.4 ⊢ ( 𝜑 → 𝑀 ≠ 𝑁 )
5 1 2 4 subne0d ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ≠ 0 )
6 elnnne0 ⊢ ( ( 𝑀 − 𝑁 ) ∈ ℕ ↔ ( ( 𝑀 − 𝑁 ) ∈ ℕ0 ∧ ( 𝑀 − 𝑁 ) ≠ 0 ) )
7 3 5 6 sylanbrc ⊢ ( 𝜑 → ( 𝑀 − 𝑁 ) ∈ ℕ )