elfz0fzfz0

Description: A member of a finite set of sequential nonnegative integers is a member of a finite set of sequential nonnegative integers with a member of a finite set of sequential nonnegative integers starting at the upper bound of the first interval. (Contributed by Alexander van der Vekens, 27-May-2018)

		Ref	Expression
	Assertion	elfz0fzfz0	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to M \in (0 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
2		elfz2	$⊢ N \in (L \dots X) \leftrightarrow ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X))$
3		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
4		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
5		zre	$⊢ N \in ℤ \to N \in ℝ$
6	3 4 5	3anim123i	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land N \in ℤ) \to (M \in ℝ \land L \in ℝ \land N \in ℝ)$
7	6	3expa	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to (M \in ℝ \land L \in ℝ \land N \in ℝ)$
8		letr	$⊢ (M \in ℝ \land L \in ℝ \land N \in ℝ) \to ((M \leq L \land L \leq N) \to M \leq N)$
9	7 8	syl	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to ((M \leq L \land L \leq N) \to M \leq N)$
10		simplll	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to M \in ℕ_{0}$
11		simpr	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to N \in ℤ$
12	11	adantr	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to N \in ℤ$
13		elnn0z	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℤ \land 0 \leq M)$
14		0red	$⊢ (M \in ℤ \land N \in ℤ) \to 0 \in ℝ$
15		zre	$⊢ M \in ℤ \to M \in ℝ$
16	15	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℝ$
17	5	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℝ$
18		letr	$⊢ (0 \in ℝ \land M \in ℝ \land N \in ℝ) \to ((0 \leq M \land M \leq N) \to 0 \leq N)$
19	14 16 17 18	syl3anc	$⊢ (M \in ℤ \land N \in ℤ) \to ((0 \leq M \land M \leq N) \to 0 \leq N)$
20	19	exp4b	$⊢ M \in ℤ \to (N \in ℤ \to (0 \leq M \to (M \leq N \to 0 \leq N)))$
21	20	com23	$⊢ M \in ℤ \to (0 \leq M \to (N \in ℤ \to (M \leq N \to 0 \leq N)))$
22	21	imp	$⊢ (M \in ℤ \land 0 \leq M) \to (N \in ℤ \to (M \leq N \to 0 \leq N))$
23	13 22	sylbi	$⊢ M \in ℕ_{0} \to (N \in ℤ \to (M \leq N \to 0 \leq N))$
24	23	adantr	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (N \in ℤ \to (M \leq N \to 0 \leq N))$
25	24	imp	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to (M \leq N \to 0 \leq N)$
26	25	imp	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to 0 \leq N$
27		elnn0z	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℤ \land 0 \leq N)$
28	12 26 27	sylanbrc	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to N \in ℕ_{0}$
29		simpr	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to M \leq N$
30	10 28 29	3jca	$⊢ (((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \land M \leq N) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
31	30	ex	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to (M \leq N \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
32	9 31	syld	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land N \in ℤ) \to ((M \leq L \land L \leq N) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
33	32	exp4b	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (N \in ℤ \to (M \leq L \to (L \leq N \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))))$
34	33	com23	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (M \leq L \to (N \in ℤ \to (L \leq N \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))))$
35	34	3impia	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in ℤ \to (L \leq N \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)))$
36	35	com13	$⊢ L \leq N \to (N \in ℤ \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)))$
37	36	adantr	$⊢ (L \leq N \land N \leq X) \to (N \in ℤ \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)))$
38	37	com12	$⊢ N \in ℤ \to ((L \leq N \land N \leq X) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)))$
39	38	3ad2ant3	$⊢ (L \in ℤ \land X \in ℤ \land N \in ℤ) \to ((L \leq N \land N \leq X) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)))$
40	39	imp	$⊢ ((L \in ℤ \land X \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq X)) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
41	2 40	sylbi	$⊢ N \in (L \dots X) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
42	41	com12	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in (L \dots X) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
43	1 42	sylbi	$⊢ M \in (0 \dots L) \to (N \in (L \dots X) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N))$
44	43	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
45		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
46	44 45	sylibr	$⊢ (M \in (0 \dots L) \land N \in (L \dots X)) \to M \in (0 \dots N)$

Metamath Proof Explorer

Theorem elfz0fzfz0

Proof