seqf1o - Metamath Proof Explorer

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

Theorem seqf1o 11319

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 2404	. . . 4
4	2, 3	fmptd 5852	. . 3
5		seqf1o.4	. . . . 5
6		oveq2 6048	. . . . . . . . . . 11
7		f1oeq23 5627	. . . . . . . . . . 11 $/\$
8	6, 6, 7	syl2anc 643	. . . . . . . . . 10
9	6	feq2d 5540	. . . . . . . . . 10
10	8, 9	anbi12d 692	. . . . . . . . 9 $/\$ $/\$
11		fveq2 5687	. . . . . . . . . 10
12		fveq2 5687	. . . . . . . . . 10
13	11, 12	eqeq12d 2418	. . . . . . . . 9
14	10, 13	imbi12d 312	. . . . . . . 8 $/\$ $/\$
15	14	2albidv 1634	. . . . . . 7 $/\$ $/\$
16	15	imbi2d 308	. . . . . 6 $/\$ $/\$
17		oveq2 6048	. . . . . . . . . . 11
18		f1oeq23 5627	. . . . . . . . . . 11 $/\$
19	17, 17, 18	syl2anc 643	. . . . . . . . . 10
20	17	feq2d 5540	. . . . . . . . . 10
21	19, 20	anbi12d 692	. . . . . . . . 9 $/\$ $/\$
22		fveq2 5687	. . . . . . . . . 10
23		fveq2 5687	. . . . . . . . . 10
24	22, 23	eqeq12d 2418	. . . . . . . . 9
25	21, 24	imbi12d 312	. . . . . . . 8 $/\$ $/\$
26	25	2albidv 1634	. . . . . . 7 $/\$ $/\$
27	26	imbi2d 308	. . . . . 6 $/\$ $/\$
28		oveq2 6048	. . . . . . . . . . 11
29		f1oeq23 5627	. . . . . . . . . . 11 $/\$
30	28, 28, 29	syl2anc 643	. . . . . . . . . 10
31	28	feq2d 5540	. . . . . . . . . 10
32	30, 31	anbi12d 692	. . . . . . . . 9 $/\$ $/\$
33		fveq2 5687	. . . . . . . . . 10
34		fveq2 5687	. . . . . . . . . 10
35	33, 34	eqeq12d 2418	. . . . . . . . 9
36	32, 35	imbi12d 312	. . . . . . . 8 $/\$ $/\$
37	36	2albidv 1634	. . . . . . 7 $/\$ $/\$
38	37	imbi2d 308	. . . . . 6 $/\$ $/\$
39		oveq2 6048	. . . . . . . . . . 11
40		f1oeq23 5627	. . . . . . . . . . 11 $/\$
41	39, 39, 40	syl2anc 643	. . . . . . . . . 10
42	39	feq2d 5540	. . . . . . . . . 10
43	41, 42	anbi12d 692	. . . . . . . . 9 $/\$ $/\$
44		fveq2 5687	. . . . . . . . . 10
45		fveq2 5687	. . . . . . . . . 10
46	44, 45	eqeq12d 2418	. . . . . . . . 9
47	43, 46	imbi12d 312	. . . . . . . 8 $/\$ $/\$
48	47	2albidv 1634	. . . . . . 7 $/\$ $/\$
49	48	imbi2d 308	. . . . . 6 $/\$ $/\$
50		f1of 5633	. . . . . . . . . . . . 13
51	50	adantr 452	. . . . . . . . . . . 12 $/\$
52		elfz3 11023	. . . . . . . . . . . 12
53		fvco3 5759	. . . . . . . . . . . 12 $/\$
54	51, 52, 53	syl2anr 465	. . . . . . . . . . 11 $/\$ $/\$
55		ffvelrn 5827	. . . . . . . . . . . . . . 15 $/\$
56	50, 52, 55	syl2anr 465	. . . . . . . . . . . . . 14 $/\$
57		fzsn 11050	. . . . . . . . . . . . . . . . 17
58	57	eleq2d 2471	. . . . . . . . . . . . . . . 16
59		elsni 3798	. . . . . . . . . . . . . . . 16
60	58, 59	syl6bi 220	. . . . . . . . . . . . . . 15
61	60	imp 419	. . . . . . . . . . . . . 14 $/\$
62	56, 61	syldan 457	. . . . . . . . . . . . 13 $/\$
63	62	adantrr 698	. . . . . . . . . . . 12 $/\$ $/\$
64	63	fveq2d 5691	. . . . . . . . . . 11 $/\$ $/\$
65	54, 64	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$
66		seq1 11291	. . . . . . . . . . 11
67	66	adantr 452	. . . . . . . . . 10 $/\$ $/\$
68		seq1 11291	. . . . . . . . . . 11
69	68	adantr 452	. . . . . . . . . 10 $/\$ $/\$
70	65, 67, 69	3eqtr4d 2446	. . . . . . . . 9 $/\$ $/\$
71	70	ex 424	. . . . . . . 8 $/\$
72	71	alrimivv 1639	. . . . . . 7 $/\$
73	72	a1d 23	. . . . . 6 $/\$
74		f1oeq1 5624	. . . . . . . . . . . 12
75		feq1 5535	. . . . . . . . . . . 12
76	74, 75	bi2anan9r 845	. . . . . . . . . . 11 $/\$ $/\$ $/\$
77		coeq1 4989	. . . . . . . . . . . . . . 15
78		coeq2 4990	. . . . . . . . . . . . . . 15
79	77, 78	sylan9eq 2456	. . . . . . . . . . . . . 14 $/\$
80	79	seqeq3d 11286	. . . . . . . . . . . . 13 $/\$
81	80	fveq1d 5689	. . . . . . . . . . . 12 $/\$
82		simpl 444	. . . . . . . . . . . . . 14 $/\$
83	82	seqeq3d 11286	. . . . . . . . . . . . 13 $/\$
84	83	fveq1d 5689	. . . . . . . . . . . 12 $/\$
85	81, 84	eqeq12d 2418	. . . . . . . . . . 11 $/\$
86	76, 85	imbi12d 312	. . . . . . . . . 10 $/\$ $/\$ $/\$
87	86	cbval2v 2056	. . . . . . . . 9 $/\$ $/\$
88		simplll 735	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
89		seqf1o.1	. . . . . . . . . . . . . . 15 $/\$ $/\$
90	88, 89	sylan 458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91		seqf1o.2	. . . . . . . . . . . . . . 15 $/\$ $/\$
92	88, 91	sylan 458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
93		seqf1o.3	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	88, 93	sylan 458	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simpllr 736	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
96		seqf1o.5	. . . . . . . . . . . . . . 15
97	88, 96	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
98		simprl 733	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
99		simprr 734	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
100		eqid 2404	. . . . . . . . . . . . . 14
101		eqid 2404	. . . . . . . . . . . . . 14
102		simplr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102, 87	sylib 189	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	90, 92, 94, 95, 97, 98, 99, 100, 101, 103	seqf1olem2 11318	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
105	104	exp31 588	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
106	87, 105	syl5bir 210	. . . . . . . . . . 11 $/\$ $/\$ $/\$
107	106	alrimdv 1640	. . . . . . . . . 10 $/\$ $/\$ $/\$
108	107	alrimdv 1640	. . . . . . . . 9 $/\$ $/\$ $/\$
109	87, 108	syl5bi 209	. . . . . . . 8 $/\$ $/\$ $/\$
110	109	expcom 425	. . . . . . 7 $/\$ $/\$
111	110	a2d 24	. . . . . 6 $/\$ $/\$
112	16, 27, 38, 49, 73, 111	uzind4 10490	. . . . 5 $/\$
113	5, 112	mpcom 34	. . . 4 $/\$
114		fvex 5701	. . . . . . 7
115	114, 3	fnmpti 5532	. . . . . 6
116		fzfi 11266	. . . . . 6
117		fnfi 7343	. . . . . 6 $/\$
118	115, 116, 117	mp2an 654	. . . . 5
119		f1of 5633	. . . . . . 7
120	1, 119	syl 16	. . . . . 6
121		ovex 6065	. . . . . . 7
122	121	a1i 11	. . . . . 6
123		fex2 5562	. . . . . 6 $/\$ $/\$
124	120, 122, 122, 123	syl3anc 1184	. . . . 5
125		f1oeq1 5624	. . . . . . . 8
126		feq1 5535	. . . . . . . 8
127	125, 126	bi2anan9r 845	. . . . . . 7 $/\$ $/\$ $/\$
128		coeq1 4989	. . . . . . . . . . 11
129		coeq2 4990	. . . . . . . . . . 11
130	128, 129	sylan9eq 2456	. . . . . . . . . 10 $/\$
131	130	seqeq3d 11286	. . . . . . . . 9 $/\$
132	131	fveq1d 5689	. . . . . . . 8 $/\$
133		simpl 444	. . . . . . . . . 10 $/\$
134	133	seqeq3d 11286	. . . . . . . . 9 $/\$
135	134	fveq1d 5689	. . . . . . . 8 $/\$
136	132, 135	eqeq12d 2418	. . . . . . 7 $/\$
137	127, 136	imbi12d 312	. . . . . 6 $/\$ $/\$ $/\$
138	137	spc2gv 2999	. . . . 5 $/\$ $/\$ $/\$
139	118, 124, 138	sylancr 645	. . . 4 $/\$ $/\$
140	113, 139	mpd 15	. . 3 $/\$
141	1, 4, 140	mp2and 661	. 2
142	120	ffvelrnda 5829	. . . . 5 $/\$
143		fveq2 5687	. . . . . 6
144		fvex 5701	. . . . . 6
145	143, 3, 144	fvmpt 5765	. . . . 5
146	142, 145	syl 16	. . . 4 $/\$
147		fvco3 5759	. . . . 5 $/\$
148	120, 147	sylan 458	. . . 4 $/\$
149		seqf1o.8	. . . 4 $/\$
150	146, 148, 149	3eqtr4d 2446	. . 3 $/\$
151	5, 150	seqfveq 11302	. 2
152		fveq2 5687	. . . . 5
153		fvex 5701	. . . . 5
154	152, 3, 153	fvmpt 5765	. . . 4
155	154	adantl 453	. . 3 $/\$
156	5, 155	seqfveq 11302	. 2
157	141, 151, 156	3eqtr3d 2444	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wal 1546

wceq 1649

wcel 1721

cvv 2916

wss 3280

cif 3699

csn 3774 class class class wbr 4172

cmpt 4226

ccnv 4836

ccom 4841

wfn 5408

wf 5409

wf1o 5412

cfv 5413 (class class class)co 6040

cfn 7068

c1 8947

caddc 8949

clt 9076

cz 10238

cuz 10444

cfz 10999

cseq 11278

This theorem is referenced by: summolem3 12463 eulerthlem2 13126 gsumval3eu 15468 gsumval3 15469 prodmolem3 25212

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-fzo 11091 df-seq 11279

W3C validator