Metamath Proof Explorer

Theorem fzrevral3

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

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

Proof

Step	Hyp	Ref	Expression
1		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
2		fzrevral	$⊢ (M \in ℤ \land N \in ℤ \land M + N \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (M + N - N \dots M + N - M) \underset{˙}{[} (M + N - k) / j \underset{˙}{]} φ)$
3	1 2	mpd3an3	$⊢ (M \in ℤ \land N \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (M + N - N \dots M + N - M) \underset{˙}{[} (M + N - k) / j \underset{˙}{]} φ)$
4		zcn	$⊢ M \in ℤ \to M \in ℂ$
5		zcn	$⊢ N \in ℤ \to N \in ℂ$
6		pncan	$⊢ (M \in ℂ \land N \in ℂ) \to M + N - N = M$
7		pncan2	$⊢ (M \in ℂ \land N \in ℂ) \to M + N - M = N$
8	6 7	oveq12d	$⊢ (M \in ℂ \land N \in ℂ) \to (M + N - N \dots M + N - M) = (M \dots N)$
9	4 5 8	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M + N - N \dots M + N - M) = (M \dots N)$
10	9	raleqdv	$⊢ (M \in ℤ \land N \in ℤ) \to (\forall k \in (M + N - N \dots M + N - M) \underset{˙}{[} (M + N - k) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (M + N - k) / j \underset{˙}{]} φ)$
11	3 10	bitrd	$⊢ (M \in ℤ \land N \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (M \dots N) \underset{˙}{[} (M + N - k) / j \underset{˙}{]} φ)$