Metamath Proof Explorer

Theorem fzrev3

Description: The "complement" of a member of a finite set of sequential integers. (Contributed by NM, 20-Nov-2005)

Ref Expression
Assertion fzrev3 
|- ( K e. ZZ -> ( K e. ( M ... N ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( K e. ZZ /\ K e. ( M ... N ) ) -> K e. ZZ )
2 elfzel1 
 |-  ( K e. ( M ... N ) -> M e. ZZ )
3 2 adantl 
 |-  ( ( K e. ZZ /\ K e. ( M ... N ) ) -> M e. ZZ )
4 elfzel2 
 |-  ( K e. ( M ... N ) -> N e. ZZ )
5 4 adantl 
 |-  ( ( K e. ZZ /\ K e. ( M ... N ) ) -> N e. ZZ )
6 1 3 5 3jca 
 |-  ( ( K e. ZZ /\ K e. ( M ... N ) ) -> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
7 simpl 
 |-  ( ( K e. ZZ /\ ( ( M + N ) - K ) e. ( M ... N ) ) -> K e. ZZ )
8 elfzel1 
 |-  ( ( ( M + N ) - K ) e. ( M ... N ) -> M e. ZZ )
9 8 adantl 
 |-  ( ( K e. ZZ /\ ( ( M + N ) - K ) e. ( M ... N ) ) -> M e. ZZ )
10 elfzel2 
 |-  ( ( ( M + N ) - K ) e. ( M ... N ) -> N e. ZZ )
11 10 adantl 
 |-  ( ( K e. ZZ /\ ( ( M + N ) - K ) e. ( M ... N ) ) -> N e. ZZ )
12 7 9 11 3jca 
 |-  ( ( K e. ZZ /\ ( ( M + N ) - K ) e. ( M ... N ) ) -> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
13 zcn 
 |-  ( M e. ZZ -> M e. CC )
14 zcn 
 |-  ( N e. ZZ -> N e. CC )
15 pncan 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - N ) = M )
16 pncan2 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - M ) = N )
17 15 16 oveq12d 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) = ( M ... N ) )
18 13 14 17 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) = ( M ... N ) )
19 18 eleq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) <-> K e. ( M ... N ) ) )
20 19 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) <-> K e. ( M ... N ) ) )
21 3simpc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M e. ZZ /\ N e. ZZ ) )
22 zaddcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
23 22 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
24 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
25 fzrev 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( M + N ) e. ZZ /\ K e. ZZ ) ) -> ( K e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )
26 21 23 24 25 syl12anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )
27 20 26 bitr3d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ... N ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )
28 6 12 27 pm5.21nd 
 |-  ( K e. ZZ -> ( K e. ( M ... N ) <-> ( ( M + N ) - K ) e. ( M ... N ) ) )