fsum3 - Intuitionistic Logic Explorer

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

Theorem fsum3 11379

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 11346	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
2		nnuz 9552	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9269	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		elnnuz 9553	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈ (ℤ_≥‘1))
5	2	eqimss2i 3212	. . . . . . . . . 10 ⊢ (ℤ_≥‘1) ⊆ ℕ
6	5	sseli 3151	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℕ)
7	6	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℕ)
8		fveq2 5511	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑥 → (𝐺‘𝑛) = (𝐺‘𝑥))
9	8	eleq1d 2246	. . . . . . . . . 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 11378	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
16	15	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
17		1zzd 9269	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ∈ ℤ)
18	11	nnzd 9363	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑀 ∈ ℤ)
20		eluzelz 9526	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℤ)
21	20	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ ℤ)
22	17, 19, 21	3jca 1177	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ))
23		eluzle 9529	. . . . . . . . . . . . 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 10002	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀)))
28	22, 26, 27	sylanbrc 417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ (1...𝑀))
29	9, 16, 28	rspcdva 2846	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (𝐺‘𝑥) ∈ ℂ)
30		0cnd 7941	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑥 ≤ 𝑀) → 0 ∈ ℂ)
31	7	nnzd 9363	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℤ)
32	18	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑀 ∈ ℤ)
33		zdcle 9318	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑥 ≤ 𝑀)
34	31, 32, 33	syl2anc 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → DECID 𝑥 ≤ 𝑀)
35	29, 30, 34	ifcldadc 3563	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ)
36		breq1 4003	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑀 ↔ 𝑥 ≤ 𝑀))
37	36, 8	ifbieq1d 3556	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
38		eqid 2177	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))
39	37, 38	fvmptg 5588	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
40	7, 35, 39	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
41	40, 35	eqeltrd 2254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
42	4, 41	sylan2b 287	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
43	2, 3, 42	serf 10460	. . . 4 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))):ℕ⟶ℂ)
44	43, 11	ffvelcdmd 5648	. . 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 2238	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47		csbeq1 3060	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
48	46, 47	ifbieq1d 3556	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
49	48	cbvmptv 4096	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
50	13	ralrimiva 2550	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
51		nfcsb1v 3090	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
52	51	nfel1 2330	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
53		csbeq1a 3066	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
54	53	eleq1d 2246	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
55	52, 54	rspc 2835	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
56	50, 55	mpan9 281	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
57		breq1 4003	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
58		fveq2 5511	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
59	58	csbeq1d 3064	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
60		csbco 3067	. . . . . . . . . . . . . 14 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
61	59, 60	eqtr4di 2228	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
62	57, 61	ifbieq1d 3556	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
63	62	cbvmptv 4096	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
64	49, 56, 63, 63	summodc 11375	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
65		eleq1w 2238	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑗 → (𝑢 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
66	65	dcbid 838	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑗 → (DECID 𝑢 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
67	66	cbvralv 2703	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
68	67	3anbi2i 1191	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
69	68	rexbii 2484	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
70		1zzd 9269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℤ)
71		nnz 9261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
72	70, 71	fzfigd 10417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ → (1...𝑚) ∈ Fin)
73		fihasheqf1oi 10751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
74	72, 73	sylan 283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
75		nnnn0 9172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
76	75	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ₀)
77		hashfz1 10747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
79	74, 78	eqtr3d 2212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘𝐴) = 𝑚)
80	79	breq2d 4012	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
81	80	ifbid 3555	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
82	81	mpteq2dv 4091	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
83	82	seqeq3d 10439	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
84	83	fveq1d 5513	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
85	84	eqeq2d 2189	. . . . . . . . . . . . . . 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 1825	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
88	87	rexbiia 2492	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
89	69, 88	orbi12i 764	. . . . . . . . . . 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 2063	. . . . . . . . . 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 5457	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
95	12, 94	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
96	3, 18	fzfigd 10417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
97		fex 5741	. . . . . . . . . . . . 13 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
98	95, 96, 97	syl2anc 411	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
99	11, 2	eleqtrdi 2270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
100	14	ralrimiva 2550	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶)
101		nfv 1528	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝐺‘𝑛) = 𝐶
102		nfcsb1v 3090	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶
103	102	nfeq2 2331	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶
104		fveq2 5511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
105		csbeq1a 3066	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → 𝐶 = ⦋𝑘 / 𝑛⦌𝐶)
106	104, 105	eqeq12d 2192	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶))
107	101, 103, 106	cbvral 2699	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶 ↔ ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
108	100, 107	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
109	108	r19.21bi 2565	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
110		elfznn 10040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
111	110	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
112		elfzle2 10014	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ≤ 𝑀)
113	112	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≤ 𝑀)
114	113	iftrued 3541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) = (𝐺‘𝑘))
115	104	eleq1d 2246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑘) ∈ ℂ))
116	15	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
117		simpr 110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝑀))
118	115, 116, 117	rspcdva 2846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) ∈ ℂ)
119	114, 118	eqeltrd 2254	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ)
120		breq1 4003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑀 ↔ 𝑘 ≤ 𝑀))
121	120, 104	ifbieq1d 3556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
122	121, 38	fvmptg 5588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
123	111, 119, 122	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
124	123, 114	eqtrd 2210	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = (𝐺‘𝑘))
125	113	iftrued 3541	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) = ⦋𝑘 / 𝑛⦌𝐶)
126	95	ffvelcdmda 5647	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
127	10	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
128	126, 127	csbied 3103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
129	50	adantr 276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3090	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
131	130	nfel1 2330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3066	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
133	132	eleq1d 2246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
135	126, 129, 134	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ)
136	128, 135	eqeltrrd 2255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ ℂ)
137	136	ralrimiva 2550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
138		nfv 1528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘 𝐶 ∈ ℂ
139	102	nfel1 2330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ
140	105	eleq1d 2246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐶 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ))
141	138, 139, 140	cbvral 2699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ ↔ ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
142	137, 141	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
143	142	r19.21bi 2565	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
144	125, 143	eqeltrd 2254	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ)
145		nfcv 2319	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑘
146		nfv 1528	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝑘 ≤ 𝑀
147		nfcv 2319	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛0
148	146, 102, 147	nfif 3562	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0)
149	120, 105	ifbieq1d 3556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
150		eqid 2177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))
151	145, 148, 149, 150	fvmptf 5604	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
152	111, 144, 151	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
153	152, 125	eqtrd 2210	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
154	109, 124, 153	3eqtr4d 2220	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘))
155	137	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
156		nfcsb1v 3090	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶
157	156	nfel1 2330	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ
158		csbeq1a 3066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → 𝐶 = ⦋𝑥 / 𝑛⦌𝐶)
159	158	eleq1d 2246	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (𝐶 ∈ ℂ ↔ ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
160	157, 159	rspc 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
161	28, 155, 160	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ)
162	161, 30, 34	ifcldadc 3563	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ)
163		nfcv 2319	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛𝑥
164		nfv 1528	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛 𝑥 ≤ 𝑀
165	164, 156, 147	nfif 3562	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0)
166	36, 158	ifbieq1d 3556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
167	163, 165, 166, 150	fvmptf 5604	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
168	7, 162, 167	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
169	168, 162	eqeltrd 2254	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) ∈ ℂ)
170		addcl 7927	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
171	170	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
172	99, 154, 41, 169, 171	seq3fveq 10457	. . . . . . . . . . . . 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 5445	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175		fveq1 5510	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
176	175	csbeq1d 3064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
177		vex 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑓 ∈ V
178		vex 2740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑛 ∈ V
179	177, 178	fvex 5531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑛) ∈ V
180	175, 179	eqeltrrdi 2269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝐹‘𝑛) ∈ V)
181	10	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝐹 ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
182	180, 181	csbied 3103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
183	176, 182	eqtrd 2210	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
184	183	ifeq1d 3551	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, 𝐶, 0))
185	184	mpteq2dv 4091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))
186	185	seqeq3d 10439	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))))
187	186	fveq1d 5513	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
188	187	eqeq2d 2189	. . . . . . . . . . . . . 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 2825	. . . . . . . . . . . 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 5877	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
193		f1oeq2 5446	. . . . . . . . . . . . . . 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 4004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑀))
196	195	ifbid 3555	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
197	196	mpteq2dv 4091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
198	197	seqeq3d 10439	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
199		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
200	198, 199	fveq12d 5518	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))
201	200	eqeq2d 2189	. . . . . . . . . . . . . 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 1825	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
204	203	rspcev 2841	. . . . . . . . . . 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 734	. . . . . . . . 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 4004	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
209	208	3anbi3d 1318	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
210	209	rexbidv 2478	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
211		eqeq1 2184	. . . . . . . . . . . . 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 1825	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
214	213	rexbidv 2478	. . . . . . . . . 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 793	. . . . . . . . 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 2918	. . . . . . . 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 1239	. . . . . . 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 5194	. . 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 2222	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 708 DECID wdc 834 ∧ w3a 978 = wceq 1353 ∃wex 1492 ∃*wmo 2027 ∈ wcel 2148 ∀wral 2455 ∃wrex 2456 Vcvv 2737 ⦋csb 3057 ⊆ wss 3129 ifcif 3534 class class class wbr 4000 ↦ cmpt 4061 ℩cio 5172 ⟶wf 5208 –1-1-onto→wf1o 5211 ‘cfv 5212 (class class class)co 5869 Fincfn 6734 ℂcc 7800 0cc0 7802 1c1 7803 + caddc 7805 ≤ cle 7983 ℕcn 8908 ℕ₀cn0 9165 ℤcz 9242 ℤ_≥cuz 9517 ...cfz 9995 seqcseq 10431 ♯chash 10739 ⇝ cli 11270 Σcsu 11345

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-isom 5221 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-1st 6135 df-2nd 6136 df-recs 6300 df-irdg 6365 df-frec 6386 df-1o 6411 df-oadd 6415 df-er 6529 df-en 6735 df-dom 6736 df-fin 6737 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-fz 9996 df-fzo 10129 df-seqfrec 10432 df-exp 10506 df-ihash 10740 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-clim 11271 df-sumdc 11346

This theorem is referenced by: isumz 11381 fsumf1o 11382 fsumcl2lem 11390 fsumadd 11398 sumsnf 11401 fsummulc2 11440

W3C validator