fsum3 - Intuitionistic Logic Explorer

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

Theorem fsum3 11350

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 11317	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
2		nnuz 9522	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
3		1zzd 9239	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
4		elnnuz 9523	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↔ 𝑥 ∈ (ℤ_≥‘1))
5	2	eqimss2i 3204	. . . . . . . . . 10 ⊢ (ℤ_≥‘1) ⊆ ℕ
6	5	sseli 3143	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℕ)
7	6	adantl 275	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℕ)
8		fveq2 5496	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑥 → (𝐺‘𝑛) = (𝐺‘𝑥))
9	8	eleq1d 2239	. . . . . . . . . 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 11349	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
16	15	ad2antrr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
17		1zzd 9239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ∈ ℤ)
18	11	nnzd 9333	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
19	18	ad2antrr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑀 ∈ ℤ)
20		eluzelz 9496	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 𝑥 ∈ ℤ)
21	20	ad2antlr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ ℤ)
22	17, 19, 21	3jca 1172	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ))
23		eluzle 9499	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (ℤ_≥‘1) → 1 ≤ 𝑥)
24	23	ad2antlr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 1 ≤ 𝑥)
25		simpr 109	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ≤ 𝑀)
26	24, 25	jca 304	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀))
27		elfz2 9972	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝑀) ↔ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ (1 ≤ 𝑥 ∧ 𝑥 ≤ 𝑀)))
28	22, 26, 27	sylanbrc 415	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → 𝑥 ∈ (1...𝑀))
29	9, 16, 28	rspcdva 2839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → (𝐺‘𝑥) ∈ ℂ)
30		0cnd 7913	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑥 ≤ 𝑀) → 0 ∈ ℂ)
31	7	nnzd 9333	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑥 ∈ ℤ)
32	18	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → 𝑀 ∈ ℤ)
33		zdcle 9288	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑥 ≤ 𝑀)
34	31, 32, 33	syl2anc 409	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → DECID 𝑥 ≤ 𝑀)
35	29, 30, 34	ifcldadc 3555	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ)
36		breq1 3992	. . . . . . . . . 10 ⊢ (𝑛 = 𝑥 → (𝑛 ≤ 𝑀 ↔ 𝑥 ≤ 𝑀))
37	36, 8	ifbieq1d 3548	. . . . . . . . 9 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
38		eqid 2170	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))
39	37, 38	fvmptg 5572	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
40	7, 35, 39	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) = if(𝑥 ≤ 𝑀, (𝐺‘𝑥), 0))
41	40, 35	eqeltrd 2247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
42	4, 41	sylan2b 285	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑥) ∈ ℂ)
43	2, 3, 42	serf 10430	. . . 4 ⊢ (𝜑 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))):ℕ⟶ℂ)
44	43, 11	ffvelrnd 5632	. . 3 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ)
45	44	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ)
46		eleq1w 2231	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
47		csbeq1 3052	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
48	46, 47	ifbieq1d 3548	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
49	48	cbvmptv 4085	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
50	13	ralrimiva 2543	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
51		nfcsb1v 3082	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
52	51	nfel1 2323	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
53		csbeq1a 3058	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
54	53	eleq1d 2239	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
55	52, 54	rspc 2828	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
56	50, 55	mpan9 279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
57		breq1 3992	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑖 ≤ (♯‘𝐴)))
58		fveq2 5496	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖))
59	58	csbeq1d 3056	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵)
60		csbco 3059	. . . . . . . . . . . . . 14 ⊢ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵
61	59, 60	eqtr4di 2221	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵)
62	57, 61	ifbieq1d 3548	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
63	62	cbvmptv 4085	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℕ ↦ if(𝑖 ≤ (♯‘𝐴), ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵, 0))
64	49, 56, 63, 63	summodc 11346	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
65		eleq1w 2231	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑗 → (𝑢 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
66	65	dcbid 833	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑗 → (DECID 𝑢 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
67	66	cbvralv 2696	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴)
68	67	3anbi2i 1186	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
69	68	rexbii 2477	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑢 ∈ (ℤ_≥‘𝑚)DECID 𝑢 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
70		1zzd 9239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 1 ∈ ℤ)
71		nnz 9231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
72	70, 71	fzfigd 10387	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ → (1...𝑚) ∈ Fin)
73		fihasheqf1oi 10722	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
74	72, 73	sylan 281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = (♯‘𝐴))
75		nnnn0 9142	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
76	75	adantr 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ₀)
77		hashfz1 10717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
78	76, 77	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘(1...𝑚)) = 𝑚)
79	74, 78	eqtr3d 2205	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (♯‘𝐴) = 𝑚)
80	79	breq2d 4001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
81	80	ifbid 3547	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
82	81	mpteq2dv 4080	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
83	82	seqeq3d 10409	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
84	83	fveq1d 5498	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
85	84	eqeq2d 2182	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
86	85	pm5.32da 449	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
87	86	exbidv 1818	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
88	87	rexbiia 2485	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
89	69, 88	orbi12i 759	. . . . . . . . . . 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 2056	. . . . . . . . . 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 121	. . . . . . . . 9 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
92	91	adantr 274	. . . . . . . 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 109	. . . . . . . 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 5442	. . . . . . . . . . . . . 14 ⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴)
95	12, 94	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴)
96	3, 18	fzfigd 10387	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
97		fex 5725	. . . . . . . . . . . . 13 ⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ Fin) → 𝐹 ∈ V)
98	95, 96, 97	syl2anc 409	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ V)
99	11, 2	eleqtrdi 2263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
100	14	ralrimiva 2543	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶)
101		nfv 1521	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑘(𝐺‘𝑛) = 𝐶
102		nfcsb1v 3082	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶
103	102	nfeq2 2324	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶
104		fveq2 5496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
105		csbeq1a 3058	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → 𝐶 = ⦋𝑘 / 𝑛⦌𝐶)
106	104, 105	eqeq12d 2185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = 𝐶 ↔ (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶))
107	101, 103, 106	cbvral 2692	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = 𝐶 ↔ ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
108	100, 107	sylib 121	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
109	108	r19.21bi 2558	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
110		elfznn 10010	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
111	110	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
112		elfzle2 9984	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ≤ 𝑀)
113	112	adantl 275	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≤ 𝑀)
114	113	iftrued 3533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) = (𝐺‘𝑘))
115	104	eleq1d 2239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) ∈ ℂ ↔ (𝐺‘𝑘) ∈ ℂ))
116	15	adantr 274	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) ∈ ℂ)
117		simpr 109	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ (1...𝑀))
118	115, 116, 117	rspcdva 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) ∈ ℂ)
119	114, 118	eqeltrd 2247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ)
120		breq1 3992	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑘 → (𝑛 ≤ 𝑀 ↔ 𝑘 ≤ 𝑀))
121	120, 104	ifbieq1d 3548	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
122	121, 38	fvmptg 5572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
123	111, 119, 122	syl2anc 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = if(𝑘 ≤ 𝑀, (𝐺‘𝑘), 0))
124	123, 114	eqtrd 2203	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = (𝐺‘𝑘))
125	113	iftrued 3533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) = ⦋𝑘 / 𝑛⦌𝐶)
126	95	ffvelrnda 5631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐹‘𝑛) ∈ 𝐴)
127	10	adantl 275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
128	126, 127	csbied 3095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
129	50	adantr 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵
131	130	nfel1 2323	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3058	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
133	132	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐹‘𝑛) → (𝐵 ∈ ℂ ↔ ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ))
135	126, 129, 134	sylc 62	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 ∈ ℂ)
136	128, 135	eqeltrrd 2248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ ℂ)
137	136	ralrimiva 2543	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
138		nfv 1521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑘 𝐶 ∈ ℂ
139	102	nfel1 2323	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ⅎ𝑛⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ
140	105	eleq1d 2239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → (𝐶 ∈ ℂ ↔ ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ))
141	138, 139, 140	cbvral 2692	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ ↔ ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
142	137, 141	sylib 121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
143	142	r19.21bi 2558	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ⦋𝑘 / 𝑛⦌𝐶 ∈ ℂ)
144	125, 143	eqeltrd 2247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ)
145		nfcv 2312	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑘
146		nfv 1521	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛 𝑘 ≤ 𝑀
147		nfcv 2312	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛0
148	146, 102, 147	nfif 3554	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0)
149	120, 105	ifbieq1d 3548	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑘 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
150		eqid 2170	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))
151	145, 148, 149, 150	fvmptf 5588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
152	111, 144, 151	syl2anc 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = if(𝑘 ≤ 𝑀, ⦋𝑘 / 𝑛⦌𝐶, 0))
153	152, 125	eqtrd 2203	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘) = ⦋𝑘 / 𝑛⦌𝐶)
154	109, 124, 153	3eqtr4d 2213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0))‘𝑘) = ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑘))
155	137	ad2antrr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ)
156		nfcsb1v 3082	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶
157	156	nfel1 2323	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑛⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ
158		csbeq1a 3058	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → 𝐶 = ⦋𝑥 / 𝑛⦌𝐶)
159	158	eleq1d 2239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (𝐶 ∈ ℂ ↔ ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
160	157, 159	rspc 2828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)𝐶 ∈ ℂ → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ))
161	28, 155, 160	sylc 62	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) ∧ 𝑥 ≤ 𝑀) → ⦋𝑥 / 𝑛⦌𝐶 ∈ ℂ)
162	161, 30, 34	ifcldadc 3555	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ)
163		nfcv 2312	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛𝑥
164		nfv 1521	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛 𝑥 ≤ 𝑀
165	164, 156, 147	nfif 3554	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑛if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0)
166	36, 158	ifbieq1d 3548	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → if(𝑛 ≤ 𝑀, 𝐶, 0) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
167	163, 165, 166, 150	fvmptf 5588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0) ∈ ℂ) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
168	7, 162, 167	syl2anc 409	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) = if(𝑥 ≤ 𝑀, ⦋𝑥 / 𝑛⦌𝐶, 0))
169	168, 162	eqeltrd 2247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘1)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))‘𝑥) ∈ ℂ)
170		addcl 7899	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ)
171	170	adantl 275	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ)
172	99, 154, 41, 169, 171	seq3fveq 10427	. . . . . . . . . . . . 13 ⊢ (𝜑 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
173	12, 172	jca 304	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)))
174		f1oeq1 5431	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴))
175		fveq1 5495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛))
176	175	csbeq1d 3056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵)
177		vex 2733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑓 ∈ V
178		vex 2733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑛 ∈ V
179	177, 178	fvex 5516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓‘𝑛) ∈ V
180	175, 179	eqeltrrdi 2262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝐹 → (𝐹‘𝑛) ∈ V)
181	10	adantl 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝐹 ∧ 𝑘 = (𝐹‘𝑛)) → 𝐵 = 𝐶)
182	180, 181	csbied 3095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝐹 → ⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶)
183	176, 182	eqtrd 2203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶)
184	183	ifeq1d 3543	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝐹 → if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, 𝐶, 0))
185	184	mpteq2dv 4080	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))
186	185	seqeq3d 10409	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0))))
187	186	fveq1d 5498	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))
188	187	eqeq2d 2182	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀)))
189	174, 188	anbi12d 470	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, 𝐶, 0)))‘𝑀))))
190	189	spcegv 2818	. . . . . . . . . . . 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 5861	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
193		f1oeq2 5432	. . . . . . . . . . . . . . 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 3993	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑚 = 𝑀 → (𝑛 ≤ 𝑚 ↔ 𝑛 ≤ 𝑀))
196	195	ifbid 3547	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑀 → if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
197	196	mpteq2dv 4080	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑀 → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
198	197	seqeq3d 10409	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
199		id 19	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
200	198, 199	fveq12d 5503	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))
201	200	eqeq2d 2182	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → ((seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀)))
202	194, 201	anbi12d 470	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
203	202	exbidv 1818	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑀))))
204	203	rspcev 2834	. . . . . . . . . . 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 409	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
206	205	olcd 729	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
207	206	adantr 274	. . . . . . . 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 3993	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
209	208	3anbi3d 1313	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
210	209	rexbidv 2471	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))))
211		eqeq1 2177	. . . . . . . . . . . . 13 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) ↔ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
212	211	anbi2d 461	. . . . . . . . . . . 12 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
213	212	exbidv 1818	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
214	213	rexbidv 2471	. . . . . . . . . 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 788	. . . . . . . . 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 2911	. . . . . . . 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 1234	. . . . . . 7 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) → 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
218	217	ex 114	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) → 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
219	206, 215	syl5ibrcom 156	. . . . . 6 ⊢ (𝜑 → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))))
220	218, 219	impbid 128	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
221	220	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀)))
222	221	iota5 5180	. . 3 ⊢ ((𝜑 ∧ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀) ∈ ℂ) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
223	44, 222	mpdan 419	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))
224	1, 223	eqtrid 2215	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑀, (𝐺‘𝑛), 0)))‘𝑀))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 DECID wdc 829 ∧ w3a 973 = wceq 1348 ∃wex 1485 ∃*wmo 2020 ∈ wcel 2141 ∀wral 2448 ∃wrex 2449 Vcvv 2730 ⦋csb 3049 ⊆ wss 3121 ifcif 3526 class class class wbr 3989 ↦ cmpt 4050 ℩cio 5158 ⟶wf 5194 –1-1-onto→wf1o 5197 ‘cfv 5198 (class class class)co 5853 Fincfn 6718 ℂcc 7772 0cc0 7774 1c1 7775 + caddc 7777 ≤ cle 7955 ℕcn 8878 ℕ₀cn0 9135 ℤcz 9212 ℤ_≥cuz 9487 ...cfz 9965 seqcseq 10401 ♯chash 10709 ⇝ cli 11241 Σcsu 11316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-oadd 6399 df-er 6513 df-en 6719 df-dom 6720 df-fin 6721 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-seqfrec 10402 df-exp 10476 df-ihash 10710 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-clim 11242 df-sumdc 11317

This theorem is referenced by: isumz 11352 fsumf1o 11353 fsumcl2lem 11361 fsumadd 11369 sumsnf 11372 fsummulc2 11411

W3C validator