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

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 ..^ 𝑁 ) )