fzrevral

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	fzrevral	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land k \in (K - N \dots K - M)) \to k \in (K - N \dots K - M)$
2		elfzelz	$⊢ k \in (K - N \dots K - M) \to k \in ℤ$
3		fzrev	$⊢ ((M \in ℤ \land N \in ℤ) \land (K \in ℤ \land k \in ℤ)) \to (k \in (K - N \dots K - M) \leftrightarrow K - k \in (M \dots N))$
4	3	anassrs	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land k \in ℤ) \to (k \in (K - N \dots K - M) \leftrightarrow K - k \in (M \dots N))$
5	2 4	sylan2	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land k \in (K - N \dots K - M)) \to (k \in (K - N \dots K - M) \leftrightarrow K - k \in (M \dots N))$
6	1 5	mpbid	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land k \in (K - N \dots K - M)) \to K - k \in (M \dots N)$
7		rspsbc	$⊢ K - k \in (M \dots N) \to (\forall j \in (M \dots N) φ \to \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
8	6 7	syl	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℤ) \land k \in (K - N \dots K - M)) \to (\forall j \in (M \dots N) φ \to \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
9	8	ex3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (k \in (K - N \dots K - M) \to (\forall j \in (M \dots N) φ \to \underset{˙}{[} (K - k) / j \underset{˙}{]} φ))$
10	9	com23	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \to (k \in (K - N \dots K - M) \to \underset{˙}{[} (K - k) / j \underset{˙}{]} φ))$
11	10	ralrimdv	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \to \forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$
12		nfv	$⊢ Ⅎ j K \in ℤ$
13		nfcv	$⊢ \underline{Ⅎ} j (K - N \dots K - M)$
14		nfsbc1v	$⊢ Ⅎ j \underset{˙}{[} (K - k) / j \underset{˙}{]} φ$
15	13 14	nfralw	$⊢ Ⅎ j \forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ$
16		fzrev2i	$⊢ (K \in ℤ \land j \in (M \dots N)) \to K - j \in (K - N \dots K - M)$
17		oveq2	$⊢ k = K - j \to K - k = K - (K - j)$
18	17	sbceq1d	$⊢ k = K - j \to (\underset{˙}{[} (K - k) / j \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (K - (K - j)) / j \underset{˙}{]} φ)$
19	18	rspcv	$⊢ K - j \in (K - N \dots K - M) \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to \underset{˙}{[} (K - (K - j)) / j \underset{˙}{]} φ)$
20	16 19	syl	$⊢ (K \in ℤ \land j \in (M \dots N)) \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to \underset{˙}{[} (K - (K - j)) / j \underset{˙}{]} φ)$
21		zcn	$⊢ K \in ℤ \to K \in ℂ$
22		elfzelz	$⊢ j \in (M \dots N) \to j \in ℤ$
23	22	zcnd	$⊢ j \in (M \dots N) \to j \in ℂ$
24		nncan	$⊢ (K \in ℂ \land j \in ℂ) \to K - (K - j) = j$
25	21 23 24	syl2an	$⊢ (K \in ℤ \land j \in (M \dots N)) \to K - (K - j) = j$
26	25	eqcomd	$⊢ (K \in ℤ \land j \in (M \dots N)) \to j = K - (K - j)$
27		sbceq1a	$⊢ j = K - (K - j) \to (φ \leftrightarrow \underset{˙}{[} (K - (K - j)) / j \underset{˙}{]} φ)$
28	26 27	syl	$⊢ (K \in ℤ \land j \in (M \dots N)) \to (φ \leftrightarrow \underset{˙}{[} (K - (K - j)) / j \underset{˙}{]} φ)$
29	20 28	sylibrd	$⊢ (K \in ℤ \land j \in (M \dots N)) \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to φ)$
30	29	ex	$⊢ K \in ℤ \to (j \in (M \dots N) \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to φ))$
31	30	com23	$⊢ K \in ℤ \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to (j \in (M \dots N) \to φ))$
32	12 15 31	ralrimd	$⊢ K \in ℤ \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to \forall j \in (M \dots N) φ)$
33	32	3ad2ant3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ \to \forall j \in (M \dots N) φ)$
34	11 33	impbid	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (K - N \dots K - M) \underset{˙}{[} (K - k) / j \underset{˙}{]} φ)$

Metamath Proof Explorer

Theorem fzrevral

Proof