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)

Step	Hyp	Ref	Expression
1		nn0difffzod.1	$⊢ φ \to N \in ℤ$
2		nn0difffzod.2	$⊢ φ \to M \in (ℕ_{0} ∖ (0 ..^N))$
3	2	eldifbd	$⊢ φ \to \neg M \in (0 ..^N)$
4	2	eldifad	$⊢ φ \to M \in ℕ_{0}$
5		elfzo0z	$⊢ M \in (0 ..^N) \leftrightarrow (M \in ℕ_{0} \land N \in ℤ \land M < N)$
6	5	biimpri	$⊢ (M \in ℕ_{0} \land N \in ℤ \land M < N) \to M \in (0 ..^N)$
7	6	3expa	$⊢ ((M \in ℕ_{0} \land N \in ℤ) \land M < N) \to M \in (0 ..^N)$
8	7	con3i	$⊢ \neg M \in (0 ..^N) \to \neg ((M \in ℕ_{0} \land N \in ℤ) \land M < N)$
9		imnan	$⊢ ((M \in ℕ_{0} \land N \in ℤ) \to \neg M < N) \leftrightarrow \neg ((M \in ℕ_{0} \land N \in ℤ) \land M < N)$
10	8 9	sylibr	$⊢ \neg M \in (0 ..^N) \to ((M \in ℕ_{0} \land N \in ℤ) \to \neg M < N)$
11	10	imp	$⊢ (\neg M \in (0 ..^N) \land (M \in ℕ_{0} \land N \in ℤ)) \to \neg M < N$
12	3 4 1 11	syl12anc	$⊢ φ \to \neg M < N$

Metamath Proof Explorer