This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ... 𝑁 ) )