Metamath Proof Explorer

Theorem uzm1

Description: Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion uzm1 
|- ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2 1 a1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> M e. ZZ ) )
3 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
4 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
5 3 4 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - 1 ) e. ZZ )
6 5 a1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> ( N - 1 ) e. ZZ ) )
7 df-ne 
 |-  ( N =/= M <-> -. N = M )
8 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
9 1 zred 
 |-  ( N e. ( ZZ>= ` M ) -> M e. RR )
10 eluzelre 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
11 9 10 ltlend 
 |-  ( N e. ( ZZ>= ` M ) -> ( M < N <-> ( M <_ N /\ N =/= M ) ) )
12 11 biimprd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M <_ N /\ N =/= M ) -> M < N ) )
13 8 12 mpand 
 |-  ( N e. ( ZZ>= ` M ) -> ( N =/= M -> M < N ) )
14 7 13 syl5bir 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> M < N ) )
15 zltlem1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> M <_ ( N - 1 ) ) )
16 1 3 15 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M < N <-> M <_ ( N - 1 ) ) )
17 14 16 sylibd 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> M <_ ( N - 1 ) ) )
18 2 6 17 3jcad 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ M <_ ( N - 1 ) ) ) )
19 eluz2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ M <_ ( N - 1 ) ) )
20 18 19 syl6ibr 
 |-  ( N e. ( ZZ>= ` M ) -> ( -. N = M -> ( N - 1 ) e. ( ZZ>= ` M ) ) )
21 20 orrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )