Theorem fsum 15627

Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)

Hypotheses

Ref	Expression
fsum.1	⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
fsum.2	⊢ (𝜑 → 𝑀 ∈ ℕ)
fsum.3	⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
fsum.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
fsum.5	⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)

Assertion

Ref	Expression
fsum	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))

Distinct variable groups:   𝐵,𝑛   𝐶,𝑘   𝑘,𝑛,𝐹   𝜑,𝑘,𝑛   𝐴,𝑘,𝑛   𝑘,𝐺,𝑛   𝑘,𝑀,𝑛

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑛)

Proof of Theorem fsum

Dummy variables 𝑓 𝑖 𝑗 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sum 15594	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		fvex 6835	. . 3 ⊢ (seq1( + , 𝐺)‘𝑀) ∈ V
3		eleq1w 2814	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
4		csbeq1 3848	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
5	3, 4	ifbieq1d 4497	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
6	5	cbvmptv 5193	. . . . . . . 8 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
7		fsum.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
8	7	ralrimiva 3124	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
9		nfcsb1v 3869	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
10	9	nfel1 2911	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
11		csbeq1a 3859	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
12	11	eleq1d 2816	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
13	10, 12	rspc 3560	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
14	8, 13	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
15		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
16	15	csbeq1d 3849	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
17		csbcow 3860	. . . . . . . . . 10 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
18	16, 17	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
19	18	cbvmptv 5193	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑖 ∈ ℕ ↦ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
20	6, 14, 19	summo 15624	. . . . . . 7 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
21		fsum.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
22		fsum.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
23		f1of 6763	. . . . . . . . . . . 12 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
24	22, 23	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
25		ovex 7379	. . . . . . . . . . 11 ⊢ (1...𝑀) ∈ V
26		fex 7160	. . . . . . . . . . 11 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
27	24, 25, 26	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ V)
28		nnuz 12775	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
29	21, 28	eleqtrdi 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
30		fsum.5	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)
31		elfznn 13453	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
32		fvex 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘𝑛) ∈ V
33	30, 32	eqeltrrdi 2840	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ V)
34		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ 𝐶) = (𝑛 ∈ ℕ ↦ 𝐶)
35	34	fvmpt2 6940	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝐶 ∈ V) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
36	31, 33, 35	syl2an2 686	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
37	30, 36	eqtr4d 2769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
38	37	ralrimiva 3124	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
39		nffvmpt1 6833	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
40	39	nfeq2 2912	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
41		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
42		fveq2 6822	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
43	41, 42	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) ↔ (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
44	40, 43	rspc 3560	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
45	38, 44	mpan9 506	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
46	29, 45	seqfveq 13933	. . . . . . . . . . 11 ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
47	22, 46	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
48		f1oeq1 6751	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
49		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
50	49	csbeq1d 3849	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
51		fvex 6835	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑛) ∈ V
52		fsum.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
53	51, 52	csbie 3880	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶
54	50, 53	eqtrdi 2782	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
55	54	mpteq2dv 5183	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ 𝐶))
56	55	seqeq3d 13916	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ 𝐶)))
57	56	fveq1d 6824	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
58	57	eqeq2d 2742	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
59	48, 58	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))))
60	27, 47, 59	spcedv 3548	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))
61		oveq2 7354	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
62	61	f1oeq2d 6759	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
63		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))
64	63	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))
65	62, 64	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))))
66	65	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))))
67	66	rspcev 3572	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
68	21, 60, 67	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
69	68	olcd 874	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
70		breq2 5093	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)))
71	70	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
72	71	rexbidv 3156	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
73		eqeq1 2735	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
74	73	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
75	74	exbidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
76	75	rexbidv 3156	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
77	72, 76	orbi12d 918	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
78	77	moi2 3670	. . . . . . . . . 10 ⊢ ((((seq1( + , 𝐺)‘𝑀) ∈ V ∧ ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
79	2, 78	mpanl1 700	. . . . . . . . 9 ⊢ ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
80	79	ancom2s 650	. . . . . . . 8 ⊢ ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
81	80	expr 456	. . . . . . 7 ⊢ ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → 𝑥 = (seq1( + , 𝐺)‘𝑀)))
82	20, 69, 81	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → 𝑥 = (seq1( + , 𝐺)‘𝑀)))
83	69, 77	syl5ibrcom 247	. . . . . 6 ⊢ (𝜑 → (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
84	82, 83	impbid 212	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
85	84	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
86	85	iota5 6464	. . 3 ⊢ ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
87	2, 86	mpan2 691	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
88	1, 87	eqtrid 2778	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∃*wmo 2533  ∀wral 3047  ∃wrex 3056  Vcvv 3436  ⦋csb 3845   ⊆ wss 3897  ifcif 4472   class class class wbr 5089   ↦ cmpt 5170  ℩cio 6435  ⟶wf 6477  –1-1-onto→wf1o 6480  ‘cfv 6481  (class class class)co 7346  ℂcc 11004  0cc0 11006  1c1 11007   + caddc 11009  ℕcn 12125  ℤcz 12468  ℤ_≥cuz 12732  ...cfz 13407  seqcseq 13908   ⇝ cli 15391  Σcsu 15593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-inf2 9531  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-int 4896  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-se 5568  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-1st 7921  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-sup 9326  df-oi 9396  df-card 9832  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-n0 12382  df-z 12469  df-uz 12733  df-rp 12891  df-fz 13408  df-fzo 13555  df-seq 13909  df-exp 13969  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-sum 15594

This theorem is referenced by:  sumz  15629  fsumf1o  15630  fsumcl2lem  15638  fsumadd  15647  sumsnf  15650  fsummulc2  15691  fsumconst  15697  fsumrelem  15714  gsumfsum  21371  sumsnd  45071