Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... 𝑅 ) ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) )
2 elfz2 ⊢ ( 𝑀 ∈ ( 𝑁 ... 𝑅 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) )
3 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ≤ 𝑀 ) → 𝑀 ∈ ℤ )
4 0red ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → 0 ∈ ℝ )
5 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → 𝑁 ∈ ℝ )
7 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8 7 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℝ )
9 4 6 8 3jca ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ≤ 𝑀 ) → ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
11 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
12 11 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) → 0 ≤ 𝑁 )
13 12 anim1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ≤ 𝑀 ) → ( 0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) )
14 letr ⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀 ) → 0 ≤ 𝑀 ) )
15 10 13 14 sylc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ≤ 𝑀 ) → 0 ≤ 𝑀 )
16 elnn0z ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) )
17 3 15 16 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ≤ 𝑀 ) → 𝑀 ∈ ℕ0 )
18 17 exp31 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℤ → ( 𝑁 ≤ 𝑀 → 𝑀 ∈ ℕ0 ) ) )
19 18 com23 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 𝑀 → ( 𝑀 ∈ ℤ → 𝑀 ∈ ℕ0 ) ) )
20 19 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → ( 𝑁 ≤ 𝑀 → ( 𝑀 ∈ ℤ → 𝑀 ∈ ℕ0 ) ) )
21 20 com13 ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ≤ 𝑀 → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → 𝑀 ∈ ℕ0 ) ) )
22 21 adantrd ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → 𝑀 ∈ ℕ0 ) ) )
23 22 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → 𝑀 ∈ ℕ0 ) ) )
24 23 imp ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → 𝑀 ∈ ℕ0 ) )
25 24 imp ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) ) → 𝑀 ∈ ℕ0 )
26 simpr2 ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) ) → 𝑅 ∈ ℕ0 )
27 simplrr ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) ) → 𝑀 ≤ 𝑅 )
28 25 26 27 3jca ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) )
29 28 ex ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) ) )
30 2 29 sylbi ⊢ ( 𝑀 ∈ ( 𝑁 ... 𝑅 ) → ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) ) )
31 30 com12 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑁 ≤ 𝑅 ) → ( 𝑀 ∈ ( 𝑁 ... 𝑅 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) ) )
32 1 31 sylbi ⊢ ( 𝑁 ∈ ( 0 ... 𝑅 ) → ( 𝑀 ∈ ( 𝑁 ... 𝑅 ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) ) )
33 32 imp ⊢ ( ( 𝑁 ∈ ( 0 ... 𝑅 ) ∧ 𝑀 ∈ ( 𝑁 ... 𝑅 ) ) → ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) )
34 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑅 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0 ∧ 𝑀 ≤ 𝑅 ) )
35 33 34 sylibr ⊢ ( ( 𝑁 ∈ ( 0 ... 𝑅 ) ∧ 𝑀 ∈ ( 𝑁 ... 𝑅 ) ) → 𝑀 ∈ ( 0 ... 𝑅 ) )