Theorem fzshftralt 6454

Description: Shift the scanning order inside of a quantification over a finite set of sequential integers.

Assertion

Ref	Expression
fzshftralt	|- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. (M...N)ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))

Distinct variable groups:   j,k,K   j,M,k   j,N,k   ph,k

Proof of Theorem fzshftralt

Step	Hyp	Ref	Expression
1		0z 6093	. . . 4 |- 0 e. ZZ
2		fzrevralt 6451	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ 0 e. ZZ) -> (A.j e. (M...N)ph <-> A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph))
3	1, 2	mp3an3 902	. . 3 |- ((M e. ZZ /\ N e. ZZ) -> (A.j e. (M...N)ph <-> A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph))
4	3	3adant3 797	. 2 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. (M...N)ph <-> A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph))
5		fzrevralt 6451	. . . 4 |- (((0 - N) e. ZZ /\ (0 - M) e. ZZ /\ K e. ZZ) -> (A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph <-> A.k e. ((K - (0 - M))...(K - (0 - N)))[(K - k) / x][(0 - x) / j]ph))
6		zsubclt 6115	. . . . 5 |- ((0 e. ZZ /\ N e. ZZ) -> (0 - N) e. ZZ)
7	1, 6	mpan 693	. . . 4 |- (N e. ZZ -> (0 - N) e. ZZ)
8		zsubclt 6115	. . . . 5 |- ((0 e. ZZ /\ M e. ZZ) -> (0 - M) e. ZZ)
9	1, 8	mpan 693	. . . 4 |- (M e. ZZ -> (0 - M) e. ZZ)
10		id 59	. . . 4 |- (K e. ZZ -> K e. ZZ)
11	5, 7, 9, 10	syl3an 866	. . 3 |- ((N e. ZZ /\ M e. ZZ /\ K e. ZZ) -> (A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph <-> A.k e. ((K - (0 - M))...(K - (0 - N)))[(K - k) / x][(0 - x) / j]ph))
12	11	3com12 835	. 2 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.x e. ((0 - N)...(0 - M))[(0 - x) / j]ph <-> A.k e. ((K - (0 - M))...(K - (0 - N)))[(K - k) / x][(0 - x) / j]ph))
13		subnegt 5366	. . . . . . . . . . 11 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (K + M))
14		axaddcom 5247	. . . . . . . . . . 11 |- ((K e. CC /\ M e. CC) -> (K + M) = (M + K))
15	13, 14	eqtrd 1499	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (M + K))
16		df-neg 5330	. . . . . . . . . . 11 |- -uM = (0 - M)
17	16	opreq2i 3957	. . . . . . . . . 10 |- (K - -uM) = (K - (0 - M))
18	15, 17	syl5eqr 1513	. . . . . . . . 9 |- ((K e. CC /\ M e. CC) -> (K - (0 - M)) = (M + K))
19	18	3adant3 797	. . . . . . . 8 |- ((K e. CC /\ M e. CC /\ N e. CC) -> (K - (0 - M)) = (M + K))
20		subnegt 5366	. . . . . . . . . . 11 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (K + N))
21		axaddcom 5247	. . . . . . . . . . 11 |- ((K e. CC /\ N e. CC) -> (K + N) = (N + K))
22	20, 21	eqtrd 1499	. . . . . . . . . 10 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (N + K))
23		df-neg 5330	. . . . . . . . . . 11 |- -uN = (0 - N)
24	23	opreq2i 3957	. . . . . . . . . 10 |- (K - -uN) = (K - (0 - N))
25	22, 24	syl5eqr 1513	. . . . . . . . 9 |- ((K e. CC /\ N e. CC) -> (K - (0 - N)) = (N + K))
26	25	3adant2 796	. . . . . . . 8 |- ((K e. CC /\ M e. CC /\ N e. CC) -> (K - (0 - N)) = (N + K))
27	19, 26	opreq12d 3963	. . . . . . 7 |- ((K e. CC /\ M e. CC /\ N e. CC) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
28	27	3coml 838	. . . . . 6 |- ((M e. CC /\ N e. CC /\ K e. CC) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
29		zcnt 6087	. . . . . 6 |- (M e. ZZ -> M e. CC)
30		zcnt 6087	. . . . . 6 |- (N e. ZZ -> N e. CC)
31		zcnt 6087	. . . . . 6 |- (K e. ZZ -> K e. CC)
32	28, 29, 30, 31	syl3an 866	. . . . 5 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
33	32	raleq1d 1781	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.k e. ((K - (0 - M))...(K - (0 - N)))[(0 - (K - k)) / j]ph <-> A.k e. ((M + K)...(N + K))[(0 - (K - k)) / j]ph))
34		negsubdi2t 5430	. . . . . . . . 9 |- ((K e. CC /\ k e. CC) -> -u(K - k) = (k - K))
35		df-neg 5330	. . . . . . . . 9 |- -u(K - k) = (0 - (K - k))
36	34, 35	syl5eqr 1513	. . . . . . . 8 |- ((K e. CC /\ k e. CC) -> (0 - (K - k)) = (k - K))
37		elfzelz 6414	. . . . . . . . 9 |- (k e. ((M + K)...(N + K)) -> k e. ZZ)
38		zcnt 6087	. . . . . . . . 9 |- (k e. ZZ -> k e. CC)
39	37, 38	syl 10	. . . . . . . 8 |- (k e. ((M + K)...(N + K)) -> k e. CC)
40	36, 31, 39	syl2an 454	. . . . . . 7 |- ((K e. ZZ /\ k e. ((M + K)...(N + K))) -> (0 - (K - k)) = (k - K))
41		dfsbcq 1933	. . . . . . 7 |- ((0 - (K - k)) = (k - K) -> ([(0 - (K - k)) / j]ph <-> [(k - K) / j]ph))
42	40, 41	syl 10	. . . . . 6 |- ((K e. ZZ /\ k e. ((M + K)...(N + K))) -> ([(0 - (K - k)) / j]ph <-> [(k - K) / j]ph))
43	42	ralbidva 1651	. . . . 5 |- (K e. ZZ -> (A.k e. ((M + K)...(N + K))[(0 - (K - k)) / j]ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))
44	43	3ad2ant3 800	. . . 4 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.k e. ((M + K)...(N + K))[(0 - (K - k)) / j]ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))
45	33, 44	bitrd 526	. . 3 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.k e. ((K - (0 - M))...(K - (0 - N)))[(0 - (K - k)) / j]ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))
46		oprex 3968	. . . . 5 |- (K - k) e. V
47		oprex 3968	. . . . . 6 |- (0 - x) e. V
48	47	ax-gen 960	. . . . 5 |- A.x(0 - x) e. V
49		opreq2 3954	. . . . . 6 |- (x = (K - k) -> (0 - x) = (0 - (K - k)))
50	49	sbcco3g 2031	. . . . 5 |- (((K - k) e. V /\ A.x(0 - x) e. V) -> ([(K - k) / x][(0 - x) / j]ph <-> [(0 - (K - k)) / j]ph))
51	46, 48, 50	mp2an 695	. . . 4 |- ([(K - k) / x][(0 - x) / j]ph <-> [(0 - (K - k)) / j]ph)
52	51	ralbii 1659	. . 3 |- (A.k e. ((K - (0 - M))...(K - (0 - N)))[(K - k) / x][(0 - x) / j]ph <-> A.k e. ((K - (0 - M))...(K - (0 - N)))[(0 - (K - k)) / j]ph)
53	45, 52	syl5bb 530	. 2 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.k e. ((K - (0 - M))...(K - (0 - N)))[(K - k) / x][(0 - x) / j]ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j]ph))
54	4, 12, 53	3bitrd 542	1 |- ((M e. ZZ /\ N e. ZZ /\ K e. ZZ) -> (A.j e. (M...N)ph <-> A.k e. ((M + K)...(N + K))[(k - K) / j