Metamath Proof Explorer

Theorem fzm1ne1

Description: Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 fzne1 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ... N ) )
2 elfzel1 
 |-  ( K e. ( ( M + 1 ) ... N ) -> ( M + 1 ) e. ZZ )
3 elfzel2 
 |-  ( K e. ( ( M + 1 ) ... N ) -> N e. ZZ )
4 elfzelz 
 |-  ( K e. ( ( M + 1 ) ... N ) -> K e. ZZ )
5 1zzd 
 |-  ( K e. ( ( M + 1 ) ... N ) -> 1 e. ZZ )
6 id 
 |-  ( K e. ( ( M + 1 ) ... N ) -> K e. ( ( M + 1 ) ... N ) )
7 fzsubel 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ 1 e. ZZ ) ) -> ( K e. ( ( M + 1 ) ... N ) <-> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) ) )
8 7 biimp3a 
 |-  ( ( ( ( M + 1 ) e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ 1 e. ZZ ) /\ K e. ( ( M + 1 ) ... N ) ) -> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) )
9 2 3 4 5 6 8 syl221anc 
 |-  ( K e. ( ( M + 1 ) ... N ) -> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) )
10 1 9 syl 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> ( K - 1 ) e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) )
11 elfzel1 
 |-  ( K e. ( M ... N ) -> M e. ZZ )
12 11 adantr 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> M e. ZZ )
13 12 zcnd 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> M e. CC )
14 1cnd 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> 1 e. CC )
15 13 14 pncand 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> ( ( M + 1 ) - 1 ) = M )
16 15 oveq1d 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) = ( M ... ( N - 1 ) ) )
17 10 16 eleqtrd 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> ( K - 1 ) e. ( M ... ( N - 1 ) ) )