Metamath Proof Explorer

Theorem fzm1

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

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( N = M -> ( N ... N ) = ( M ... N ) )
2 1 eleq2d 
 |-  ( N = M -> ( K e. ( N ... N ) <-> K e. ( M ... N ) ) )
3 elfz1eq 
 |-  ( K e. ( N ... N ) -> K = N )
4 2 3 syl6bir 
 |-  ( N = M -> ( K e. ( M ... N ) -> K = N ) )
5 olc 
 |-  ( K = N -> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) )
6 4 5 syl6 
 |-  ( N = M -> ( K e. ( M ... N ) -> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )
7 6 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( K e. ( M ... N ) -> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )
8 noel 
 |-  -. K e. (/)
9 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10 9 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> N e. ZZ )
11 10 zred 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> N e. RR )
12 11 ltm1d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( N - 1 ) < N )
13 breq2 
 |-  ( N = M -> ( ( N - 1 ) < N <-> ( N - 1 ) < M ) )
14 13 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( ( N - 1 ) < N <-> ( N - 1 ) < M ) )
15 12 14 mpbid 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( N - 1 ) < M )
16 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
17 1zzd 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> 1 e. ZZ )
18 10 17 zsubcld 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( N - 1 ) e. ZZ )
19 fzn 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( ( N - 1 ) < M <-> ( M ... ( N - 1 ) ) = (/) ) )
20 16 18 19 syl2an2r 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( ( N - 1 ) < M <-> ( M ... ( N - 1 ) ) = (/) ) )
21 15 20 mpbid 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( M ... ( N - 1 ) ) = (/) )
22 21 eleq2d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( K e. ( M ... ( N - 1 ) ) <-> K e. (/) ) )
23 8 22 mtbiri 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> -. K e. ( M ... ( N - 1 ) ) )
24 23 pm2.21d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( K e. ( M ... ( N - 1 ) ) -> K e. ( M ... N ) ) )
25 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
26 25 ad2antrr 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ N = M ) /\ K = N ) -> N e. ( M ... N ) )
27 eleq1 
 |-  ( K = N -> ( K e. ( M ... N ) <-> N e. ( M ... N ) ) )
28 27 adantl 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ N = M ) /\ K = N ) -> ( K e. ( M ... N ) <-> N e. ( M ... N ) ) )
29 26 28 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` M ) /\ N = M ) /\ K = N ) -> K e. ( M ... N ) )
30 29 ex 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( K = N -> K e. ( M ... N ) ) )
31 24 30 jaod 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( ( K e. ( M ... ( N - 1 ) ) \/ K = N ) -> K e. ( M ... N ) ) )
32 7 31 impbid 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> ( K e. ( M ... N ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )
33 elfzp1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( K e. ( M ... ( ( N - 1 ) + 1 ) ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = ( ( N - 1 ) + 1 ) ) ) )
34 33 adantl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( K e. ( M ... ( ( N - 1 ) + 1 ) ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = ( ( N - 1 ) + 1 ) ) ) )
35 9 adantr 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> N e. ZZ )
36 35 zcnd 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> N e. CC )
37 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
38 36 37 syl 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( N - 1 ) + 1 ) = N )
39 38 oveq2d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
40 39 eleq2d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( K e. ( M ... ( ( N - 1 ) + 1 ) ) <-> K e. ( M ... N ) ) )
41 38 eqeq2d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( K = ( ( N - 1 ) + 1 ) <-> K = N ) )
42 41 orbi2d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( K e. ( M ... ( N - 1 ) ) \/ K = ( ( N - 1 ) + 1 ) ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )
43 34 40 42 3bitr3d 
 |-  ( ( N e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( K e. ( M ... N ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )
44 uzm1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
45 32 43 44 mpjaodan 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K e. ( M ... ( N - 1 ) ) \/ K = N ) ) )