fsum3 - Intuitionistic Logic Explorer

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

Theorem fsum3 11409

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 11376	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
2		nnuz 9577	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9294	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		elnnuz 9578	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈ (ℤ_≥‘1))
5	2	eqimss2i 3224	. . . . . . . . . 10 ⊢ (ℤ_≥‘1) ⊆ ℕ
6	5	sseli 3163	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℕ)
7	6	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℕ)
8		fveq2 5527	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑥 → (𝐺‘𝑛) = (𝐺‘𝑥))
9	8	eleq1d 2256	. . . . . . . . . 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 11408	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
16	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
17		1zzd 9294	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ∈ ℤ)
18	11	nnzd 9388	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑀 ∈ ℤ)
20		eluzelz 9551	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℤ)
21	20	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ ℤ)
22	17, 19, 21	3jca 1178	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ))
23		eluzle 9554	. . . . . . . . . . . . 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 10029	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀)))
28	22, 26, 27	sylanbrc 417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ (1...𝑀))
29	9, 16, 28	rspcdva 2858	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (𝐺‘𝑥) ∈ ℂ)
30		0cnd 7964	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑥 ≤ 𝑀) → 0 ∈ ℂ)
31	7	nnzd 9388	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℤ)
32	18	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑀 ∈ ℤ)
33		zdcle 9343	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑥 ≤ 𝑀)
34	31, 32, 33	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → DECID 𝑥 ≤ 𝑀)
35	29, 30, 34	ifcldadc 3575	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ)
36		breq1 4018	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑀 ↔ 𝑥 ≤ 𝑀))
37	36, 8	ifbieq1d 3568	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
38		eqid 2187	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))
39	37, 38	fvmptg 5605	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
40	7, 35, 39	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
41	40, 35	eqeltrd 2264	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
42	4, 41	sylan2b 287	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
43	2, 3, 42	serf 10488	. . . 4 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))):ℕ⟶ℂ)
44	43, 11	ffvelcdmd 5665	. . 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 2248	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47		csbeq1 3072	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
48	46, 47	ifbieq1d 3568	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
49	48	cbvmptv 4111	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
50	13	ralrimiva 2560	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
51		nfcsb1v 3102	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
52	51	nfel1 2340	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
53		csbeq1a 3078	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
54	53	eleq1d 2256	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
55	52, 54	rspc 2847	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
56	50, 55	mpan9 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
57		breq1 4018	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
58		fveq2 5527	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
59	58	csbeq1d 3076	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
60		csbco 3079	. . . . . . . . . . . . . 14 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
61	59, 60	eqtr4di 2238	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
62	57, 61	ifbieq1d 3568	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
63	62	cbvmptv 4111	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
64	49, 56, 63, 63	summodc 11405	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
65		eleq1w 2248	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑗 → (𝑢 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
66	65	dcbid 839	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑗 → (DECID 𝑢 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
67	66	cbvralv 2715	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
68	67	3anbi2i 1192	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
69	68	rexbii 2494	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
70		1zzd 9294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℤ)
71		nnz 9286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
72	70, 71	fzfigd 10445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ → (1...𝑚) ∈ Fin)
73		fihasheqf1oi 10781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
74	72, 73	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
75		nnnn0 9197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
76	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ₀)
77		hashfz1 10777	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
79	74, 78	eqtr3d 2222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘𝐴) = 𝑚)
80	79	breq2d 4027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
81	80	ifbid 3567	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
82	81	mpteq2dv 4106	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
83	82	seqeq3d 10467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
84	83	fveq1d 5529	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
85	84	eqeq2d 2199	. . . . . . . . . . . . . . 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 1835	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
88	87	rexbiia 2502	. . . . . . . . . . . 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 2073	. . . . . . . . . 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 5473	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
95	12, 94	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
96	3, 18	fzfigd 10445	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
97		fex 5758	. . . . . . . . . . . . 13 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
98	95, 96, 97	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
99	11, 2	eleqtrdi 2280	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
100	14	ralrimiva 2560	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶)
101		nfv 1538	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝐺‘𝑛) = 𝐶
102		nfcsb1v 3102	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶
103	102	nfeq2 2341	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶
104		fveq2 5527	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
105		csbeq1a 3078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → 𝐶 = ⦋𝑘 / 𝑛⦌𝐶)
106	104, 105	eqeq12d 2202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶))
107	101, 103, 106	cbvral 2711	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶 ↔ ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
108	100, 107	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
109	108	r19.21bi 2575	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
110		elfznn 10068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
111	110	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
112		elfzle2 10042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ≤ 𝑀)
113	112	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≤ 𝑀)
114	113	iftrued 3553	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) = (𝐺‘𝑘))
115	104	eleq1d 2256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑘) ∈ ℂ))
116	15	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
117		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝑀))
118	115, 116, 117	rspcdva 2858	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) ∈ ℂ)
119	114, 118	eqeltrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ)
120		breq1 4018	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑀 ↔ 𝑘 ≤ 𝑀))
121	120, 104	ifbieq1d 3568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
122	121, 38	fvmptg 5605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
123	111, 119, 122	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
124	123, 114	eqtrd 2220	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = (𝐺‘𝑘))
125	113	iftrued 3553	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) = ⦋𝑘 / 𝑛⦌𝐶)
126	95	ffvelcdmda 5664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
127	10	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
128	126, 127	csbied 3115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
129	50	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3102	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
131	130	nfel1 2340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3078	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
133	132	eleq1d 2256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
135	126, 129, 134	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ)
136	128, 135	eqeltrrd 2265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ ℂ)
137	136	ralrimiva 2560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
138		nfv 1538	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘 𝐶 ∈ ℂ
139	102	nfel1 2340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ
140	105	eleq1d 2256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐶 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ))
141	138, 139, 140	cbvral 2711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ ↔ ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
142	137, 141	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
143	142	r19.21bi 2575	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
144	125, 143	eqeltrd 2264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ)
145		nfcv 2329	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑘
146		nfv 1538	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝑘 ≤ 𝑀
147		nfcv 2329	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛0
148	146, 102, 147	nfif 3574	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0)
149	120, 105	ifbieq1d 3568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
150		eqid 2187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))
151	145, 148, 149, 150	fvmptf 5621	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
152	111, 144, 151	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
153	152, 125	eqtrd 2220	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
154	109, 124, 153	3eqtr4d 2230	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘))
155	137	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
156		nfcsb1v 3102	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶
157	156	nfel1 2340	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ
158		csbeq1a 3078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → 𝐶 = ⦋𝑥 / 𝑛⦌𝐶)
159	158	eleq1d 2256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (𝐶 ∈ ℂ ↔ ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
160	157, 159	rspc 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
161	28, 155, 160	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ)
162	161, 30, 34	ifcldadc 3575	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ)
163		nfcv 2329	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛𝑥
164		nfv 1538	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛 𝑥 ≤ 𝑀
165	164, 156, 147	nfif 3574	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0)
166	36, 158	ifbieq1d 3568	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
167	163, 165, 166, 150	fvmptf 5621	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
168	7, 162, 167	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
169	168, 162	eqeltrd 2264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) ∈ ℂ)
170		addcl 7950	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
171	170	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
172	99, 154, 41, 169, 171	seq3fveq 10485	. . . . . . . . . . . . 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 5461	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175		fveq1 5526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
176	175	csbeq1d 3076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
177		vex 2752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑓 ∈ V
178		vex 2752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑛 ∈ V
179	177, 178	fvex 5547	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑛) ∈ V
180	175, 179	eqeltrrdi 2279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝐹‘𝑛) ∈ V)
181	10	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝐹 ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
182	180, 181	csbied 3115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
183	176, 182	eqtrd 2220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
184	183	ifeq1d 3563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, 𝐶, 0))
185	184	mpteq2dv 4106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))
186	185	seqeq3d 10467	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))))
187	186	fveq1d 5529	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
188	187	eqeq2d 2199	. . . . . . . . . . . . . 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 2837	. . . . . . . . . . . 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 5896	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
193		f1oeq2 5462	. . . . . . . . . . . . . . 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 4019	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑀))
196	195	ifbid 3567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
197	196	mpteq2dv 4106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
198	197	seqeq3d 10467	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
199		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
200	198, 199	fveq12d 5534	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))
201	200	eqeq2d 2199	. . . . . . . . . . . . . 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 1835	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
204	203	rspcev 2853	. . . . . . . . . . 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 4019	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
209	208	3anbi3d 1328	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
210	209	rexbidv 2488	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
211		eqeq1 2194	. . . . . . . . . . . . 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 1835	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
214	213	rexbidv 2488	. . . . . . . . . 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 2930	. . . . . . . 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 1249	. . . . . . 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 5210	. . 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 2232	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 979 = wceq 1363 ∃wex 1502 ∃*wmo 2037 ∈ wcel 2158 ∀wral 2465 ∃wrex 2466 Vcvv 2749 ⦋csb 3069 ⊆ wss 3141 ifcif 3546 class class class wbr 4015 ↦ cmpt 4076 ℩cio 5188 ⟶wf 5224 –1-1-onto→wf1o 5227 ‘cfv 5228 (class class class)co 5888 Fincfn 6754 ℂcc 7823 0cc0 7825 1c1 7826 + caddc 7828 ≤ cle 8007 ℕcn 8933 ℕ₀cn0 9190 ℤcz 9267 ℤ_≥cuz 9542 ...cfz 10022 seqcseq 10459 ♯chash 10769 ⇝ cli 11300 Σcsu 11375

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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-13 2160 ax-14 2161 ax-ext 2169 ax-coll 4130 ax-sep 4133 ax-nul 4141 ax-pow 4186 ax-pr 4221 ax-un 4445 ax-setind 4548 ax-iinf 4599 ax-cnex 7916 ax-resscn 7917 ax-1cn 7918 ax-1re 7919 ax-icn 7920 ax-addcl 7921 ax-addrcl 7922 ax-mulcl 7923 ax-mulrcl 7924 ax-addcom 7925 ax-mulcom 7926 ax-addass 7927 ax-mulass 7928 ax-distr 7929 ax-i2m1 7930 ax-0lt1 7931 ax-1rid 7932 ax-0id 7933 ax-rnegex 7934 ax-precex 7935 ax-cnre 7936 ax-pre-ltirr 7937 ax-pre-ltwlin 7938 ax-pre-lttrn 7939 ax-pre-apti 7940 ax-pre-ltadd 7941 ax-pre-mulgt0 7942 ax-pre-mulext 7943 ax-arch 7944 ax-caucvg 7945

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 980 df-3an 981 df-tru 1366 df-fal 1369 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ne 2358 df-nel 2453 df-ral 2470 df-rex 2471 df-reu 2472 df-rmo 2473 df-rab 2474 df-v 2751 df-sbc 2975 df-csb 3070 df-dif 3143 df-un 3145 df-in 3147 df-ss 3154 df-nul 3435 df-if 3547 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-iun 3900 df-br 4016 df-opab 4077 df-mpt 4078 df-tr 4114 df-id 4305 df-po 4308 df-iso 4309 df-iord 4378 df-on 4380 df-ilim 4381 df-suc 4383 df-iom 4602 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-rn 4649 df-res 4650 df-ima 4651 df-iota 5190 df-fun 5230 df-fn 5231 df-f 5232 df-f1 5233 df-fo 5234 df-f1o 5235 df-fv 5236 df-isom 5237 df-riota 5844 df-ov 5891 df-oprab 5892 df-mpo 5893 df-1st 6155 df-2nd 6156 df-recs 6320 df-irdg 6385 df-frec 6406 df-1o 6431 df-oadd 6435 df-er 6549 df-en 6755 df-dom 6756 df-fin 6757 df-pnf 8008 df-mnf 8009 df-xr 8010 df-ltxr 8011 df-le 8012 df-sub 8144 df-neg 8145 df-reap 8546 df-ap 8553 df-div 8644 df-inn 8934 df-2 8992 df-3 8993 df-4 8994 df-n0 9191 df-z 9268 df-uz 9543 df-q 9634 df-rp 9668 df-fz 10023 df-fzo 10157 df-seqfrec 10460 df-exp 10534 df-ihash 10770 df-cj 10865 df-re 10866 df-im 10867 df-rsqrt 11021 df-abs 11022 df-clim 11301 df-sumdc 11376

This theorem is referenced by: isumz 11411 fsumf1o 11412 fsumcl2lem 11420 fsumadd 11428 sumsnf 11431 fsummulc2 11470

W3C validator