Theorem ubmelfzo

Description: If an integer in a 1-based finite set of sequential integers is subtracted from the upper bound of this finite set of sequential integers, the result is contained in a half-open range of nonnegative integers with the same upper bound. (Contributed by AV, 18-Mar-2018) (Revised by AV, 30-Oct-2018)

	Ref	Expression
Assertion	ubmelfzo	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → 𝐾 ≤ 𝑁 )
2		nnnn0	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
3		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4	2 3	anim12i	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
5	4	3adant3	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
6		nn0sub	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ0 ) )
7	5 6	syl	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 ≤ 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ0 ) )
8	1 7	mpbid	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
9		simp2	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → 𝑁 ∈ ℕ )
10		nngt0	⊢ ( 𝐾 ∈ ℕ → 0 < 𝐾 )
11	10	3ad2ant1	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → 0 < 𝐾 )
12		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
13		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14	12 13	anim12i	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
15	14	3adant3	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
16		ltsubpos	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 < 𝐾 ↔ ( 𝑁 − 𝐾 ) < 𝑁 ) )
17	15 16	syl	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 0 < 𝐾 ↔ ( 𝑁 − 𝐾 ) < 𝑁 ) )
18	11 17	mpbid	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( 𝑁 − 𝐾 ) < 𝑁 )
19	8 9 18	3jca	⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 − 𝐾 ) < 𝑁 ) )
20		elfz1b	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) )
21		elfzo0	⊢ ( ( 𝑁 − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) ↔ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ( 𝑁 − 𝐾 ) < 𝑁 ) )
22	19 20 21	3imtr4i	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ( 0 ..^ 𝑁 ) )