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

Metamath Proof Explorer

Theorem nn0difffzod

Description: A nonnegative integer that is not in the half-open range from 0 to N is at least N . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses nn0difffzod.1 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
nn0difffzod.2 ⊢ ( 𝜑 → 𝑀 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) )
Assertion nn0difffzod ( 𝜑 → ¬ 𝑀 < 𝑁 )

Proof

Step Hyp Ref Expression
1 nn0difffzod.1 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
2 nn0difffzod.2 ⊢ ( 𝜑 → 𝑀 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) )
3 2 eldifbd ⊢ ( 𝜑 → ¬ 𝑀 ∈ ( 0 ..^ 𝑁 ) )
4 2 eldifad ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 elfzo0z ⊢ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
6 5 biimpri ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ( 0 ..^ 𝑁 ) )
7 6 3expa ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 < 𝑁 ) → 𝑀 ∈ ( 0 ..^ 𝑁 ) )
8 7 con3i ⊢ ( ¬ 𝑀 ∈ ( 0 ..^ 𝑁 ) → ¬ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 < 𝑁 ) )
9 imnan ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ¬ 𝑀 < 𝑁 ) ↔ ¬ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 < 𝑁 ) )
10 8 9 sylibr ⊢ ( ¬ 𝑀 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ¬ 𝑀 < 𝑁 ) )
11 10 imp ⊢ ( ( ¬ 𝑀 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) ) → ¬ 𝑀 < 𝑁 )
12 3 4 1 11 syl12anc ⊢ ( 𝜑 → ¬ 𝑀 < 𝑁 )