fsum3 - Intuitionistic Logic Explorer

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

Theorem fsum3 12173

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 12139	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
2		nnuz 9968	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9676	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		elnnuz 9969	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈ (ℤ_≥‘1))
5	2	eqimss2i 3305	. . . . . . . . . 10 ⊢ (ℤ_≥‘1) ⊆ ℕ
6	5	sseli 3244	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℕ)
7	6	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℕ)
8		fveq2 5695	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑥 → (𝐺‘𝑛) = (𝐺‘𝑥))
9	8	eleq1d 2307	. . . . . . . . . 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 12172	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
16	15	ad2antrr 492	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
17		1zzd 9676	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ∈ ℤ)
18	11	nnzd 9772	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad2antrr 492	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑀 ∈ ℤ)
20		eluzelz 9941	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℤ)
21	20	ad2antlr 493	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ ℤ)
22	17, 19, 21	3jca 1208	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ))
23		eluzle 9944	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 1 ≤ 𝑥)
24	23	ad2antlr 493	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ≤ 𝑥)
25		simpr 110	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ≤ 𝑀)
26	24, 25	jca 306	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀))
27		elfz2 10429	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀)))
28	22, 26, 27	sylanbrc 421	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ (1...𝑀))
29	9, 16, 28	rspcdva 2934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (𝐺‘𝑥) ∈ ℂ)
30		0cnd 8320	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑥 ≤ 𝑀) → 0 ∈ ℂ)
31	7	nnzd 9772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℤ)
32	18	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑀 ∈ ℤ)
33		zdcle 9726	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑥 ≤ 𝑀)
34	31, 32, 33	syl2anc 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → DECID 𝑥 ≤ 𝑀)
35	29, 30, 34	ifcldadc 3670	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ)
36		breq1 4133	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑀 ↔ 𝑥 ≤ 𝑀))
37	36, 8	ifbieq1d 3663	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
38		eqid 2238	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))
39	37, 38	fvmptg 5781	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
40	7, 35, 39	syl2anc 415	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
41	40, 35	eqeltrd 2315	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
42	4, 41	sylan2b 287	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
43	2, 3, 42	serf 10935	. . . 4 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))):ℕ⟶ℂ)
44	43, 11	ffvelcdmd 5844	. . 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 2299	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47		csbeq1 3150	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
48	46, 47	ifbieq1d 3663	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
49	48	cbvmptv 4227	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
50	13	ralrimiva 2623	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
51		nfcsb1v 3180	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
52	51	nfel1 2403	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
53		csbeq1a 3156	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
54	53	eleq1d 2307	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
55	52, 54	rspc 2923	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
56	50, 55	mpan9 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
57		breq1 4133	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
58		fveq2 5695	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
59	58	csbeq1d 3154	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
60		csbco 3157	. . . . . . . . . . . . . 14 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
61	59, 60	eqtr4di 2289	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
62	57, 61	ifbieq1d 3663	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
63	62	cbvmptv 4227	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
64	49, 56, 63, 63	summodc 12169	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
65		eleq1w 2299	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑗 → (𝑢 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
66	65	dcbid 850	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑗 → (DECID 𝑢 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
67	66	cbvralv 2786	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
68	67	3anbi2i 1222	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
69	68	rexbii 2557	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
70		1zzd 9676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℤ)
71		nnz 9668	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
72	70, 71	fzfigd 10883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ → (1...𝑚) ∈ Fin)
73		fihasheqf1oi 11242	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
74	72, 73	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
75		nnnn0 9575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
76	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ₀)
77		hashfz1 11238	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
79	74, 78	eqtr3d 2273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘𝐴) = 𝑚)
80	79	breq2d 4142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
81	80	ifbid 3662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
82	81	mpteq2dv 4222	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
83	82	seqeq3d 10907	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
84	83	fveq1d 5697	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
85	84	eqeq2d 2250	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
86	85	pm5.32da 456	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
87	86	exbidv 1878	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
88	87	rexbiia 2565	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
89	69, 88	orbi12i 776	. . . . . . . . . . 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 2123	. . . . . . . . . 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 5639	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
95	12, 94	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
96	3, 18	fzfigd 10883	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
97		fex 5947	. . . . . . . . . . . . 13 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
98	95, 96, 97	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
99	11, 2	eleqtrdi 2331	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
100	14	ralrimiva 2623	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶)
101		nfv 1581	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝐺‘𝑛) = 𝐶
102		nfcsb1v 3180	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶
103	102	nfeq2 2404	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶
104		fveq2 5695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
105		csbeq1a 3156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → 𝐶 = ⦋𝑘 / 𝑛⦌𝐶)
106	104, 105	eqeq12d 2253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶))
107	101, 103, 106	cbvral 2782	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶 ↔ ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
108	100, 107	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
109	108	r19.21bi 2638	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
110		elfznn 10471	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
111	110	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
112		elfzle2 10443	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ≤ 𝑀)
113	112	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≤ 𝑀)
114	113	iftrued 3647	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) = (𝐺‘𝑘))
115	104	eleq1d 2307	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑘) ∈ ℂ))
116	15	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
117		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝑀))
118	115, 116, 117	rspcdva 2934	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) ∈ ℂ)
119	114, 118	eqeltrd 2315	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ)
120		breq1 4133	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑀 ↔ 𝑘 ≤ 𝑀))
121	120, 104	ifbieq1d 3663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
122	121, 38	fvmptg 5781	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
123	111, 119, 122	syl2anc 415	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
124	123, 114	eqtrd 2271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = (𝐺‘𝑘))
125	113	iftrued 3647	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) = ⦋𝑘 / 𝑛⦌𝐶)
126	95	ffvelcdmda 5843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
127	10	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
128	126, 127	csbied 3194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
129	50	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
131	130	nfel1 2403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3156	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
133	132	eleq1d 2307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
135	126, 129, 134	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ)
136	128, 135	eqeltrrd 2316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ ℂ)
137	136	ralrimiva 2623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
138		nfv 1581	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘 𝐶 ∈ ℂ
139	102	nfel1 2403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ
140	105	eleq1d 2307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐶 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ))
141	138, 139, 140	cbvral 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ ↔ ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
142	137, 141	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
143	142	r19.21bi 2638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
144	125, 143	eqeltrd 2315	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ)
145		nfcv 2392	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑘
146		nfv 1581	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝑘 ≤ 𝑀
147		nfcv 2392	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛0
148	146, 102, 147	nfif 3669	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0)
149	120, 105	ifbieq1d 3663	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
150		eqid 2238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))
151	145, 148, 149, 150	fvmptf 5798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
152	111, 144, 151	syl2anc 415	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
153	152, 125	eqtrd 2271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
154	109, 124, 153	3eqtr4d 2281	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘))
155	137	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
156		nfcsb1v 3180	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶
157	156	nfel1 2403	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ
158		csbeq1a 3156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → 𝐶 = ⦋𝑥 / 𝑛⦌𝐶)
159	158	eleq1d 2307	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (𝐶 ∈ ℂ ↔ ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
160	157, 159	rspc 2923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
161	28, 155, 160	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ)
162	161, 30, 34	ifcldadc 3670	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ)
163		nfcv 2392	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛𝑥
164		nfv 1581	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛 𝑥 ≤ 𝑀
165	164, 156, 147	nfif 3669	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0)
166	36, 158	ifbieq1d 3663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
167	163, 165, 166, 150	fvmptf 5798	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
168	7, 162, 167	syl2anc 415	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
169	168, 162	eqeltrd 2315	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) ∈ ℂ)
170		addcl 8305	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
171	170	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
172	99, 154, 41, 169, 171	seq3fveq 10931	. . . . . . . . . . . . 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 5627	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175		fveq1 5694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
176	175	csbeq1d 3154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
177		vex 2824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑓 ∈ V
178		vex 2824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑛 ∈ V
179	177, 178	fvex 5715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑛) ∈ V
180	175, 179	eqeltrrdi 2330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝐹‘𝑛) ∈ V)
181	10	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝐹 ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
182	180, 181	csbied 3194	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
183	176, 182	eqtrd 2271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
184	183	ifeq1d 3658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, 𝐶, 0))
185	184	mpteq2dv 4222	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))
186	185	seqeq3d 10907	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))))
187	186	fveq1d 5697	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
188	187	eqeq2d 2250	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)))
189	174, 188	anbi12d 477	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))))
190	189	spcegv 2913	. . . . . . . . . . . 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 6093	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
193		f1oeq2 5628	. . . . . . . . . . . . . . 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 4134	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑀))
196	195	ifbid 3662	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
197	196	mpteq2dv 4222	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
198	197	seqeq3d 10907	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
199		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
200	198, 199	fveq12d 5702	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))
201	200	eqeq2d 2250	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)))
202	194, 201	anbi12d 477	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
203	202	exbidv 1878	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
204	203	rspcev 2929	. . . . . . . . . . 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 415	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
206	205	olcd 746	. . . . . . . . 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 4134	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
209	208	3anbi3d 1359	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
210	209	rexbidv 2551	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
211		eqeq1 2245	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
212	211	anbi2d 468	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
213	212	exbidv 1878	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
214	213	rexbidv 2551	. . . . . . . . . 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 805	. . . . . . . . 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 3007	. . . . . . . 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 1279	. . . . . . 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 5359	. . 3 ⊢ ((𝜑 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
223	44, 222	mpdan 425	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
224	1, 223	eqtrid 2283	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∃wex 1545 ∃*wmo 2087 ∈ wcel 2209 ∀wral 2528 ∃wrex 2529 Vcvv 2821 ⦋csb 3147 ⊆ wss 3220 ifcif 3638 class class class wbr 4130 ↦ cmpt 4192 ℩cio 5335 ⟶wf 5373 –1-1-onto→wf1o 5376 ‘cfv 5377 (class class class)co 6085 Fincfn 7022 ℂcc 8178 0cc0 8180 1c1 8181 + caddc 8183 ≤ cle 8362 ℕcn 9307 ℕ₀cn0 9568 ℤcz 9649 ℤ_≥cuz 9931 ...cfz 10422 seqcseq 10899 ♯chash 11230 ⇝ cli 12063 Σcsu 12138

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8271 ax-resscn 8272 ax-1cn 8273 ax-1re 8274 ax-icn 8275 ax-addcl 8276 ax-addrcl 8277 ax-mulcl 8278 ax-mulrcl 8279 ax-addcom 8280 ax-mulcom 8281 ax-addass 8282 ax-mulass 8283 ax-distr 8284 ax-i2m1 8285 ax-0lt1 8286 ax-1rid 8287 ax-0id 8288 ax-rnegex 8289 ax-precex 8290 ax-cnre 8291 ax-pre-ltirr 8292 ax-pre-ltwlin 8293 ax-pre-lttrn 8294 ax-pre-apti 8295 ax-pre-ltadd 8296 ax-pre-mulgt0 8297 ax-pre-mulext 8298 ax-arch 8299 ax-caucvg 8300

This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-oadd 6691 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-pnf 8363 df-mnf 8364 df-xr 8365 df-ltxr 8366 df-le 8367 df-sub 8501 df-neg 8502 df-reap 8906 df-ap 8913 df-div 9006 df-inn 9308 df-2 9366 df-3 9367 df-4 9368 df-n0 9569 df-z 9650 df-uz 9932 df-q 10030 df-rp 10066 df-fz 10423 df-fzo 10561 df-seqfrec 10900 df-exp 10991 df-ihash 11231 df-cj 11623 df-re 11624 df-im 11625 df-rsqrt 11780 df-abs 11781 df-clim 12064 df-sumdc 12139

This theorem is used by: isumz 12175 fsumf1o 12176 fsumcl2lem 12184 fsumadd 12192 sumsnf 12195 fsummulc2 12234

W3C validator