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 syl6bir ( 𝑁 = 𝑀 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 = 𝑁 ) )
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 ) ) ∨ 𝐾 = 𝑁 ) ) )