Theorem 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	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
2		elfz2	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) ↔ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) )
3		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
4		nn0re	⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
5		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6	3 4 5	3anim123i	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
7	6	3expa	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
8		letr	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → 𝑀 ≤ 𝑁 ) )
9	7 8	syl	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → 𝑀 ≤ 𝑁 ) )
10		simplll	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
11		simpr	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
12	11	adantr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
13		elnn0z	⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) )
14		0red	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 0 ∈ ℝ )
15		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
16	15	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
17	5	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
18		letr	⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) → 0 ≤ 𝑁 ) )
19	14 16 17 18	syl3anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) → 0 ≤ 𝑁 ) )
20	19	exp4b	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑀 → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) ) ) )
21	20	com23	⊢ ( 𝑀 ∈ ℤ → ( 0 ≤ 𝑀 → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) ) ) )
22	21	imp	⊢ ( ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) ) )
23	13 22	sylbi	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) ) )
24	23	adantr	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) ) )
25	24	imp	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 → 0 ≤ 𝑁 ) )
26	25	imp	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 0 ≤ 𝑁 )
27		elnn0z	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
28	12 26 27	sylanbrc	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℕ0 )
29		simpr	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ≤ 𝑁 )
30	10 28 29	3jca	⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
31	30	ex	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
32	9 31	syld	⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
33	32	exp4b	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ℤ → ( 𝑀 ≤ 𝐿 → ( 𝐿 ≤ 𝑁 → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) ) )
34	33	com23	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 ≤ 𝐿 → ( 𝑁 ∈ ℤ → ( 𝐿 ≤ 𝑁 → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) ) )
35	34	3impia	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ℤ → ( 𝐿 ≤ 𝑁 → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) )
36	35	com13	⊢ ( 𝐿 ≤ 𝑁 → ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) )
37	36	adantr	⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) → ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) )
38	37	com12	⊢ ( 𝑁 ∈ ℤ → ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) )
39	38	3ad2ant3	⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) ) )
40	39	imp	⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
41	2 40	sylbi	⊢ ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
42	41	com12	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
43	1 42	sylbi	⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... 𝑋 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ) )
44	43	imp	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
45		elfz2nn0	⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
46	44 45	sylibr	⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... 𝑋 ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )