isumshft

Description: Index shift of an infinite sum. (Contributed by Paul Chapman, 31-Oct-2007) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumshft.1	$⊢ Z = ℤ_{\geq M}$
	isumshft.2	$⊢ W = ℤ_{\geq (M + K)}$
	isumshft.3	$⊢ j = K + k \to A = B$
	isumshft.4	$⊢ φ \to K \in ℤ$
	isumshft.5	$⊢ φ \to M \in ℤ$
	isumshft.6	$⊢ (φ \land j \in W) \to A \in ℂ$
Assertion	isumshft	$⊢ φ \to \sum_{j \in W} A = \sum_{k \in Z} B$

Proof

Step	Hyp	Ref	Expression
1		isumshft.1	$⊢ Z = ℤ_{\geq M}$
2		isumshft.2	$⊢ W = ℤ_{\geq (M + K)}$
3		isumshft.3	$⊢ j = K + k \to A = B$
4		isumshft.4	$⊢ φ \to K \in ℤ$
5		isumshft.5	$⊢ φ \to M \in ℤ$
6		isumshft.6	$⊢ (φ \land j \in W) \to A \in ℂ$
7	5 4	zaddcld	$⊢ φ \to M + K \in ℤ$
8	2	eleq2i	$⊢ m \in W \leftrightarrow m \in ℤ_{\geq (M + K)}$
9	4	zcnd	$⊢ φ \to K \in ℂ$
10		eluzelcn	$⊢ m \in ℤ_{\geq (M + K)} \to m \in ℂ$
11	10 2	eleq2s	$⊢ m \in W \to m \in ℂ$
12	1	fvexi	$⊢ Z \in V$
13	12	mptex	$⊢ (k \in Z ⟼ B) \in V$
14	13	shftval	$⊢ (K \in ℂ \land m \in ℂ) \to ((k \in Z ⟼ B) shift K) (m) = (k \in Z ⟼ B) (m - K)$
15	9 11 14	syl2an	$⊢ (φ \land m \in W) \to ((k \in Z ⟼ B) shift K) (m) = (k \in Z ⟼ B) (m - K)$
16		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
17		eqid	$⊢ (k \in Z ⟼ B) = (k \in Z ⟼ B)$
18	17	fvmpt2i	$⊢ k \in Z \to (k \in Z ⟼ B) (k) = I (B)$
19	16 18	syl	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ B) (k) = I (B)$
20		eluzelcn	$⊢ k \in ℤ_{\geq M} \to k \in ℂ$
21	20 1	eleq2s	$⊢ k \in Z \to k \in ℂ$
22		addcom	$⊢ (K \in ℂ \land k \in ℂ) \to K + k = k + K$
23	9 21 22	syl2an	$⊢ (φ \land k \in Z) \to K + k = k + K$
24		id	$⊢ k \in Z \to k \in Z$
25	24 1	eleqtrdi	$⊢ k \in Z \to k \in ℤ_{\geq M}$
26		eluzadd	$⊢ (k \in ℤ_{\geq M} \land K \in ℤ) \to k + K \in ℤ_{\geq (M + K)}$
27	25 4 26	syl2anr	$⊢ (φ \land k \in Z) \to k + K \in ℤ_{\geq (M + K)}$
28	23 27	eqeltrd	$⊢ (φ \land k \in Z) \to K + k \in ℤ_{\geq (M + K)}$
29	28 2	eleqtrrdi	$⊢ (φ \land k \in Z) \to K + k \in W$
30		eqid	$⊢ (j \in W ⟼ A) = (j \in W ⟼ A)$
31	3 30	fvmpti	$⊢ K + k \in W \to (j \in W ⟼ A) (K + k) = I (B)$
32	29 31	syl	$⊢ (φ \land k \in Z) \to (j \in W ⟼ A) (K + k) = I (B)$
33	19 32	eqtr4d	$⊢ (φ \land k \in Z) \to (k \in Z ⟼ B) (k) = (j \in W ⟼ A) (K + k)$
34	33	ralrimiva	$⊢ φ \to \forall k \in Z (k \in Z ⟼ B) (k) = (j \in W ⟼ A) (K + k)$
35		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in Z ⟼ B) (n)$
36	35	nfeq1	$⊢ Ⅎ k (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n)$
37		fveq2	$⊢ k = n \to (k \in Z ⟼ B) (k) = (k \in Z ⟼ B) (n)$
38		oveq2	$⊢ k = n \to K + k = K + n$
39	38	fveq2d	$⊢ k = n \to (j \in W ⟼ A) (K + k) = (j \in W ⟼ A) (K + n)$
40	37 39	eqeq12d	$⊢ k = n \to ((k \in Z ⟼ B) (k) = (j \in W ⟼ A) (K + k) \leftrightarrow (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n))$
41	36 40	rspc	$⊢ n \in Z \to (\forall k \in Z (k \in Z ⟼ B) (k) = (j \in W ⟼ A) (K + k) \to (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n))$
42	34 41	mpan9	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n)$
43	42	ralrimiva	$⊢ φ \to \forall n \in Z (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n)$
44	5	adantr	$⊢ (φ \land m \in W) \to M \in ℤ$
45	4	adantr	$⊢ (φ \land m \in W) \to K \in ℤ$
46		simpr	$⊢ (φ \land m \in W) \to m \in W$
47	46 2	eleqtrdi	$⊢ (φ \land m \in W) \to m \in ℤ_{\geq (M + K)}$
48		eluzsub	$⊢ (M \in ℤ \land K \in ℤ \land m \in ℤ_{\geq (M + K)}) \to m - K \in ℤ_{\geq M}$
49	44 45 47 48	syl3anc	$⊢ (φ \land m \in W) \to m - K \in ℤ_{\geq M}$
50	49 1	eleqtrrdi	$⊢ (φ \land m \in W) \to m - K \in Z$
51		fveq2	$⊢ n = m - K \to (k \in Z ⟼ B) (n) = (k \in Z ⟼ B) (m - K)$
52		oveq2	$⊢ n = m - K \to K + n = K + m - K$
53	52	fveq2d	$⊢ n = m - K \to (j \in W ⟼ A) (K + n) = (j \in W ⟼ A) (K + m - K)$
54	51 53	eqeq12d	$⊢ n = m - K \to ((k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n) \leftrightarrow (k \in Z ⟼ B) (m - K) = (j \in W ⟼ A) (K + m - K))$
55	54	rspccva	$⊢ (\forall n \in Z (k \in Z ⟼ B) (n) = (j \in W ⟼ A) (K + n) \land m - K \in Z) \to (k \in Z ⟼ B) (m - K) = (j \in W ⟼ A) (K + m - K)$
56	43 50 55	syl2an2r	$⊢ (φ \land m \in W) \to (k \in Z ⟼ B) (m - K) = (j \in W ⟼ A) (K + m - K)$
57		pncan3	$⊢ (K \in ℂ \land m \in ℂ) \to K + m - K = m$
58	9 11 57	syl2an	$⊢ (φ \land m \in W) \to K + m - K = m$
59	58	fveq2d	$⊢ (φ \land m \in W) \to (j \in W ⟼ A) (K + m - K) = (j \in W ⟼ A) (m)$
60	15 56 59	3eqtrrd	$⊢ (φ \land m \in W) \to (j \in W ⟼ A) (m) = ((k \in Z ⟼ B) shift K) (m)$
61	8 60	sylan2br	$⊢ (φ \land m \in ℤ_{\geq (M + K)}) \to (j \in W ⟼ A) (m) = ((k \in Z ⟼ B) shift K) (m)$
62	7 61	seqfeq	$⊢ φ \to seq (M + K) (+ (j \in W ⟼ A)) = seq (M + K) (+ ((k \in Z ⟼ B) shift K))$
63	62	breq1d	$⊢ φ \to (seq (M + K) (+ (j \in W ⟼ A)) ⇝ x \leftrightarrow seq (M + K) (+ ((k \in Z ⟼ B) shift K)) ⇝ x)$
64	13	isershft	$⊢ (M \in ℤ \land K \in ℤ) \to (seq M (+ (k \in Z ⟼ B)) ⇝ x \leftrightarrow seq (M + K) (+ ((k \in Z ⟼ B) shift K)) ⇝ x)$
65	5 4 64	syl2anc	$⊢ φ \to (seq M (+ (k \in Z ⟼ B)) ⇝ x \leftrightarrow seq (M + K) (+ ((k \in Z ⟼ B) shift K)) ⇝ x)$
66	63 65	bitr4d	$⊢ φ \to (seq (M + K) (+ (j \in W ⟼ A)) ⇝ x \leftrightarrow seq M (+ (k \in Z ⟼ B)) ⇝ x)$
67	66	iotabidv	$⊢ φ \to (ι x \| seq (M + K) (+ (j \in W ⟼ A)) ⇝ x) = (ι x \| seq M (+ (k \in Z ⟼ B)) ⇝ x)$
68		df-fv	$⊢ ⇝ (seq (M + K) (+ (j \in W ⟼ A))) = (ι x \| seq (M + K) (+ (j \in W ⟼ A)) ⇝ x)$
69		df-fv	$⊢ ⇝ (seq M (+ (k \in Z ⟼ B))) = (ι x \| seq M (+ (k \in Z ⟼ B)) ⇝ x)$
70	67 68 69	3eqtr4g	$⊢ φ \to ⇝ (seq (M + K) (+ (j \in W ⟼ A))) = ⇝ (seq M (+ (k \in Z ⟼ B)))$
71		eqidd	$⊢ (φ \land m \in W) \to (j \in W ⟼ A) (m) = (j \in W ⟼ A) (m)$
72	6	fmpttd	$⊢ φ \to (j \in W ⟼ A) : W ⟶ ℂ$
73	72	ffvelrnda	$⊢ (φ \land m \in W) \to (j \in W ⟼ A) (m) \in ℂ$
74	2 7 71 73	isum	$⊢ φ \to \sum_{m \in W} (j \in W ⟼ A) (m) = ⇝ (seq (M + K) (+ (j \in W ⟼ A)))$
75		eqidd	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ B) (n) = (k \in Z ⟼ B) (n)$
76	29	ralrimiva	$⊢ φ \to \forall k \in Z K + k \in W$
77	38	eleq1d	$⊢ k = n \to (K + k \in W \leftrightarrow K + n \in W)$
78	77	rspccva	$⊢ (\forall k \in Z K + k \in W \land n \in Z) \to K + n \in W$
79	76 78	sylan	$⊢ (φ \land n \in Z) \to K + n \in W$
80		ffvelrn	$⊢ ((j \in W ⟼ A) : W ⟶ ℂ \land K + n \in W) \to (j \in W ⟼ A) (K + n) \in ℂ$
81	72 79 80	syl2an2r	$⊢ (φ \land n \in Z) \to (j \in W ⟼ A) (K + n) \in ℂ$
82	42 81	eqeltrd	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ B) (n) \in ℂ$
83	1 5 75 82	isum	$⊢ φ \to \sum_{n \in Z} (k \in Z ⟼ B) (n) = ⇝ (seq M (+ (k \in Z ⟼ B)))$
84	70 74 83	3eqtr4d	$⊢ φ \to \sum_{m \in W} (j \in W ⟼ A) (m) = \sum_{n \in Z} (k \in Z ⟼ B) (n)$
85		sumfc	$⊢ \sum_{m \in W} (j \in W ⟼ A) (m) = \sum_{j \in W} A$
86		sumfc	$⊢ \sum_{n \in Z} (k \in Z ⟼ B) (n) = \sum_{k \in Z} B$
87	84 85 86	3eqtr3g	$⊢ φ \to \sum_{j \in W} A = \sum_{k \in Z} B$

Metamath Proof Explorer

Theorem isumshft

Proof