fzshftral

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

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

Proof

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		fzrevral	$⊢ (M \in ℤ \land N \in ℤ \land 0 \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
3	1 2	mp3an3	$⊢ (M \in ℤ \land N \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
4	3	3adant3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
5		zsubcl	$⊢ (0 \in ℤ \land N \in ℤ) \to 0 - N \in ℤ$
6	1 5	mpan	$⊢ N \in ℤ \to 0 - N \in ℤ$
7		zsubcl	$⊢ (0 \in ℤ \land M \in ℤ) \to 0 - M \in ℤ$
8	1 7	mpan	$⊢ M \in ℤ \to 0 - M \in ℤ$
9		id	$⊢ K \in ℤ \to K \in ℤ$
10		fzrevral	$⊢ (0 - N \in ℤ \land 0 - M \in ℤ \land K \in ℤ) \to (\forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
11	6 8 9 10	syl3an	$⊢ (N \in ℤ \land M \in ℤ \land K \in ℤ) \to (\forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
12	11	3com12	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall x \in (0 - N \dots 0 - M) \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ)$
13		ovex	$⊢ K - k \in V$
14		oveq2	$⊢ x = K - k \to 0 - x = 0 - (K - k)$
15	14	sbcco3gw	$⊢ K - k \in V \to (\underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ)$
16	13 15	ax-mp	$⊢ \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ$
17	16	ralbii	$⊢ \forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ$
18		zcn	$⊢ M \in ℤ \to M \in ℂ$
19		zcn	$⊢ N \in ℤ \to N \in ℂ$
20		zcn	$⊢ K \in ℤ \to K \in ℂ$
21		df-neg	$⊢ - M = 0 - M$
22	21	oveq2i	$⊢ K - -M = K - (0 - M)$
23		subneg	$⊢ (K \in ℂ \land M \in ℂ) \to K - -M = K + M$
24		addcom	$⊢ (K \in ℂ \land M \in ℂ) \to K + M = M + K$
25	23 24	eqtrd	$⊢ (K \in ℂ \land M \in ℂ) \to K - -M = M + K$
26	22 25	syl5eqr	$⊢ (K \in ℂ \land M \in ℂ) \to K - (0 - M) = M + K$
27	26	3adant3	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to K - (0 - M) = M + K$
28		df-neg	$⊢ - N = 0 - N$
29	28	oveq2i	$⊢ K - -N = K - (0 - N)$
30		subneg	$⊢ (K \in ℂ \land N \in ℂ) \to K - -N = K + N$
31		addcom	$⊢ (K \in ℂ \land N \in ℂ) \to K + N = N + K$
32	30 31	eqtrd	$⊢ (K \in ℂ \land N \in ℂ) \to K - -N = N + K$
33	29 32	syl5eqr	$⊢ (K \in ℂ \land N \in ℂ) \to K - (0 - N) = N + K$
34	33	3adant2	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to K - (0 - N) = N + K$
35	27 34	oveq12d	$⊢ (K \in ℂ \land M \in ℂ \land N \in ℂ) \to (K - (0 - M) \dots K - (0 - N)) = (M + K \dots N + K)$
36	35	3coml	$⊢ (M \in ℂ \land N \in ℂ \land K \in ℂ) \to (K - (0 - M) \dots K - (0 - N)) = (M + K \dots N + K)$
37	18 19 20 36	syl3an	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (K - (0 - M) \dots K - (0 - N)) = (M + K \dots N + K)$
38	37	raleqdv	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ)$
39		elfzelz	$⊢ k \in (M + K \dots N + K) \to k \in ℤ$
40	39	zcnd	$⊢ k \in (M + K \dots N + K) \to k \in ℂ$
41		df-neg	$⊢ - (K - k) = 0 - (K - k)$
42		negsubdi2	$⊢ (K \in ℂ \land k \in ℂ) \to - (K - k) = k - K$
43	41 42	syl5eqr	$⊢ (K \in ℂ \land k \in ℂ) \to 0 - (K - k) = k - K$
44	20 40 43	syl2an	$⊢ (K \in ℤ \land k \in (M + K \dots N + K)) \to 0 - (K - k) = k - K$
45	44	sbceq1d	$⊢ (K \in ℤ \land k \in (M + K \dots N + K)) \to (\underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
46	45	ralbidva	$⊢ K \in ℤ \to (\forall k \in (M + K \dots N + K) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
47	46	3ad2ant3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (M + K \dots N + K) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
48	38 47	bitrd	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (0 - (K - k)) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
49	17 48	syl5bb	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall k \in (K - (0 - M) \dots K - (0 - N)) \underset{˙}{[} (K - k) / x \underset{˙}{]} \underset{˙}{[} (0 - x) / j \underset{˙}{]} φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$
50	4 12 49	3bitrd	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (\forall j \in (M \dots N) φ \leftrightarrow \forall k \in (M + K \dots N + K) \underset{˙}{[} (k - K) / j \underset{˙}{]} φ)$

Metamath Proof Explorer

Theorem fzshftral

Proof