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 ) ) )