nn0p1elfzo

Description: A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021)

		Ref	Expression
	Assertion	nn0p1elfzo	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \to K \in (0 ..^N)$

Proof

Step	Hyp	Ref	Expression
1		nn0ltp1le	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (K < N \leftrightarrow K + 1 \leq N)$
2	1	biimp3ar	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \to K < N$
3		simpl1	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \land K < N) \to K \in ℕ_{0}$
4		simpr	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to N \in ℕ_{0}$
5	4	adantr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0}) \land K < N) \to N \in ℕ_{0}$
6		nn0ge0	$⊢ K \in ℕ_{0} \to 0 \leq K$
7	6	adantr	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to 0 \leq K$
8		0re	$⊢ 0 \in ℝ$
9		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
10		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
11		lelttr	$⊢ (0 \in ℝ \land K \in ℝ \land N \in ℝ) \to ((0 \leq K \land K < N) \to 0 < N)$
12	8 9 10 11	mp3an3an	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to ((0 \leq K \land K < N) \to 0 < N)$
13	7 12	mpand	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (K < N \to 0 < N)$
14	13	imp	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0}) \land K < N) \to 0 < N$
15		elnnnn0b	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land 0 < N)$
16	5 14 15	sylanbrc	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0}) \land K < N) \to N \in ℕ$
17	16	3adantl3	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \land K < N) \to N \in ℕ$
18		simpr	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \land K < N) \to K < N$
19	3 17 18	3jca	$⊢ ((K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \land K < N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
20	2 19	mpdan	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \to (K \in ℕ_{0} \land N \in ℕ \land K < N)$
21		elfzo0	$⊢ K \in (0 ..^N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ \land K < N)$
22	20 21	sylibr	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K + 1 \leq N) \to K \in (0 ..^N)$

Metamath Proof Explorer

Theorem nn0p1elfzo

Proof