This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzp1

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

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

Proof

Step Hyp Ref Expression
1 uzm1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
2 eluzp1p1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
3 eluzelcn 
 |-  ( N e. ( ZZ>= ` M ) -> N e. CC )
4 ax-1cn 
 |-  1 e. CC
5 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
6 3 4 5 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) = N )
7 6 eleq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) <-> N e. ( ZZ>= ` ( M + 1 ) ) ) )
8 2 7 imbitrid 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` ( M + 1 ) ) ) )
9 8 orim2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) ) )
10 1 9 mpd 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )