Theorem fzofzim

Description: If a nonnegative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open integer range. (Contributed by Alexander van der Vekens, 15-Jun-2018)

	Ref	Expression
Assertion	fzofzim	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → 𝐾 ∈ ( 0 ..^ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑀 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) )
2		simpl1	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 ∈ ℕ0 )
3		necom	⊢ ( 𝐾 ≠ 𝑀 ↔ 𝑀 ≠ 𝐾 )
4		nn0re	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
5		nn0re	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
6		ltlen	⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐾 < 𝑀 ↔ ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ) )
7	4 5 6	syl2an	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 < 𝑀 ↔ ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ) )
8	7	bicomd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) ↔ 𝐾 < 𝑀 ) )
9		elnn0z	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
10		0red	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 0 ∈ ℝ )
11		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝐾 ∈ ℝ )
13	5	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
14		lelttr	⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 0 < 𝑀 ) )
15	10 12 13 14	syl3anc	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 0 < 𝑀 ) )
16		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
17		elnnz	⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
18	17	simplbi2	⊢ ( 𝑀 ∈ ℤ → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
19	16 18	syl	⊢ ( 𝑀 ∈ ℕ0 → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
20	19	adantl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 < 𝑀 → 𝑀 ∈ ℕ ) )
21	15 20	syld	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 < 𝑀 ) → 𝑀 ∈ ℕ ) )
22	21	expd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ 𝐾 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
23	22	impancom	⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
24	9 23	sylbi	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) ) )
25	24	imp	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 < 𝑀 → 𝑀 ∈ ℕ ) )
26	8 25	sylbid	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) → 𝑀 ∈ ℕ ) )
27	26	expd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑀 → ( 𝑀 ≠ 𝐾 → 𝑀 ∈ ℕ ) ) )
28	3 27	syl7bi	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑀 → ( 𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ ) ) )
29	28	3impia	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ ) )
30	29	imp	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝑀 ∈ ℕ )
31	8	biimpd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾 ) → 𝐾 < 𝑀 ) )
32	31	exp4b	⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑀 → ( 𝑀 ≠ 𝐾 → 𝐾 < 𝑀 ) ) ) )
33	32	3imp	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 ≠ 𝐾 → 𝐾 < 𝑀 ) )
34	3 33	syl5bi	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → 𝐾 < 𝑀 ) )
35	34	imp	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → 𝐾 < 𝑀 )
36	2 30 35	3jca	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) ∧ 𝐾 ≠ 𝑀 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
37	36	ex	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝐾 ≤ 𝑀 ) → ( 𝐾 ≠ 𝑀 → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) ) )
38	1 37	sylbi	⊢ ( 𝐾 ∈ ( 0 ... 𝑀 ) → ( 𝐾 ≠ 𝑀 → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) ) )
39	38	impcom	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
40		elfzo0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀 ) )
41	39 40	sylibr	⊢ ( ( 𝐾 ≠ 𝑀 ∧ 𝐾 ∈ ( 0 ... 𝑀 ) ) → 𝐾 ∈ ( 0 ..^ 𝑀 ) )