fsum3 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > fsum3		GIF version

Theorem fsum3 11530

Description: The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)

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

**Assertion**
Ref	Expression
fsum3	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))

Distinct variable groups: 𝐴,𝑘,𝑛 𝐵,𝑛 𝐶,𝑘 𝑘,𝐹,𝑛 𝑘,𝐺,𝑛 𝑘,𝑀,𝑛 𝜑,𝑘,𝑛 Allowed substitution hints: 𝐵(𝑘) 𝐶(𝑛)

Proof of Theorem fsum3 Dummy variables 𝑓 𝑖 𝑗 𝑚 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sumdc 11497	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
2		nnuz 9628	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9344	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		elnnuz 9629	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈ (ℤ_≥‘1))
5	2	eqimss2i 3236	. . . . . . . . . 10 ⊢ (ℤ_≥‘1) ⊆ ℕ
6	5	sseli 3175	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℕ)
7	6	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℕ)
8		fveq2 5554	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑥 → (𝐺‘𝑛) = (𝐺‘𝑥))
9	8	eleq1d 2262	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑥) ∈ ℂ))
10		fsum.1	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶)
11		fsum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℕ)
12		fsum.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴)
13		fsum.4	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
14		fsum.5	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶)
15	10, 11, 12, 13, 14	fsumgcl 11529	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
16	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
17		1zzd 9344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ∈ ℤ)
18	11	nnzd 9438	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑀 ∈ ℤ)
20		eluzelz 9601	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℤ)
21	20	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ ℤ)
22	17, 19, 21	3jca 1179	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ))
23		eluzle 9604	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 1 ≤ 𝑥)
24	23	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ≤ 𝑥)
25		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ≤ 𝑀)
26	24, 25	jca 306	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀))
27		elfz2 10081	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀)))
28	22, 26, 27	sylanbrc 417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ (1...𝑀))
29	9, 16, 28	rspcdva 2869	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (𝐺‘𝑥) ∈ ℂ)
30		0cnd 8012	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑥 ≤ 𝑀) → 0 ∈ ℂ)
31	7	nnzd 9438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℤ)
32	18	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑀 ∈ ℤ)
33		zdcle 9393	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑥 ≤ 𝑀)
34	31, 32, 33	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → DECID 𝑥 ≤ 𝑀)
35	29, 30, 34	ifcldadc 3586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ)
36		breq1 4032	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑀 ↔ 𝑥 ≤ 𝑀))
37	36, 8	ifbieq1d 3579	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
38		eqid 2193	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))
39	37, 38	fvmptg 5633	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
40	7, 35, 39	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
41	40, 35	eqeltrd 2270	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
42	4, 41	sylan2b 287	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
43	2, 3, 42	serf 10554	. . . 4 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))):ℕ⟶ℂ)
44	43, 11	ffvelcdmd 5694	. . 3 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ)
45	44	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ)
46		eleq1w 2254	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47		csbeq1 3083	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
48	46, 47	ifbieq1d 3579	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
49	48	cbvmptv 4125	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
50	13	ralrimiva 2567	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
51		nfcsb1v 3113	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
52	51	nfel1 2347	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
53		csbeq1a 3089	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
54	53	eleq1d 2262	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
55	52, 54	rspc 2858	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
56	50, 55	mpan9 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
57		breq1 4032	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
58		fveq2 5554	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
59	58	csbeq1d 3087	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
60		csbco 3090	. . . . . . . . . . . . . 14 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
61	59, 60	eqtr4di 2244	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
62	57, 61	ifbieq1d 3579	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
63	62	cbvmptv 4125	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
64	49, 56, 63, 63	summodc 11526	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
65		eleq1w 2254	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑗 → (𝑢 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
66	65	dcbid 839	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑗 → (DECID 𝑢 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
67	66	cbvralv 2726	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
68	67	3anbi2i 1193	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
69	68	rexbii 2501	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
70		1zzd 9344	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℤ)
71		nnz 9336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
72	70, 71	fzfigd 10502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ → (1...𝑚) ∈ Fin)
73		fihasheqf1oi 10858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
74	72, 73	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
75		nnnn0 9247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
76	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ₀)
77		hashfz1 10854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
79	74, 78	eqtr3d 2228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘𝐴) = 𝑚)
80	79	breq2d 4041	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
81	80	ifbid 3578	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
82	81	mpteq2dv 4120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
83	82	seqeq3d 10526	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
84	83	fveq1d 5556	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
85	84	eqeq2d 2205	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
86	85	pm5.32da 452	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
87	86	exbidv 1836	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
88	87	rexbiia 2509	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
89	69, 88	orbi12i 765	. . . . . . . . . . 11 ⊢ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
90	89	mobii 2079	. . . . . . . . . 10 ⊢ (∃𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ ∃𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
91	64, 90	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
92	91	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
93		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
94		f1of 5500	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
95	12, 94	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
96	3, 18	fzfigd 10502	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
97		fex 5787	. . . . . . . . . . . . 13 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
98	95, 96, 97	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
99	11, 2	eleqtrdi 2286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
100	14	ralrimiva 2567	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶)
101		nfv 1539	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝐺‘𝑛) = 𝐶
102		nfcsb1v 3113	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶
103	102	nfeq2 2348	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶
104		fveq2 5554	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
105		csbeq1a 3089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → 𝐶 = ⦋𝑘 / 𝑛⦌𝐶)
106	104, 105	eqeq12d 2208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶))
107	101, 103, 106	cbvral 2722	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶 ↔ ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
108	100, 107	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
109	108	r19.21bi 2582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
110		elfznn 10120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
111	110	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
112		elfzle2 10094	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ≤ 𝑀)
113	112	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≤ 𝑀)
114	113	iftrued 3564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) = (𝐺‘𝑘))
115	104	eleq1d 2262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑘) ∈ ℂ))
116	15	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
117		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝑀))
118	115, 116, 117	rspcdva 2869	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) ∈ ℂ)
119	114, 118	eqeltrd 2270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ)
120		breq1 4032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑀 ↔ 𝑘 ≤ 𝑀))
121	120, 104	ifbieq1d 3579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
122	121, 38	fvmptg 5633	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
123	111, 119, 122	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
124	123, 114	eqtrd 2226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = (𝐺‘𝑘))
125	113	iftrued 3564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) = ⦋𝑘 / 𝑛⦌𝐶)
126	95	ffvelcdmda 5693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
127	10	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
128	126, 127	csbied 3127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
129	50	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
131	130	nfel1 2347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3089	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
133	132	eleq1d 2262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
135	126, 129, 134	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ)
136	128, 135	eqeltrrd 2271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ ℂ)
137	136	ralrimiva 2567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
138		nfv 1539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘 𝐶 ∈ ℂ
139	102	nfel1 2347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ
140	105	eleq1d 2262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐶 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ))
141	138, 139, 140	cbvral 2722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ ↔ ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
142	137, 141	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
143	142	r19.21bi 2582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
144	125, 143	eqeltrd 2270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ)
145		nfcv 2336	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑘
146		nfv 1539	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝑘 ≤ 𝑀
147		nfcv 2336	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛0
148	146, 102, 147	nfif 3585	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0)
149	120, 105	ifbieq1d 3579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
150		eqid 2193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))
151	145, 148, 149, 150	fvmptf 5650	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
152	111, 144, 151	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
153	152, 125	eqtrd 2226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
154	109, 124, 153	3eqtr4d 2236	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘))
155	137	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
156		nfcsb1v 3113	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶
157	156	nfel1 2347	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ
158		csbeq1a 3089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → 𝐶 = ⦋𝑥 / 𝑛⦌𝐶)
159	158	eleq1d 2262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (𝐶 ∈ ℂ ↔ ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
160	157, 159	rspc 2858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
161	28, 155, 160	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ)
162	161, 30, 34	ifcldadc 3586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ)
163		nfcv 2336	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛𝑥
164		nfv 1539	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛 𝑥 ≤ 𝑀
165	164, 156, 147	nfif 3585	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0)
166	36, 158	ifbieq1d 3579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
167	163, 165, 166, 150	fvmptf 5650	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
168	7, 162, 167	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
169	168, 162	eqeltrd 2270	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) ∈ ℂ)
170		addcl 7997	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
171	170	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
172	99, 154, 41, 169, 171	seq3fveq 10550	. . . . . . . . . . . . 13 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
173	12, 172	jca 306	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)))
174		f1oeq1 5488	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175		fveq1 5553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
176	175	csbeq1d 3087	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
177		vex 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑓 ∈ V
178		vex 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑛 ∈ V
179	177, 178	fvex 5574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑛) ∈ V
180	175, 179	eqeltrrdi 2285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝐹‘𝑛) ∈ V)
181	10	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝐹 ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
182	180, 181	csbied 3127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
183	176, 182	eqtrd 2226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
184	183	ifeq1d 3574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, 𝐶, 0))
185	184	mpteq2dv 4120	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))
186	185	seqeq3d 10526	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))))
187	186	fveq1d 5556	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
188	187	eqeq2d 2205	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)))
189	174, 188	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))))
190	189	spcegv 2848	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ V → ((𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)) → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
191	98, 173, 190	sylc 62	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)))
192		oveq2 5926	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
193		f1oeq2 5489	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑚) = (1...𝑀) → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
194	192, 193	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴))
195		breq2 4033	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑀))
196	195	ifbid 3578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
197	196	mpteq2dv 4120	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
198	197	seqeq3d 10526	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
199		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
200	198, 199	fveq12d 5561	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))
201	200	eqeq2d 2205	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)))
202	194, 201	anbi12d 473	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
203	202	exbidv 1836	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
204	203	rspcev 2864	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
205	11, 191, 204	syl2anc 411	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
206	205	olcd 735	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
207	206	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
208		breq2 4033	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
209	208	3anbi3d 1329	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
210	209	rexbidv 2495	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
211		eqeq1 2200	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
212	211	anbi2d 464	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
213	212	exbidv 1836	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
214	213	rexbidv 2495	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
215	210, 214	orbi12d 794	. . . . . . . . 9 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))))
216	215	moi2 2941	. . . . . . . 8 ⊢ ((((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ ∧ ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))) → 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
217	45, 92, 93, 207, 216	syl22anc 1250	. . . . . . 7 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
218	217	ex 115	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) → 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
219	206, 215	syl5ibrcom 157	. . . . . 6 ⊢ (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))))
220	218, 219	impbid 129	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
221	220	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
222	221	iota5 5236	. . 3 ⊢ ((𝜑 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
223	44, 222	mpdan 421	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
224	1, 223	eqtrid 2238	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∃wex 1503 ∃*wmo 2043 ∈ wcel 2164 ∀wral 2472 ∃wrex 2473 Vcvv 2760 ⦋csb 3080 ⊆ wss 3153 ifcif 3557 class class class wbr 4029 ↦ cmpt 4090 ℩cio 5213 ⟶wf 5250 –1-1-onto→wf1o 5253 ‘cfv 5254 (class class class)co 5918 Fincfn 6794 ℂcc 7870 0cc0 7872 1c1 7873 + caddc 7875 ≤ cle 8055 ℕcn 8982 ℕ₀cn0 9240 ℤcz 9317 ℤ_≥cuz 9592 ...cfz 10074 seqcseq 10518 ♯chash 10846 ⇝ cli 11421 Σcsu 11496

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990 ax-arch 7991 ax-caucvg 7992

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-isom 5263 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-irdg 6423 df-frec 6444 df-1o 6469 df-oadd 6473 df-er 6587 df-en 6795 df-dom 6796 df-fin 6797 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-n0 9241 df-z 9318 df-uz 9593 df-q 9685 df-rp 9720 df-fz 10075 df-fzo 10209 df-seqfrec 10519 df-exp 10610 df-ihash 10847 df-cj 10986 df-re 10987 df-im 10988 df-rsqrt 11142 df-abs 11143 df-clim 11422 df-sumdc 11497

This theorem is referenced by: isumz 11532 fsumf1o 11533 fsumcl2lem 11541 fsumadd 11549 sumsnf 11552 fsummulc2 11591

W3C validator