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