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 ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑁 = 𝑀 → ( 𝑁 ... 𝑁 ) = ( 𝑀 ... 𝑁 ) )
2 1 eleq2d ⊢ ( 𝑁 = 𝑀 → ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) ↔ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
3 elfz1eq ⊢ ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 )
4 2 3 biimtrrdi ⊢ ( 𝑁 = 𝑀 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 = 𝑁 ) )
5 olc ⊢ ( 𝐾 = 𝑁 → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) )
6 4 5 syl6 ⊢ ( 𝑁 = 𝑀 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
7 6 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
8 noel ⊢ ¬ 𝐾 ∈ ∅
9 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
10 9 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → 𝑁 ∈ ℤ )
11 10 zred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → 𝑁 ∈ ℝ )
12 11 ltm1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝑁 − 1 ) < 𝑁 )
13 breq2 ⊢ ( 𝑁 = 𝑀 → ( ( 𝑁 − 1 ) < 𝑁 ↔ ( 𝑁 − 1 ) < 𝑀 ) )
14 13 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( ( 𝑁 − 1 ) < 𝑁 ↔ ( 𝑁 − 1 ) < 𝑀 ) )
15 12 14 mpbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝑁 − 1 ) < 𝑀 )
16 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
17 1zzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → 1 ∈ ℤ )
18 10 17 zsubcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
19 fzn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ ) )
20 16 18 19 syl2an2r ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( ( 𝑁 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ ) )
21 15 20 mpbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝑀 ... ( 𝑁 − 1 ) ) = ∅ )
22 21 eleq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝐾 ∈ ∅ ) )
23 8 22 mtbiri ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ¬ 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
24 23 pm2.21d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
25 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
26 25 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
27 eleq1 ⊢ ( 𝐾 = 𝑁 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
28 27 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) ∧ 𝐾 = 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑁 ∈ ( 𝑀 ... 𝑁 ) ) )
29 26 28 mpbird ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) ∧ 𝐾 = 𝑁 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
30 29 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝐾 = 𝑁 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
31 24 30 jaod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
32 7 31 impbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 = 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
33 elfzp1 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = ( ( 𝑁 − 1 ) + 1 ) ) ) )
34 33 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐾 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = ( ( 𝑁 − 1 ) + 1 ) ) ) )
35 9 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
36 35 zcnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℂ )
37 npcan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
38 36 37 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
39 38 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝑀 ... 𝑁 ) )
40 39 eleq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐾 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) + 1 ) ) ↔ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) )
41 38 eqeq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐾 = ( ( 𝑁 − 1 ) + 1 ) ↔ 𝐾 = 𝑁 ) )
42 41 orbi2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = ( ( 𝑁 − 1 ) + 1 ) ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
43 34 40 42 3bitr3d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )
44 uzm1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
45 32 43 44 mpjaodan ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝐾 = 𝑁 ) ) )