Metamath Proof Explorer


Theorem ubmelm1fzo

Description: The result of subtracting 1 and an integer of a half-open range of nonnegative integers from the upper bound of this range is contained in this range. (Contributed by AV, 23-Mar-2018) (Revised by AV, 30-Oct-2018)

Ref Expression
Assertion ubmelm1fzo ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfzo0 ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
2 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3 2 adantr ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
4 nn0z ( 𝐾 ∈ ℕ0𝐾 ∈ ℤ )
5 4 adantl ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℤ )
6 3 5 zsubcld ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁𝐾 ) ∈ ℤ )
7 6 ancoms ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( 𝑁𝐾 ) ∈ ℤ )
8 peano2zm ( ( 𝑁𝐾 ) ∈ ℤ → ( ( 𝑁𝐾 ) − 1 ) ∈ ℤ )
9 7 8 syl ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ℤ )
10 9 3adant3 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ℤ )
11 simp3 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
12 4 2 anim12i ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
13 12 3adant3 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
14 znnsub ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ( 𝑁𝐾 ) ∈ ℕ ) )
15 13 14 syl ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝐾 < 𝑁 ↔ ( 𝑁𝐾 ) ∈ ℕ ) )
16 11 15 mpbid ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( 𝑁𝐾 ) ∈ ℕ )
17 nnm1ge0 ( ( 𝑁𝐾 ) ∈ ℕ → 0 ≤ ( ( 𝑁𝐾 ) − 1 ) )
18 16 17 syl ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 0 ≤ ( ( 𝑁𝐾 ) − 1 ) )
19 elnn0z ( ( ( 𝑁𝐾 ) − 1 ) ∈ ℕ0 ↔ ( ( ( 𝑁𝐾 ) − 1 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑁𝐾 ) − 1 ) ) )
20 10 18 19 sylanbrc ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ℕ0 )
21 simp2 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ )
22 nncn ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
23 22 adantl ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
24 nn0cn ( 𝐾 ∈ ℕ0𝐾 ∈ ℂ )
25 24 adantr ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → 𝐾 ∈ ℂ )
26 1cnd ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → 1 ∈ ℂ )
27 23 25 26 subsub4d ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( ( 𝑁𝐾 ) − 1 ) = ( 𝑁 − ( 𝐾 + 1 ) ) )
28 nn0p1gt0 ( 𝐾 ∈ ℕ0 → 0 < ( 𝐾 + 1 ) )
29 28 adantr ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → 0 < ( 𝐾 + 1 ) )
30 nn0re ( 𝐾 ∈ ℕ0𝐾 ∈ ℝ )
31 peano2re ( 𝐾 ∈ ℝ → ( 𝐾 + 1 ) ∈ ℝ )
32 30 31 syl ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℝ )
33 nnre ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
34 ltsubpos ( ( ( 𝐾 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < ( 𝐾 + 1 ) ↔ ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 ) )
35 32 33 34 syl2an ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( 0 < ( 𝐾 + 1 ) ↔ ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 ) )
36 29 35 mpbid ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( 𝑁 − ( 𝐾 + 1 ) ) < 𝑁 )
37 27 36 eqbrtrd ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ) → ( ( 𝑁𝐾 ) − 1 ) < 𝑁 )
38 37 3adant3 ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) < 𝑁 )
39 elfzo0 ( ( ( 𝑁𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( ( 𝑁𝐾 ) − 1 ) ∈ ℕ0𝑁 ∈ ℕ ∧ ( ( 𝑁𝐾 ) − 1 ) < 𝑁 ) )
40 20 21 38 39 syl3anbrc ( ( 𝐾 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )
41 1 40 sylbi ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝑁𝐾 ) − 1 ) ∈ ( 0 ..^ 𝑁 ) )