fzo0opth

Description: Equality for a half open integer range starting at zero is the same as equality of its upper bound, analogous to fzopth and fzoopth . (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	fzo0opth.1	$⊢ φ \to M \in ℕ_{0}$
	fzo0opth.2	$⊢ φ \to N \in ℕ_{0}$
Assertion	fzo0opth	$⊢ φ \to ((0 ..^M) = (0 ..^N) \leftrightarrow M = N)$

Proof

Step	Hyp	Ref	Expression
1		fzo0opth.1	$⊢ φ \to M \in ℕ_{0}$
2		fzo0opth.2	$⊢ φ \to N \in ℕ_{0}$
3		0z	$⊢ 0 \in ℤ$
4	1	nn0zd	$⊢ φ \to M \in ℤ$
5		simpr	$⊢ (φ \land 0 < M) \to 0 < M$
6		fzoopth	$⊢ (0 \in ℤ \land M \in ℤ \land 0 < M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow (0 = 0 \land M = N))$
7	3 4 5 6	mp3an2ani	$⊢ (φ \land 0 < M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow (0 = 0 \land M = N))$
8		eqid	$⊢ 0 = 0$
9	8	biantrur	$⊢ M = N \leftrightarrow (0 = 0 \land M = N)$
10	7 9	bitr4di	$⊢ (φ \land 0 < M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow M = N)$
11		simpr	$⊢ (φ \land 0 = M) \to 0 = M$
12	11	oveq2d	$⊢ (φ \land 0 = M) \to (0 ..^0) = (0 ..^M)$
13		fzo0	$⊢ (0 ..^0) = \emptyset$
14	12 13	eqtr3di	$⊢ (φ \land 0 = M) \to (0 ..^M) = \emptyset$
15	14	eqeq1d	$⊢ (φ \land 0 = M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow \emptyset = (0 ..^N))$
16		eqcom	$⊢ \emptyset = (0 ..^N) \leftrightarrow (0 ..^N) = \emptyset$
17	15 16	bitrdi	$⊢ (φ \land 0 = M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow (0 ..^N) = \emptyset)$
18		0zd	$⊢ (φ \land 0 = M) \to 0 \in ℤ$
19	2	nn0zd	$⊢ φ \to N \in ℤ$
20	19	adantr	$⊢ (φ \land 0 = M) \to N \in ℤ$
21		fzon	$⊢ (0 \in ℤ \land N \in ℤ) \to (N \leq 0 \leftrightarrow (0 ..^N) = \emptyset)$
22	18 20 21	syl2anc	$⊢ (φ \land 0 = M) \to (N \leq 0 \leftrightarrow (0 ..^N) = \emptyset)$
23		nn0le0eq0	$⊢ N \in ℕ_{0} \to (N \leq 0 \leftrightarrow N = 0)$
24	23	biimpa	$⊢ (N \in ℕ_{0} \land N \leq 0) \to N = 0$
25	2 24	sylan	$⊢ (φ \land N \leq 0) \to N = 0$
26	25	adantlr	$⊢ ((φ \land 0 = M) \land N \leq 0) \to N = 0$
27		id	$⊢ N = 0 \to N = 0$
28		0le0	$⊢ 0 \leq 0$
29	27 28	eqbrtrdi	$⊢ N = 0 \to N \leq 0$
30	29	adantl	$⊢ ((φ \land 0 = M) \land N = 0) \to N \leq 0$
31	26 30	impbida	$⊢ (φ \land 0 = M) \to (N \leq 0 \leftrightarrow N = 0)$
32		eqcom	$⊢ N = 0 \leftrightarrow 0 = N$
33	32	a1i	$⊢ (φ \land 0 = M) \to (N = 0 \leftrightarrow 0 = N)$
34	11	eqeq1d	$⊢ (φ \land 0 = M) \to (0 = N \leftrightarrow M = N)$
35	31 33 34	3bitrd	$⊢ (φ \land 0 = M) \to (N \leq 0 \leftrightarrow M = N)$
36	17 22 35	3bitr2d	$⊢ (φ \land 0 = M) \to ((0 ..^M) = (0 ..^N) \leftrightarrow M = N)$
37	1	nn0ge0d	$⊢ φ \to 0 \leq M$
38		0red	$⊢ φ \to 0 \in ℝ$
39	1	nn0red	$⊢ φ \to M \in ℝ$
40	38 39	leloed	$⊢ φ \to (0 \leq M \leftrightarrow (0 < M \lor 0 = M))$
41	37 40	mpbid	$⊢ φ \to (0 < M \lor 0 = M)$
42	10 36 41	mpjaodan	$⊢ φ \to ((0 ..^M) = (0 ..^N) \leftrightarrow M = N)$

Metamath Proof Explorer

Theorem fzo0opth

Proof