fz0fzelfz0

Description: If a member of a finite set of sequential integers with a lower bound being a member of a finite set of sequential nonnegative integers with the same upper bound, this member is also a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 21-Apr-2018)

		Ref	Expression
	Assertion	fz0fzelfz0	$⊢ (N \in (0 \dots R) \land M \in (N \dots R)) \to M \in (0 \dots R)$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ N \in (0 \dots R) \leftrightarrow (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R)$
2		elfz2	$⊢ M \in (N \dots R) \leftrightarrow ((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R))$
3		simplr	$⊢ ((N \in ℕ_{0} \land M \in ℤ) \land N \leq M) \to M \in ℤ$
4		0red	$⊢ (N \in ℕ_{0} \land M \in ℤ) \to 0 \in ℝ$
5		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
6	5	adantr	$⊢ (N \in ℕ_{0} \land M \in ℤ) \to N \in ℝ$
7		zre	$⊢ M \in ℤ \to M \in ℝ$
8	7	adantl	$⊢ (N \in ℕ_{0} \land M \in ℤ) \to M \in ℝ$
9	4 6 8	3jca	$⊢ (N \in ℕ_{0} \land M \in ℤ) \to (0 \in ℝ \land N \in ℝ \land M \in ℝ)$
10	9	adantr	$⊢ ((N \in ℕ_{0} \land M \in ℤ) \land N \leq M) \to (0 \in ℝ \land N \in ℝ \land M \in ℝ)$
11		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
12	11	adantr	$⊢ (N \in ℕ_{0} \land M \in ℤ) \to 0 \leq N$
13	12	anim1i	$⊢ ((N \in ℕ_{0} \land M \in ℤ) \land N \leq M) \to (0 \leq N \land N \leq M)$
14		letr	$⊢ (0 \in ℝ \land N \in ℝ \land M \in ℝ) \to ((0 \leq N \land N \leq M) \to 0 \leq M)$
15	10 13 14	sylc	$⊢ ((N \in ℕ_{0} \land M \in ℤ) \land N \leq M) \to 0 \leq M$
16		elnn0z	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℤ \land 0 \leq M)$
17	3 15 16	sylanbrc	$⊢ ((N \in ℕ_{0} \land M \in ℤ) \land N \leq M) \to M \in ℕ_{0}$
18	17	exp31	$⊢ N \in ℕ_{0} \to (M \in ℤ \to (N \leq M \to M \in ℕ_{0}))$
19	18	com23	$⊢ N \in ℕ_{0} \to (N \leq M \to (M \in ℤ \to M \in ℕ_{0}))$
20	19	3ad2ant1	$⊢ (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to (N \leq M \to (M \in ℤ \to M \in ℕ_{0}))$
21	20	com13	$⊢ M \in ℤ \to (N \leq M \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to M \in ℕ_{0}))$
22	21	adantrd	$⊢ M \in ℤ \to ((N \leq M \land M \leq R) \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to M \in ℕ_{0}))$
23	22	3ad2ant3	$⊢ (N \in ℤ \land R \in ℤ \land M \in ℤ) \to ((N \leq M \land M \leq R) \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to M \in ℕ_{0}))$
24	23	imp	$⊢ ((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to M \in ℕ_{0})$
25	24	imp	$⊢ (((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \land (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R)) \to M \in ℕ_{0}$
26		simpr2	$⊢ (((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \land (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R)) \to R \in ℕ_{0}$
27		simplrr	$⊢ (((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \land (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R)) \to M \leq R$
28	25 26 27	3jca	$⊢ (((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \land (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R)) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R)$
29	28	ex	$⊢ ((N \in ℤ \land R \in ℤ \land M \in ℤ) \land (N \leq M \land M \leq R)) \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R))$
30	2 29	sylbi	$⊢ M \in (N \dots R) \to ((N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R))$
31	30	com12	$⊢ (N \in ℕ_{0} \land R \in ℕ_{0} \land N \leq R) \to (M \in (N \dots R) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R))$
32	1 31	sylbi	$⊢ N \in (0 \dots R) \to (M \in (N \dots R) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R))$
33	32	imp	$⊢ (N \in (0 \dots R) \land M \in (N \dots R)) \to (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R)$
34		elfz2nn0	$⊢ M \in (0 \dots R) \leftrightarrow (M \in ℕ_{0} \land R \in ℕ_{0} \land M \leq R)$
35	33 34	sylibr	$⊢ (N \in (0 \dots R) \land M \in (N \dots R)) \to M \in (0 \dots R)$

Metamath Proof Explorer

Theorem fz0fzelfz0

Proof