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