This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzom1ne1

Description: Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024)

Ref Expression
Assertion fzom1ne1 
|- ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K - 1 ) e. ( M ..^ ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 fzone1 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ..^ N ) )
2 1z 
 |-  1 e. ZZ
3 fzosubel 
 |-  ( ( K e. ( ( M + 1 ) ..^ N ) /\ 1 e. ZZ ) -> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ..^ ( N - 1 ) ) )
4 1 2 3 sylancl 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ..^ ( N - 1 ) ) )
5 elfzoel1 
 |-  ( K e. ( M ..^ N ) -> M e. ZZ )
6 5 adantr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> M e. ZZ )
7 6 zcnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> M e. CC )
8 1cnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> 1 e. CC )
9 7 8 pncand 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( ( M + 1 ) - 1 ) = M )
10 9 oveq1d 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( ( ( M + 1 ) - 1 ) ..^ ( N - 1 ) ) = ( M ..^ ( N - 1 ) ) )
11 4 10 eleqtrd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K - 1 ) e. ( M ..^ ( N - 1 ) ) )