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 ⊢ φ → N ∈ ℤ
nn0difffzod.2 ⊢ φ → M ∈ ℕ 0 ∖ 0 ..^ N
Assertion nn0difffzod ⊢ φ → ¬ M < N

Proof

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