Metamath Proof Explorer

Theorem fzrevral2

Description: Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

		Ref	Expression
	Assertion	fzrevral2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (K - N \dots K - M) φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$

Proof

Step	Hyp	Ref	Expression
1		zsubcl	$⊢ (K \in ℤ \land N \in ℤ) \to K - N \in ℤ$
2	1	3adant2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K - N \in ℤ$
3		zsubcl	$⊢ (K \in ℤ \land M \in ℤ) \to K - M \in ℤ$
4	3	3adant3	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K - M \in ℤ$
5		simp1	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to K \in ℤ$
6		fzrevral	$⊢ (K - N \in ℤ \land K - M \in ℤ \land K \in ℤ) \to (\forall j \in (K - N \dots K - M) φ \leftrightarrow \forall k \in (K - (K - M) \dots K - (K - N)) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
7	2 4 5 6	syl3anc	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\forall j \in (K - N \dots K - M) φ \leftrightarrow \forall k \in (K - (K - M) \dots K - (K - N)) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
8		zcn	$⊢ K \in ℤ \to K \in ℂ$
9		zcn	$⊢ M \in ℤ \to M \in ℂ$
10		zcn	$⊢ N \in ℤ \to N \in ℂ$
11		nncan	$⊢ (K \in ℂ \land M \in ℂ) \to K - (K - M) = M$
12	11	3adant3	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to K - (K - M) = M$
13		nncan	$⊢ (K \in ℂ \land N \in ℂ) \to K - (K - N) = N$
14	13	3adant2	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to K - (K - N) = N$
15	12 14	oveq12d	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to (K - (K - M) \dots K - (K - N)) = (M \dots N)$
16	8 9 10 15	syl3an	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K - (K - M) \dots K - (K - N)) = (M \dots N)$
17	16	raleqdv	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\forall k \in (K - (K - M) \dots K - (K - N)) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
18	7 17	bitrd	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (\forall j \in (K - N \dots K - M) φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
19	18	3coml	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (K - N \dots K - M) φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$