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	|- ( ph -> N e. ZZ )
	nn0difffzod.2	|- ( ph -> M e. ( NN0 \ ( 0 ..^ N ) ) )
Assertion	nn0difffzod	|- ( ph -> -. M < N )

Proof

Step	Hyp	Ref	Expression
1		nn0difffzod.1	|- ( ph -> N e. ZZ )
2		nn0difffzod.2	|- ( ph -> M e. ( NN0 \ ( 0 ..^ N ) ) )
3	2	eldifbd	|- ( ph -> -. M e. ( 0 ..^ N ) )
4	2	eldifad	|- ( ph -> M e. NN0 )
5		elfzo0z	|- ( M e. ( 0 ..^ N ) <-> ( M e. NN0 /\ N e. ZZ /\ M < N ) )
6	5	biimpri	|- ( ( M e. NN0 /\ N e. ZZ /\ M < N ) -> M e. ( 0 ..^ N ) )
7	6	3expa	|- ( ( ( M e. NN0 /\ N e. ZZ ) /\ M < N ) -> M e. ( 0 ..^ N ) )
8	7	con3i	|- ( -. M e. ( 0 ..^ N ) -> -. ( ( M e. NN0 /\ N e. ZZ ) /\ M < N ) )
9		imnan	|- ( ( ( M e. NN0 /\ N e. ZZ ) -> -. M < N ) <-> -. ( ( M e. NN0 /\ N e. ZZ ) /\ M < N ) )
10	8 9	sylibr	|- ( -. M e. ( 0 ..^ N ) -> ( ( M e. NN0 /\ N e. ZZ ) -> -. M < N ) )
11	10	imp	|- ( ( -. M e. ( 0 ..^ N ) /\ ( M e. NN0 /\ N e. ZZ ) ) -> -. M < N )
12	3 4 1 11	syl12anc	|- ( ph -> -. M < N )