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

Metamath Proof Explorer

Theorem nn0p1elfzo

Description: A nonnegative integer increased by 1 which is less than or equal to another integer is an element of a half-open range of integers. (Contributed by AV, 27-Feb-2021)

Ref Expression
Assertion nn0p1elfzo ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nn0ltp1le ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 < 𝑁 ↔ ( 𝐾 + 1 ) ≤ 𝑁 ) )
2 1 biimp3ar ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 < 𝑁 )
3 simpl1 ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℕ0 )
4 simpr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5 4 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ0 )
6 nn0ge0 ⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
7 6 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝐾 )
8 0re ⊢ 0 ∈ ℝ
9 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
10 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
11 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 ) )
12 8 9 10 11 mp3an3an ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 ) )
13 7 12 mpand ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 < 𝑁 → 0 < 𝑁 ) )
14 13 imp ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 0 < 𝑁 )
15 elnnnn0b ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 0 < 𝑁 ) )
16 5 14 15 sylanbrc ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ )
17 16 3adantl3 ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝑁 ∈ ℕ )
18 simpr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → 𝐾 < 𝑁 )
19 3 17 18 3jca ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) ∧ 𝐾 < 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
20 2 19 mpdan ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
21 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁 ) )
22 20 21 sylibr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )