Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	fzo0opth.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	fzo0opth	⊢ ( 𝜑 → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ 𝑀 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzo0opth.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
2		fzo0opth.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		0z	⊢ 0 ∈ ℤ
4	1	nn0zd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝑀 ) → 0 < 𝑀 )
6		fzoopth	⊢ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
7	3 4 5 6	mp3an2ani	⊢ ( ( 𝜑 ∧ 0 < 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) ) )
8		eqid	⊢ 0 = 0
9	8	biantrur	⊢ ( 𝑀 = 𝑁 ↔ ( 0 = 0 ∧ 𝑀 = 𝑁 ) )
10	7 9	bitr4di	⊢ ( ( 𝜑 ∧ 0 < 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ 𝑀 = 𝑁 ) )
11		simpr	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → 0 = 𝑀 )
12	11	oveq2d	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 0 ..^ 0 ) = ( 0 ..^ 𝑀 ) )
13		fzo0	⊢ ( 0 ..^ 0 ) = ∅
14	12 13	eqtr3di	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 0 ..^ 𝑀 ) = ∅ )
15	14	eqeq1d	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ∅ = ( 0 ..^ 𝑁 ) ) )
16		eqcom	⊢ ( ∅ = ( 0 ..^ 𝑁 ) ↔ ( 0 ..^ 𝑁 ) = ∅ )
17	15 16	bitrdi	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ ( 0 ..^ 𝑁 ) = ∅ ) )
18		0zd	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → 0 ∈ ℤ )
19	2	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
20	19	adantr	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → 𝑁 ∈ ℤ )
21		fzon	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 0 ↔ ( 0 ..^ 𝑁 ) = ∅ ) )
22	18 20 21	syl2anc	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 𝑁 ≤ 0 ↔ ( 0 ..^ 𝑁 ) = ∅ ) )
23		nn0le0eq0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 ↔ 𝑁 = 0 ) )
24	23	biimpa	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 0 ) → 𝑁 = 0 )
25	2 24	sylan	⊢ ( ( 𝜑 ∧ 𝑁 ≤ 0 ) → 𝑁 = 0 )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 0 = 𝑀 ) ∧ 𝑁 ≤ 0 ) → 𝑁 = 0 )
27		id	⊢ ( 𝑁 = 0 → 𝑁 = 0 )
28		0le0	⊢ 0 ≤ 0
29	27 28	eqbrtrdi	⊢ ( 𝑁 = 0 → 𝑁 ≤ 0 )
30	29	adantl	⊢ ( ( ( 𝜑 ∧ 0 = 𝑀 ) ∧ 𝑁 = 0 ) → 𝑁 ≤ 0 )
31	26 30	impbida	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 𝑁 ≤ 0 ↔ 𝑁 = 0 ) )
32		eqcom	⊢ ( 𝑁 = 0 ↔ 0 = 𝑁 )
33	32	a1i	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 𝑁 = 0 ↔ 0 = 𝑁 ) )
34	11	eqeq1d	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 0 = 𝑁 ↔ 𝑀 = 𝑁 ) )
35	31 33 34	3bitrd	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( 𝑁 ≤ 0 ↔ 𝑀 = 𝑁 ) )
36	17 22 35	3bitr2d	⊢ ( ( 𝜑 ∧ 0 = 𝑀 ) → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ 𝑀 = 𝑁 ) )
37	1	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝑀 )
38		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
39	1	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
40	38 39	leloed	⊢ ( 𝜑 → ( 0 ≤ 𝑀 ↔ ( 0 < 𝑀 ∨ 0 = 𝑀 ) ) )
41	37 40	mpbid	⊢ ( 𝜑 → ( 0 < 𝑀 ∨ 0 = 𝑀 ) )
42	10 36 41	mpjaodan	⊢ ( 𝜑 → ( ( 0 ..^ 𝑀 ) = ( 0 ..^ 𝑁 ) ↔ 𝑀 = 𝑁 ) )