fsum0diag2

Description: Two ways to express "the sum of A ( j , k ) over the triangular region 0 <_ j , 0 <_ k , j + k <_ N ". (Contributed by Mario Carneiro, 21-Jul-2014)

	Ref	Expression
Hypotheses	fsum0diag2.1	$⊢ x = k \to B = A$
	fsum0diag2.2	$⊢ x = k - j \to B = C$
	fsum0diag2.3	$⊢ (φ \land (j \in (0 \dots N) \land k \in (0 \dots N - j))) \to A \in ℂ$
Assertion	fsum0diag2	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} A = \sum_{k = 0}^{N} \sum_{j = 0}^{k} C$

Proof

Step	Hyp	Ref	Expression
1		fsum0diag2.1	$⊢ x = k \to B = A$
2		fsum0diag2.2	$⊢ x = k - j \to B = C$
3		fsum0diag2.3	$⊢ (φ \land (j \in (0 \dots N) \land k \in (0 \dots N - j))) \to A \in ℂ$
4		fznn0sub2	$⊢ n \in (0 \dots N - j) \to N - j - n \in (0 \dots N - j)$
5	4	ad2antll	$⊢ (φ \land (j \in (0 \dots N) \land n \in (0 \dots N - j))) \to N - j - n \in (0 \dots N - j)$
6	3	expr	$⊢ (φ \land j \in (0 \dots N)) \to (k \in (0 \dots N - j) \to A \in ℂ)$
7	6	ralrimiv	$⊢ (φ \land j \in (0 \dots N)) \to \forall k \in (0 \dots N - j) A \in ℂ$
8	1	eleq1d	$⊢ x = k \to (B \in ℂ \leftrightarrow A \in ℂ)$
9	8	cbvralvw	$⊢ \forall x \in (0 \dots N - j) B \in ℂ \leftrightarrow \forall k \in (0 \dots N - j) A \in ℂ$
10	7 9	sylibr	$⊢ (φ \land j \in (0 \dots N)) \to \forall x \in (0 \dots N - j) B \in ℂ$
11	10	adantrr	$⊢ (φ \land (j \in (0 \dots N) \land n \in (0 \dots N - j))) \to \forall x \in (0 \dots N - j) B \in ℂ$
12		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ (N - j - n) / x ⦌ B$
13	12	nfel1	$⊢ Ⅎ x ⦋ (N - j - n) / x ⦌ B \in ℂ$
14		csbeq1a	$⊢ x = N - j - n \to B = ⦋ (N - j - n) / x ⦌ B$
15	14	eleq1d	$⊢ x = N - j - n \to (B \in ℂ \leftrightarrow ⦋ (N - j - n) / x ⦌ B \in ℂ)$
16	13 15	rspc	$⊢ N - j - n \in (0 \dots N - j) \to (\forall x \in (0 \dots N - j) B \in ℂ \to ⦋ (N - j - n) / x ⦌ B \in ℂ)$
17	5 11 16	sylc	$⊢ (φ \land (j \in (0 \dots N) \land n \in (0 \dots N - j))) \to ⦋ (N - j - n) / x ⦌ B \in ℂ$
18	17	fsum0diag	$⊢ φ \to \sum_{j = 0}^{N} \sum_{n = 0}^{N - j} ⦋ (N - j - n) / x ⦌ B = \sum_{n = 0}^{N} \sum_{j = 0}^{N - n} ⦋ (N - j - n) / x ⦌ B$
19		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ k / x ⦌ B$
20	19	nfel1	$⊢ Ⅎ x ⦋ k / x ⦌ B \in ℂ$
21		csbeq1a	$⊢ x = k \to B = ⦋ k / x ⦌ B$
22	21	eleq1d	$⊢ x = k \to (B \in ℂ \leftrightarrow ⦋ k / x ⦌ B \in ℂ)$
23	20 22	rspc	$⊢ k \in (0 \dots N - j) \to (\forall x \in (0 \dots N - j) B \in ℂ \to ⦋ k / x ⦌ B \in ℂ)$
24	10 23	mpan9	$⊢ ((φ \land j \in (0 \dots N)) \land k \in (0 \dots N - j)) \to ⦋ k / x ⦌ B \in ℂ$
25		csbeq1	$⊢ k = 0 + (N - j) - n \to ⦋ k / x ⦌ B = ⦋ (0 + (N - j) - n) / x ⦌ B$
26	24 25	fsumrev2	$⊢ (φ \land j \in (0 \dots N)) \to \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{n = 0}^{N - j} ⦋ (0 + (N - j) - n) / x ⦌ B$
27		elfz3nn0	$⊢ j \in (0 \dots N) \to N \in ℕ_{0}$
28	27	ad2antlr	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to N \in ℕ_{0}$
29		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
30	29	ad2antlr	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to j \in ℤ$
31		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
32		zcn	$⊢ j \in ℤ \to j \in ℂ$
33		subcl	$⊢ (N \in ℂ \land j \in ℂ) \to N - j \in ℂ$
34	31 32 33	syl2an	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to N - j \in ℂ$
35	28 30 34	syl2anc	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to N - j \in ℂ$
36		addid2	$⊢ N - j \in ℂ \to 0 + N - j = N - j$
37	35 36	syl	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to 0 + N - j = N - j$
38	37	oveq1d	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to 0 + (N - j) - n = N - j - n$
39	38	csbeq1d	$⊢ ((φ \land j \in (0 \dots N)) \land n \in (0 \dots N - j)) \to ⦋ (0 + (N - j) - n) / x ⦌ B = ⦋ (N - j - n) / x ⦌ B$
40	39	sumeq2dv	$⊢ (φ \land j \in (0 \dots N)) \to \sum_{n = 0}^{N - j} ⦋ (0 + (N - j) - n) / x ⦌ B = \sum_{n = 0}^{N - j} ⦋ (N - j - n) / x ⦌ B$
41	26 40	eqtrd	$⊢ (φ \land j \in (0 \dots N)) \to \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{n = 0}^{N - j} ⦋ (N - j - n) / x ⦌ B$
42	41	sumeq2dv	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{j = 0}^{N} \sum_{n = 0}^{N - j} ⦋ (N - j - n) / x ⦌ B$
43		elfz3nn0	$⊢ n \in (0 \dots N) \to N \in ℕ_{0}$
44	43	adantl	$⊢ (φ \land n \in (0 \dots N)) \to N \in ℕ_{0}$
45		addid2	$⊢ N \in ℂ \to 0 + N = N$
46	44 31 45	3syl	$⊢ (φ \land n \in (0 \dots N)) \to 0 + N = N$
47	46	oveq1d	$⊢ (φ \land n \in (0 \dots N)) \to 0 + N - n = N - n$
48	47	oveq2d	$⊢ (φ \land n \in (0 \dots N)) \to (0 \dots 0 + N - n) = (0 \dots N - n)$
49	47	oveq1d	$⊢ (φ \land n \in (0 \dots N)) \to (0 + N) - n - j = N - n - j$
50	49	adantr	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to (0 + N) - n - j = N - n - j$
51	43	ad2antlr	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to N \in ℕ_{0}$
52		elfzelz	$⊢ n \in (0 \dots N) \to n \in ℤ$
53	52	ad2antlr	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to n \in ℤ$
54		elfzelz	$⊢ j \in (0 \dots N - n) \to j \in ℤ$
55	54	adantl	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to j \in ℤ$
56		zcn	$⊢ n \in ℤ \to n \in ℂ$
57		sub32	$⊢ (N \in ℂ \land n \in ℂ \land j \in ℂ) \to N - n - j = N - j - n$
58	31 56 32 57	syl3an	$⊢ (N \in ℕ_{0} \land n \in ℤ \land j \in ℤ) \to N - n - j = N - j - n$
59	51 53 55 58	syl3anc	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to N - n - j = N - j - n$
60	50 59	eqtrd	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to (0 + N) - n - j = N - j - n$
61	60	csbeq1d	$⊢ ((φ \land n \in (0 \dots N)) \land j \in (0 \dots N - n)) \to ⦋ ((0 + N) - n - j) / x ⦌ B = ⦋ (N - j - n) / x ⦌ B$
62	48 61	sumeq12rdv	$⊢ (φ \land n \in (0 \dots N)) \to \sum_{j = 0}^{0 + N - n} ⦋ ((0 + N) - n - j) / x ⦌ B = \sum_{j = 0}^{N - n} ⦋ (N - j - n) / x ⦌ B$
63	62	sumeq2dv	$⊢ φ \to \sum_{n = 0}^{N} \sum_{j = 0}^{0 + N - n} ⦋ ((0 + N) - n - j) / x ⦌ B = \sum_{n = 0}^{N} \sum_{j = 0}^{N - n} ⦋ (N - j - n) / x ⦌ B$
64	18 42 63	3eqtr4d	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{n = 0}^{N} \sum_{j = 0}^{0 + N - n} ⦋ ((0 + N) - n - j) / x ⦌ B$
65		fzfid	$⊢ (φ \land k \in (0 \dots N)) \to (0 \dots k) \in Fin$
66		elfzuz3	$⊢ j \in (0 \dots k) \to k \in ℤ_{\geq j}$
67	66	adantl	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to k \in ℤ_{\geq j}$
68		elfzuz3	$⊢ k \in (0 \dots N) \to N \in ℤ_{\geq k}$
69	68	adantl	$⊢ (φ \land k \in (0 \dots N)) \to N \in ℤ_{\geq k}$
70	69	adantr	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to N \in ℤ_{\geq k}$
71		elfzuzb	$⊢ k \in (j \dots N) \leftrightarrow (k \in ℤ_{\geq j} \land N \in ℤ_{\geq k})$
72	67 70 71	sylanbrc	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to k \in (j \dots N)$
73		elfzelz	$⊢ j \in (0 \dots k) \to j \in ℤ$
74	73	adantl	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to j \in ℤ$
75		elfzel2	$⊢ k \in (0 \dots N) \to N \in ℤ$
76	75	ad2antlr	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to N \in ℤ$
77		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
78	77	ad2antlr	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to k \in ℤ$
79		fzsubel	$⊢ ((j \in ℤ \land N \in ℤ) \land (k \in ℤ \land j \in ℤ)) \to (k \in (j \dots N) \leftrightarrow k - j \in (j - j \dots N - j))$
80	74 76 78 74 79	syl22anc	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to (k \in (j \dots N) \leftrightarrow k - j \in (j - j \dots N - j))$
81	72 80	mpbid	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to k - j \in (j - j \dots N - j)$
82		subid	$⊢ j \in ℂ \to j - j = 0$
83	74 32 82	3syl	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to j - j = 0$
84	83	oveq1d	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to (j - j \dots N - j) = (0 \dots N - j)$
85	81 84	eleqtrd	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to k - j \in (0 \dots N - j)$
86		simpll	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to φ$
87		fzss2	$⊢ N \in ℤ_{\geq k} \to (0 \dots k) \subseteq (0 \dots N)$
88	69 87	syl	$⊢ (φ \land k \in (0 \dots N)) \to (0 \dots k) \subseteq (0 \dots N)$
89	88	sselda	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to j \in (0 \dots N)$
90	86 89 10	syl2anc	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to \forall x \in (0 \dots N - j) B \in ℂ$
91		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ (k - j) / x ⦌ B$
92	91	nfel1	$⊢ Ⅎ x ⦋ (k - j) / x ⦌ B \in ℂ$
93		csbeq1a	$⊢ x = k - j \to B = ⦋ (k - j) / x ⦌ B$
94	93	eleq1d	$⊢ x = k - j \to (B \in ℂ \leftrightarrow ⦋ (k - j) / x ⦌ B \in ℂ)$
95	92 94	rspc	$⊢ k - j \in (0 \dots N - j) \to (\forall x \in (0 \dots N - j) B \in ℂ \to ⦋ (k - j) / x ⦌ B \in ℂ)$
96	85 90 95	sylc	$⊢ ((φ \land k \in (0 \dots N)) \land j \in (0 \dots k)) \to ⦋ (k - j) / x ⦌ B \in ℂ$
97	65 96	fsumcl	$⊢ (φ \land k \in (0 \dots N)) \to \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B \in ℂ$
98		oveq2	$⊢ k = 0 + N - n \to (0 \dots k) = (0 \dots 0 + N - n)$
99		oveq1	$⊢ k = 0 + N - n \to k - j = (0 + N) - n - j$
100	99	csbeq1d	$⊢ k = 0 + N - n \to ⦋ (k - j) / x ⦌ B = ⦋ ((0 + N) - n - j) / x ⦌ B$
101	100	adantr	$⊢ (k = 0 + N - n \land j \in (0 \dots k)) \to ⦋ (k - j) / x ⦌ B = ⦋ ((0 + N) - n - j) / x ⦌ B$
102	98 101	sumeq12dv	$⊢ k = 0 + N - n \to \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B = \sum_{j = 0}^{0 + N - n} ⦋ ((0 + N) - n - j) / x ⦌ B$
103	97 102	fsumrev2	$⊢ φ \to \sum_{k = 0}^{N} \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B = \sum_{n = 0}^{N} \sum_{j = 0}^{0 + N - n} ⦋ ((0 + N) - n - j) / x ⦌ B$
104	64 103	eqtr4d	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{k = 0}^{N} \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B$
105		vex	$⊢ k \in V$
106	105 1	csbie	$⊢ ⦋ k / x ⦌ B = A$
107	106	a1i	$⊢ (j \in (0 \dots N) \land k \in (0 \dots N - j)) \to ⦋ k / x ⦌ B = A$
108	107	sumeq2dv	$⊢ j \in (0 \dots N) \to \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{k = 0}^{N - j} A$
109	108	sumeq2i	$⊢ \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} ⦋ k / x ⦌ B = \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} A$
110		ovex	$⊢ k - j \in V$
111	110 2	csbie	$⊢ ⦋ (k - j) / x ⦌ B = C$
112	111	a1i	$⊢ (k \in (0 \dots N) \land j \in (0 \dots k)) \to ⦋ (k - j) / x ⦌ B = C$
113	112	sumeq2dv	$⊢ k \in (0 \dots N) \to \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B = \sum_{j = 0}^{k} C$
114	113	sumeq2i	$⊢ \sum_{k = 0}^{N} \sum_{j = 0}^{k} ⦋ (k - j) / x ⦌ B = \sum_{k = 0}^{N} \sum_{j = 0}^{k} C$
115	104 109 114	3eqtr3g	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} A = \sum_{k = 0}^{N} \sum_{j = 0}^{k} C$

Metamath Proof Explorer

Theorem fsum0diag2

Proof