Theorem fsum 15806

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 15774	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		fvex 6891	. . 3 ⊢ (seq1( + , 𝐺)‘𝑀) ∈ V
3		eleq1w 2843	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
4		csbeq1 3850	. . . . . . . . . 10 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
5	3, 4	ifbieq1d 4507	. . . . . . . . 9 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
6	5	cbvmptv 5209	. . . . . . . 8 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
7		fsum.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
8	7	ralrimiva 3154	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
9		nfcsb1v 3871	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
10	9	nfel1 2938	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
11		csbeq1a 3861	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
12	11	eleq1d 2845	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
13	10, 12	rspc 3564	. . . . . . . . 9 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
14	8, 13	mpan9 516	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
15		fveq2 6878	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
16	15	csbeq1d 3851	. . . . . . . . . 10 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
17		csbcow 3862	. . . . . . . . . 10 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
18	16, 17	eqtr4di 2813	. . . . . . . . 9 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
19	18	cbvmptv 5209	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑖 ∈ ℕ ↦ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
20	6, 14, 19	summo 15803	. . . . . . 7 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
21		fsum.2	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
22		fsum.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
23		f1of 6817	. . . . . . . . . . . 12 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
24	22, 23	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
25		ovex 7446	. . . . . . . . . . 11 ⊢ (1...𝑀) ∈ V
26		fex 7225	. . . . . . . . . . 11 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
27	24, 25, 26	sylancl 598	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ V)
28		nnuz 12926	. . . . . . . . . . . . 13 ⊢ ℕ = (ℤ≥‘1)
29	21, 28	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘1))
30		fsum.5	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)
31		elfznn 13608	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
32		fvex 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺‘𝑛) ∈ V
33	30, 32	eqeltrrdi 2869	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ V)
34		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ 𝐶) = (𝑛 ∈ ℕ ↦ 𝐶)
35	34	fvmpt2 6998	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝐶 ∈ V) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
36	31, 33, 35	syl2an2 699	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
37	30, 36	eqtr4d 2798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
38	37	ralrimiva 3154	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
39		nffvmpt1 6889	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
40	39	nfeq2 2939	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
41		fveq2 6878	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
42		fveq2 6878	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑘 → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
43	41, 42	eqeq12d 2776	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) ↔ (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
44	40, 43	rspc 3564	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
45	38, 44	mpan9 516	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
46	29, 45	seqfveq 14090	. . . . . . . . . . 11 ⊢ (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
47	22, 46	jca 521	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
48		f1oeq1 6805	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
49		fveq1 6877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
50	49	csbeq1d 3851	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
51		fvex 6891	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑛) ∈ V
52		fsum.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
53	51, 52	csbie 3882	. . . . . . . . . . . . . . . 16 ⊢ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶
54	50, 53	eqtrdi 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
55	54	mpteq2dv 5199	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ 𝐶))
56	55	seqeq3d 14073	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ 𝐶)))
57	56	fveq1d 6880	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
58	57	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
59	48, 58	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))))
60	27, 47, 59	spcedv 3552	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))
61		oveq2 7421	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
62	61	f1oeq2d 6813	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
63		fveq2 6878	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))
64	63	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))
65	62, 64	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))))
66	65	exbidv 1954	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))))
67	66	rspcev 3576	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
68	21, 60, 67	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
69	68	olcd 888	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
70		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)))
71	70	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
72	71	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
73		eqeq1 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))
74	73	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
75	74	exbidv 1954	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
76	75	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
77	72, 76	orbi12d 932	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
78	77	moi2 3674	. . . . . . . . . 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 713	. . . . . . . . 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 663	. . . . . . . 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 462	. . . . . . 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 596	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → 𝑥 = (seq1( + , 𝐺)‘𝑀)))
83	69, 77	syl5ibrcom 250	. . . . . 6 ⊢ (𝜑 → (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))))
84	82, 83	impbid 215	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
85	84	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
86	85	iota5 6516	. . 3 ⊢ ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
87	2, 86	mpan2 704	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
88	1, 87	eqtrid 2807	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2562  ∀wral 3076  ∃wrex 3086  Vcvv 3450  ⦋csb 3847   ⊆ wss 3899  ifcif 4482   class class class wbr 5103   ↦ cmpt 5186  ℩cio 6487  ⟶wf 6529  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7413  ℂcc 11122  0cc0 11124  1c1 11125   + caddc 11127  ℕcn 12257  ℤcz 12615  ℤ_≥cuz 12887  ...cfz 13561  seqcseq 14065   ⇝ cli 15571  Σcsu 15773

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-inf2 9620  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-fin 8956  df-sup 9412  df-oi 9482  df-card 9944  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-div 11896  df-nn 12258  df-2 12327  df-3 12328  df-n0 12529  df-z 12616  df-uz 12888  df-rp 13043  df-fz 13562  df-fzo 13710  df-seq 14066  df-exp 14126  df-hash 14395  df-cj 15186  df-re 15187  df-im 15188  df-sqrt 15322  df-abs 15323  df-clim 15575  df-sum 15774

This theorem is used by:  sumz  15808  fsumf1o  15809  fsumcl2lem  15817  fsumadd  15826  sumsnf  15829  fsummulc2  15870  fsumconst  15876  fsumrelem  15894  gsumfsum  21647  sumsnd  45860