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	⊢ ( 𝜑 → ¬ 𝑀 < 𝑁 )