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	$⊢ (K \neq M \land K \in (0 \dots M)) \to K \in (0 ..^M)$

Proof

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

Metamath Proof Explorer

Theorem fzofzim

Proof