Metamath Proof Explorer

Theorem elfz0ubfz0

Description: An element of a finite set of sequential nonnegative integers is an element of a finite set of sequential nonnegative integers with the upper bound being an element of the finite set of sequential nonnegative integers with the same lower bound as for the first interval and the element under consideration as upper bound. (Contributed by Alexander van der Vekens, 3-Apr-2018)

Ref Expression
Assertion elfz0ubfz0 ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐾 ∈ ( 0 ... 𝐿 ) )

Proof

Step Hyp Ref Expression
1 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )
2 elfz2 ⊢ ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) )
3 simpr1 ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝐾 ∈ ℕ0 )
4 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
5 simpr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℤ )
6 0z ⊢ 0 ∈ ℤ
7 zletr ⊢ ( ( 0 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 0 ≤ 𝐿 ) )
8 6 7 mp3an1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 0 ≤ 𝐿 ) )
9 elnn0z ⊢ ( 𝐿 ∈ ℕ0 ↔ ( 𝐿 ∈ ℤ ∧ 0 ≤ 𝐿 ) )
10 9 simplbi2 ⊢ ( 𝐿 ∈ ℤ → ( 0 ≤ 𝐿 → 𝐿 ∈ ℕ0 ) )
11 5 8 10 sylsyld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 𝐿 ∈ ℕ0 ) )
12 11 expd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝐾 ≤ 𝐿 → 𝐿 ∈ ℕ0 ) ) )
13 12 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) → ( 𝐿 ∈ ℤ → ( 𝐾 ≤ 𝐿 → 𝐿 ∈ ℕ0 ) ) )
14 4 13 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( 𝐾 ≤ 𝐿 → 𝐿 ∈ ℕ0 ) ) )
15 14 com13 ⊢ ( 𝐾 ≤ 𝐿 → ( 𝐿 ∈ ℤ → ( 𝐾 ∈ ℕ0 → 𝐿 ∈ ℕ0 ) ) )
16 15 adantr ⊢ ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝐿 ∈ ℤ → ( 𝐾 ∈ ℕ0 → 𝐿 ∈ ℕ0 ) ) )
17 16 com12 ⊢ ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 → 𝐿 ∈ ℕ0 ) ) )
18 17 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 → 𝐿 ∈ ℕ0 ) ) )
19 18 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝐾 ∈ ℕ0 → 𝐿 ∈ ℕ0 ) )
20 19 com12 ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) → 𝐿 ∈ ℕ0 ) )
21 20 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) → 𝐿 ∈ ℕ0 ) )
22 21 impcom ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝐿 ∈ ℕ0 )
23 simplrl ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → 𝐾 ≤ 𝐿 )
24 3 22 23 3jca ⊢ ( ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) ∧ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) )
25 24 ex ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) ) )
26 2 25 sylbi ⊢ ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) ) )
27 26 com12 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) ) )
28 1 27 sylbi ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐿 ∈ ( 𝐾 ... 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) ) )
29 28 imp ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) )
30 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝐿 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝐾 ≤ 𝐿 ) )
31 29 30 sylibr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝐿 ∈ ( 𝐾 ... 𝑁 ) ) → 𝐾 ∈ ( 0 ... 𝐿 ) )