seqf1o - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > seqf1o		Structured version Unicode version

Theorem seqf1o 12116

Description: Rearrange a sum via an arbitrary bijection on

. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.)

**Hypotheses**
Ref	Expression
seqf1o.1	$/\$ $/\$
seqf1o.2	$/\$ $/\$
seqf1o.3	$/\$ $/\$ $/\$
seqf1o.4
seqf1o.5
seqf1o.6
seqf1o.7	$/\$
seqf1o.8	$/\$

**Assertion**
Ref	Expression
seqf1o

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem seqf1o Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		seqf1o.6	. . 3
2		seqf1o.7	. . . 4 $/\$
3		eqid 2467	. . . 4
4	2, 3	fmptd 6045	. . 3
5		seqf1o.4	. . . . 5
6		oveq2 6292	. . . . . . . . . . 11
7		f1oeq23 5810	. . . . . . . . . . 11 $/\$
8	6, 6, 7	syl2anc 661	. . . . . . . . . 10
9	6	feq2d 5718	. . . . . . . . . 10
10	8, 9	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
11		fveq2 5866	. . . . . . . . . 10
12		fveq2 5866	. . . . . . . . . 10
13	11, 12	eqeq12d 2489	. . . . . . . . 9
14	10, 13	imbi12d 320	. . . . . . . 8 $/\$ $/\$
15	14	2albidv 1691	. . . . . . 7 $/\$ $/\$
16	15	imbi2d 316	. . . . . 6 $/\$ $/\$
17		oveq2 6292	. . . . . . . . . . 11
18		f1oeq23 5810	. . . . . . . . . . 11 $/\$
19	17, 17, 18	syl2anc 661	. . . . . . . . . 10
20	17	feq2d 5718	. . . . . . . . . 10
21	19, 20	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
22		fveq2 5866	. . . . . . . . . 10
23		fveq2 5866	. . . . . . . . . 10
24	22, 23	eqeq12d 2489	. . . . . . . . 9
25	21, 24	imbi12d 320	. . . . . . . 8 $/\$ $/\$
26	25	2albidv 1691	. . . . . . 7 $/\$ $/\$
27	26	imbi2d 316	. . . . . 6 $/\$ $/\$
28		oveq2 6292	. . . . . . . . . . 11
29		f1oeq23 5810	. . . . . . . . . . 11 $/\$
30	28, 28, 29	syl2anc 661	. . . . . . . . . 10
31	28	feq2d 5718	. . . . . . . . . 10
32	30, 31	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
33		fveq2 5866	. . . . . . . . . 10
34		fveq2 5866	. . . . . . . . . 10
35	33, 34	eqeq12d 2489	. . . . . . . . 9
36	32, 35	imbi12d 320	. . . . . . . 8 $/\$ $/\$
37	36	2albidv 1691	. . . . . . 7 $/\$ $/\$
38	37	imbi2d 316	. . . . . 6 $/\$ $/\$
39		oveq2 6292	. . . . . . . . . . 11
40		f1oeq23 5810	. . . . . . . . . . 11 $/\$
41	39, 39, 40	syl2anc 661	. . . . . . . . . 10
42	39	feq2d 5718	. . . . . . . . . 10
43	41, 42	anbi12d 710	. . . . . . . . 9 $/\$ $/\$
44		fveq2 5866	. . . . . . . . . 10
45		fveq2 5866	. . . . . . . . . 10
46	44, 45	eqeq12d 2489	. . . . . . . . 9
47	43, 46	imbi12d 320	. . . . . . . 8 $/\$ $/\$
48	47	2albidv 1691	. . . . . . 7 $/\$ $/\$
49	48	imbi2d 316	. . . . . 6 $/\$ $/\$
50		f1of 5816	. . . . . . . . . . . . 13
51	50	adantr 465	. . . . . . . . . . . 12 $/\$
52		elfz3 11696	. . . . . . . . . . . 12
53		fvco3 5944	. . . . . . . . . . . 12 $/\$
54	51, 52, 53	syl2anr 478	. . . . . . . . . . 11 $/\$ $/\$
55		ffvelrn 6019	. . . . . . . . . . . . . . 15 $/\$
56	50, 52, 55	syl2anr 478	. . . . . . . . . . . . . 14 $/\$
57		fzsn 11725	. . . . . . . . . . . . . . . . 17
58	57	eleq2d 2537	. . . . . . . . . . . . . . . 16
59		elsni 4052	. . . . . . . . . . . . . . . 16
60	58, 59	syl6bi 228	. . . . . . . . . . . . . . 15
61	60	imp 429	. . . . . . . . . . . . . 14 $/\$
62	56, 61	syldan 470	. . . . . . . . . . . . 13 $/\$
63	62	adantrr 716	. . . . . . . . . . . 12 $/\$ $/\$
64	63	fveq2d 5870	. . . . . . . . . . 11 $/\$ $/\$
65	54, 64	eqtrd 2508	. . . . . . . . . 10 $/\$ $/\$
66		seq1 12088	. . . . . . . . . . 11
67	66	adantr 465	. . . . . . . . . 10 $/\$ $/\$
68		seq1 12088	. . . . . . . . . . 11
69	68	adantr 465	. . . . . . . . . 10 $/\$ $/\$
70	65, 67, 69	3eqtr4d 2518	. . . . . . . . 9 $/\$ $/\$
71	70	ex 434	. . . . . . . 8 $/\$
72	71	alrimivv 1696	. . . . . . 7 $/\$
73	72	a1d 25	. . . . . 6 $/\$
74		f1oeq1 5807	. . . . . . . . . . . 12
75		feq1 5713	. . . . . . . . . . . 12
76	74, 75	bi2anan9r 872	. . . . . . . . . . 11 $/\$ $/\$ $/\$
77		coeq1 5160	. . . . . . . . . . . . . . 15
78		coeq2 5161	. . . . . . . . . . . . . . 15
79	77, 78	sylan9eq 2528	. . . . . . . . . . . . . 14 $/\$
80	79	seqeq3d 12083	. . . . . . . . . . . . 13 $/\$
81	80	fveq1d 5868	. . . . . . . . . . . 12 $/\$
82		simpl 457	. . . . . . . . . . . . . 14 $/\$
83	82	seqeq3d 12083	. . . . . . . . . . . . 13 $/\$
84	83	fveq1d 5868	. . . . . . . . . . . 12 $/\$
85	81, 84	eqeq12d 2489	. . . . . . . . . . 11 $/\$
86	76, 85	imbi12d 320	. . . . . . . . . 10 $/\$ $/\$ $/\$
87	86	cbval2v 2003	. . . . . . . . 9 $/\$ $/\$
88		simplll 757	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
89		seqf1o.1	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	88, 89	sylan 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		seqf1o.2	. . . . . . . . . . . . . . 15 $/\$ $/\$
92	88, 91	sylan 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		seqf1o.3	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	88, 93	sylan 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simpllr 758	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
96		seqf1o.5	. . . . . . . . . . . . . . 15
97	88, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
98		simprl 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
99		simprr 756	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100		eqid 2467	. . . . . . . . . . . . . 14
101		eqid 2467	. . . . . . . . . . . . . 14
102		simplr 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102, 87	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 92, 94, 95, 97, 98, 99, 100, 101, 103	seqf1olem2 12115	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	exp31 604	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
106	87, 105	syl5bir 218	. . . . . . . . . . 11 $/\$ $/\$ $/\$
107	106	alrimdv 1697	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	107	alrimdv 1697	. . . . . . . . 9 $/\$ $/\$ $/\$
109	87, 108	syl5bi 217	. . . . . . . 8 $/\$ $/\$ $/\$
110	109	expcom 435	. . . . . . 7 $/\$ $/\$
111	110	a2d 26	. . . . . 6 $/\$ $/\$
112	16, 27, 38, 49, 73, 111	uzind4 11139	. . . . 5 $/\$
113	5, 112	mpcom 36	. . . 4 $/\$
114		fvex 5876	. . . . . . 7
115	114, 3	fnmpti 5709	. . . . . 6
116		fzfi 12050	. . . . . 6
117		fnfi 7798	. . . . . 6 $/\$
118	115, 116, 117	mp2an 672	. . . . 5
119		f1of 5816	. . . . . . 7
120	1, 119	syl 16	. . . . . 6
121		ovex 6309	. . . . . . 7
122	121	a1i 11	. . . . . 6
123		fex2 6739	. . . . . 6 $/\$ $/\$
124	120, 122, 122, 123	syl3anc 1228	. . . . 5
125		f1oeq1 5807	. . . . . . . 8
126		feq1 5713	. . . . . . . 8
127	125, 126	bi2anan9r 872	. . . . . . 7 $/\$ $/\$ $/\$
128		coeq1 5160	. . . . . . . . . . 11
129		coeq2 5161	. . . . . . . . . . 11
130	128, 129	sylan9eq 2528	. . . . . . . . . 10 $/\$
131	130	seqeq3d 12083	. . . . . . . . 9 $/\$
132	131	fveq1d 5868	. . . . . . . 8 $/\$
133		simpl 457	. . . . . . . . . 10 $/\$
134	133	seqeq3d 12083	. . . . . . . . 9 $/\$
135	134	fveq1d 5868	. . . . . . . 8 $/\$
136	132, 135	eqeq12d 2489	. . . . . . 7 $/\$
137	127, 136	imbi12d 320	. . . . . 6 $/\$ $/\$ $/\$
138	137	spc2gv 3201	. . . . 5 $/\$ $/\$ $/\$
139	118, 124, 138	sylancr 663	. . . 4 $/\$ $/\$
140	113, 139	mpd 15	. . 3 $/\$
141	1, 4, 140	mp2and 679	. 2
142	120	ffvelrnda 6021	. . . . 5 $/\$
143		fveq2 5866	. . . . . 6
144		fvex 5876	. . . . . 6
145	143, 3, 144	fvmpt 5950	. . . . 5
146	142, 145	syl 16	. . . 4 $/\$
147		fvco3 5944	. . . . 5 $/\$
148	120, 147	sylan 471	. . . 4 $/\$
149		seqf1o.8	. . . 4 $/\$
150	146, 148, 149	3eqtr4d 2518	. . 3 $/\$
151	5, 150	seqfveq 12099	. 2
152		fveq2 5866	. . . . 5
153		fvex 5876	. . . . 5
154	152, 3, 153	fvmpt 5950	. . . 4
155	154	adantl 466	. . 3 $/\$
156	5, 155	seqfveq 12099	. 2
157	141, 151, 156	3eqtr3d 2516	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wal 1377

wceq 1379

wcel 1767

cvv 3113

wss 3476

cif 3939

csn 4027 class class class wbr 4447

cmpt 4505

ccnv 4998

ccom 5003

wfn 5583

wf 5584

wf1o 5587

cfv 5588 (class class class)co 6284

cfn 7516

c1 9493

caddc 9495

clt 9628

cz 10864

cuz 11082

cfz 11672

cseq 12075

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-fin 7520 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-nn 10537 df-n0 10796 df-z 10865 df-uz 11083 df-fz 11673 df-fzo 11793 df-seq 12076

This theorem is referenced by: summolem3 13499 eulerthlem2 14171 gsumval3eu 16710 gsumval3OLD 16711 gsumval3 16714 prodmolem3 28670

W3C validator