elfz0ubfz0

Description: An element of a finite set of sequential nonnegative integers is an element of a finite set of sequential nonnegative integers with the upper bound being an element of the finite set of sequential nonnegative integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018)

		Ref	Expression
	Assertion	elfz0ubfz0	$⊢ (K \in (0 \dots N) \land L \in (K \dots N)) \to K \in (0 \dots L)$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$
2		elfz2	$⊢ L \in (K \dots N) \leftrightarrow ((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N))$
3		simpr1	$⊢ (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \land (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)) \to K \in ℕ_{0}$
4		elnn0z	$⊢ K \in ℕ_{0} \leftrightarrow (K \in ℤ \land 0 \leq K)$
5		simpr	$⊢ (K \in ℤ \land L \in ℤ) \to L \in ℤ$
6		0z	$⊢ 0 \in ℤ$
7		zletr	$⊢ (0 \in ℤ \land K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to 0 \leq L)$
8	6 7	mp3an1	$⊢ (K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to 0 \leq L)$
9		elnn0z	$⊢ L \in ℕ_{0} \leftrightarrow (L \in ℤ \land 0 \leq L)$
10	9	simplbi2	$⊢ L \in ℤ \to (0 \leq L \to L \in ℕ_{0})$
11	5 8 10	sylsyld	$⊢ (K \in ℤ \land L \in ℤ) \to ((0 \leq K \land K \leq L) \to L \in ℕ_{0})$
12	11	expd	$⊢ (K \in ℤ \land L \in ℤ) \to (0 \leq K \to (K \leq L \to L \in ℕ_{0}))$
13	12	impancom	$⊢ (K \in ℤ \land 0 \leq K) \to (L \in ℤ \to (K \leq L \to L \in ℕ_{0}))$
14	4 13	sylbi	$⊢ K \in ℕ_{0} \to (L \in ℤ \to (K \leq L \to L \in ℕ_{0}))$
15	14	com13	$⊢ K \leq L \to (L \in ℤ \to (K \in ℕ_{0} \to L \in ℕ_{0}))$
16	15	adantr	$⊢ (K \leq L \land L \leq N) \to (L \in ℤ \to (K \in ℕ_{0} \to L \in ℕ_{0}))$
17	16	com12	$⊢ L \in ℤ \to ((K \leq L \land L \leq N) \to (K \in ℕ_{0} \to L \in ℕ_{0}))$
18	17	3ad2ant3	$⊢ (K \in ℤ \land N \in ℤ \land L \in ℤ) \to ((K \leq L \land L \leq N) \to (K \in ℕ_{0} \to L \in ℕ_{0}))$
19	18	imp	$⊢ ((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \to (K \in ℕ_{0} \to L \in ℕ_{0})$
20	19	com12	$⊢ K \in ℕ_{0} \to (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \to L \in ℕ_{0})$
21	20	3ad2ant1	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \to (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \to L \in ℕ_{0})$
22	21	impcom	$⊢ (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \land (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)) \to L \in ℕ_{0}$
23		simplrl	$⊢ (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \land (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)) \to K \leq L$
24	3 22 23	3jca	$⊢ (((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \land (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L)$
25	24	ex	$⊢ ((K \in ℤ \land N \in ℤ \land L \in ℤ) \land (K \leq L \land L \leq N)) \to ((K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L))$
26	2 25	sylbi	$⊢ L \in (K \dots N) \to ((K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L))$
27	26	com12	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \to (L \in (K \dots N) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L))$
28	1 27	sylbi	$⊢ K \in (0 \dots N) \to (L \in (K \dots N) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L))$
29	28	imp	$⊢ (K \in (0 \dots N) \land L \in (K \dots N)) \to (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L)$
30		elfz2nn0	$⊢ K \in (0 \dots L) \leftrightarrow (K \in ℕ_{0} \land L \in ℕ_{0} \land K \leq L)$
31	29 30	sylibr	$⊢ (K \in (0 \dots N) \land L \in (K \dots N)) \to K \in (0 \dots L)$

Metamath Proof Explorer

Theorem elfz0ubfz0

Proof