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	$⊢ K \in (0 ..^N) \to N - K - 1 \in (0 ..^N)$

Proof

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

Metamath Proof Explorer

Theorem ubmelm1fzo

Proof