Metamath Proof Explorer

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 
|- ( ph -> M e. NN0 )
fzo0opth.2 
|- ( ph -> N e. NN0 )
Assertion fzo0opth 
|- ( ph -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> M = N ) )

Proof

Step Hyp Ref Expression
1 fzo0opth.1 
 |-  ( ph -> M e. NN0 )
2 fzo0opth.2 
 |-  ( ph -> N e. NN0 )
3 0z 
 |-  0 e. ZZ
4 1 nn0zd 
 |-  ( ph -> M e. ZZ )
5 simpr 
 |-  ( ( ph /\ 0 < M ) -> 0 < M )
6 fzoopth 
 |-  ( ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> ( 0 = 0 /\ M = N ) ) )
7 3 4 5 6 mp3an2ani 
 |-  ( ( ph /\ 0 < M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> ( 0 = 0 /\ M = N ) ) )
8 eqid 
 |-  0 = 0
9 8 biantrur 
 |-  ( M = N <-> ( 0 = 0 /\ M = N ) )
10 7 9 bitr4di 
 |-  ( ( ph /\ 0 < M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> M = N ) )
11 simpr 
 |-  ( ( ph /\ 0 = M ) -> 0 = M )
12 11 oveq2d 
 |-  ( ( ph /\ 0 = M ) -> ( 0 ..^ 0 ) = ( 0 ..^ M ) )
13 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
14 12 13 eqtr3di 
 |-  ( ( ph /\ 0 = M ) -> ( 0 ..^ M ) = (/) )
15 14 eqeq1d 
 |-  ( ( ph /\ 0 = M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> (/) = ( 0 ..^ N ) ) )
16 eqcom 
 |-  ( (/) = ( 0 ..^ N ) <-> ( 0 ..^ N ) = (/) )
17 15 16 bitrdi 
 |-  ( ( ph /\ 0 = M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> ( 0 ..^ N ) = (/) ) )
18 0zd 
 |-  ( ( ph /\ 0 = M ) -> 0 e. ZZ )
19 2 nn0zd 
 |-  ( ph -> N e. ZZ )
20 19 adantr 
 |-  ( ( ph /\ 0 = M ) -> N e. ZZ )
21 fzon 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( N <_ 0 <-> ( 0 ..^ N ) = (/) ) )
22 18 20 21 syl2anc 
 |-  ( ( ph /\ 0 = M ) -> ( N <_ 0 <-> ( 0 ..^ N ) = (/) ) )
23 nn0le0eq0 
 |-  ( N e. NN0 -> ( N <_ 0 <-> N = 0 ) )
24 23 biimpa 
 |-  ( ( N e. NN0 /\ N <_ 0 ) -> N = 0 )
25 2 24 sylan 
 |-  ( ( ph /\ N <_ 0 ) -> N = 0 )
26 25 adantlr 
 |-  ( ( ( ph /\ 0 = M ) /\ N <_ 0 ) -> N = 0 )
27 id 
 |-  ( N = 0 -> N = 0 )
28 0le0 
 |-  0 <_ 0
29 27 28 eqbrtrdi 
 |-  ( N = 0 -> N <_ 0 )
30 29 adantl 
 |-  ( ( ( ph /\ 0 = M ) /\ N = 0 ) -> N <_ 0 )
31 26 30 impbida 
 |-  ( ( ph /\ 0 = M ) -> ( N <_ 0 <-> N = 0 ) )
32 eqcom 
 |-  ( N = 0 <-> 0 = N )
33 32 a1i 
 |-  ( ( ph /\ 0 = M ) -> ( N = 0 <-> 0 = N ) )
34 11 eqeq1d 
 |-  ( ( ph /\ 0 = M ) -> ( 0 = N <-> M = N ) )
35 31 33 34 3bitrd 
 |-  ( ( ph /\ 0 = M ) -> ( N <_ 0 <-> M = N ) )
36 17 22 35 3bitr2d 
 |-  ( ( ph /\ 0 = M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> M = N ) )
37 1 nn0ge0d 
 |-  ( ph -> 0 <_ M )
38 0red 
 |-  ( ph -> 0 e. RR )
39 1 nn0red 
 |-  ( ph -> M e. RR )
40 38 39 leloed 
 |-  ( ph -> ( 0 <_ M <-> ( 0 < M \/ 0 = M ) ) )
41 37 40 mpbid 
 |-  ( ph -> ( 0 < M \/ 0 = M ) )
42 10 36 41 mpjaodan 
 |-  ( ph -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> M = N ) )