Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem fsum0diag2 7194

Description: Two ways to express "the sum of where ."

Assertion

Ref	Expression
fsum0diag2

Distinct variable groups:   ,   ,   ,,

---

Proof of Theorem fsum0diag2

Step	Hyp	Ref	Expression
1		fsum0diag 7193	. 2
2		fsumrev 6967	. . . . . . . . . 10
3		elfzuzt 6420	. . . . . . . . . . 11
4	3	adantl 388	. . . . . . . . . 10
5		elfzelz 6414	. . . . . . . . . . 11
6	5	adantl 388	. . . . . . . . . 10
7		elfzuz3t 6410	. . . . . . . . . . . . . . . . . . 19
8		0z 6093	. . . . . . . . . . . . . . . . . . . 20
9		fzss2t 6436	. . . . . . . . . . . . . . . . . . . 20
10	8, 9	mpan2 694	. . . . . . . . . . . . . . . . . . 19
11	7, 10	syl 10	. . . . . . . . . . . . . . . . . 18
12	11	sseld 2057	. . . . . . . . . . . . . . . . 17
13	12	imim1d 28	. . . . . . . . . . . . . . . 16
14	13	adantr 389	. . . . . . . . . . . . . . 15
15		axmulcl 5245	. . . . . . . . . . . . . . . . . . 19
16		ra4csbela 2032	. . . . . . . . . . . . . . . . . . . . 21
17	11	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22
18		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . 24
19		fznn0sub2t 6431	. . . . . . . . . . . . . . . . . . . . . . . 24
20	18, 19	mpan 693	. . . . . . . . . . . . . . . . . . . . . . 23
21	20	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22
22	17, 21	sseldd 2058	. . . . . . . . . . . . . . . . . . . . 21
23	16, 22	sylan 448	. . . . . . . . . . . . . . . . . . . 20
24	23	an1rs 488	. . . . . . . . . . . . . . . . . . 19
25	15, 24	sylan2 451	. . . . . . . . . . . . . . . . . 18
26	25	exp32 377	. . . . . . . . . . . . . . . . 17
27	26	com3l 34	. . . . . . . . . . . . . . . 16
28	27	a2d 13	. . . . . . . . . . . . . . 15
29	14, 28	syld 27	. . . . . . . . . . . . . 14
30	29	r19.20dv2 1703	. . . . . . . . . . . . 13
31	30	exp31 376	. . . . . . . . . . . 12
32	31	com24 37	. . . . . . . . . . 11
33	32	imp42 369	. . . . . . . . . 10
34	2, 4, 6, 33	syl3anc 856	. . . . . . . . 9
35		zcnt 6087	. . . . . . . . . . . . . 14
36	5, 35	syl 10	. . . . . . . . . . . . 13
37		subidt 5367	. . . . . . . . . . . . . 14
38		subid1t 5368	. . . . . . . . . . . . . 14
39	37, 38	opreq12d 3963	. . . . . . . . . . . . 13
40	36, 39	syl 10	. . . . . . . . . . . 12
41	40	adantl 388	. . . . . . . . . . 11
42		nncant 5441	. . . . . . . . . . . . . . . 16
43	18	elfzel2 6411	. . . . . . . . . . . . . . . . 17
44	43, 35	syl 10	. . . . . . . . . . . . . . . 16
45		elfzelz 6414	. . . . . . . . . . . . . . . . 17
46		zcnt 6087	. . . . . . . . . . . . . . . . 17
47	45, 46	syl 10	. . . . . . . . . . . . . . . 16
48	42, 44, 47	sylanc 471	. . . . . . . . . . . . . . 15
49	48	csbeq1d 1994	. . . . . . . . . . . . . 14
50	49	opreq2d 3961	. . . . . . . . . . . . 13