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 \in ℤ \to (K \in (M \dots N) \leftrightarrow M + N - K \in (M \dots N))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (K \in ℤ \land K \in (M \dots N)) \to K \in ℤ$
2		elfzel1	$⊢ K \in (M \dots N) \to M \in ℤ$
3	2	adantl	$⊢ (K \in ℤ \land K \in (M \dots N)) \to M \in ℤ$
4		elfzel2	$⊢ K \in (M \dots N) \to N \in ℤ$
5	4	adantl	$⊢ (K \in ℤ \land K \in (M \dots N)) \to N \in ℤ$
6	1 3 5	3jca	$⊢ (K \in ℤ \land K \in (M \dots N)) \to (K \in ℤ \land M \in ℤ \land N \in ℤ)$
7		simpl	$⊢ (K \in ℤ \land M + N - K \in (M \dots N)) \to K \in ℤ$
8		elfzel1	$⊢ M + N - K \in (M \dots N) \to M \in ℤ$
9	8	adantl	$⊢ (K \in ℤ \land M + N - K \in (M \dots N)) \to M \in ℤ$
10		elfzel2	$⊢ M + N - K \in (M \dots N) \to N \in ℤ$
11	10	adantl	$⊢ (K \in ℤ \land M + N - K \in (M \dots N)) \to N \in ℤ$
12	7 9 11	3jca	$⊢ (K \in ℤ \land M + N - K \in (M \dots N)) \to (K \in ℤ \land M \in ℤ \land N \in ℤ)$
13		zcn	$⊢ M \in ℤ \to M \in ℂ$
14		zcn	$⊢ N \in ℤ \to N \in ℂ$
15		pncan	$⊢ (M \in ℂ \land N \in ℂ) \to M + N - N = M$
16		pncan2	$⊢ (M \in ℂ \land N \in ℂ) \to M + N - M = N$
17	15 16	oveq12d	$⊢ (M \in ℂ \land N \in ℂ) \to (M + N - N \dots M + N - M) = (M \dots N)$
18	13 14 17	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M + N - N \dots M + N - M) = (M \dots N)$
19	18	eleq2d	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M + N - N \dots M + N - M) \leftrightarrow K \in (M \dots N))$
20	19	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M + N - N \dots M + N - M) \leftrightarrow K \in (M \dots N))$
21		3simpc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (M \in ℤ \land N \in ℤ)$
22		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
23	22	3adant1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
24		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
25		fzrev	$⊢ ((M \in ℤ \land N \in ℤ) \land (M + N \in ℤ \land K \in ℤ)) \to (K \in (M + N - N \dots M + N - M) \leftrightarrow M + N - K \in (M \dots N))$
26	21 23 24 25	syl12anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M + N - N \dots M + N - M) \leftrightarrow M + N - K \in (M \dots N))$
27	20 26	bitr3d	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow M + N - K \in (M \dots N))$
28	6 12 27	pm5.21nd	$⊢ K \in ℤ \to (K \in (M \dots N) \leftrightarrow M + N - K \in (M \dots N))$

Metamath Proof Explorer

Theorem fzrev3

Proof