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 
|- ( 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 )