zsumdc - Intuitionistic Logic Explorer

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

Theorem zsumdc 11325

Description: Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim Kingdon, 8-Apr-2023.)

**Hypotheses**
Ref	Expression
zisum.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
zisum.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
zisum.3	⊢ (𝜑 → 𝐴 ⊆ 𝑍)
zisum.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
zisum.dc	⊢ (𝜑 → ∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴)
zisum.5	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)

**Assertion**
Ref	Expression
zsumdc	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))

Distinct variable groups: 𝐴,𝑘,𝑥 𝑥,𝐵 𝑘,𝐹,𝑥 𝑥,𝑀 𝑘,𝑍,𝑥 𝜑,𝑘,𝑥 Allowed substitution hints: 𝐵(𝑘) 𝑀(𝑘)

Proof of Theorem zsumdc Dummy variables 𝑎 𝑏 𝑗 𝑛 𝑓 𝑔 𝑖 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		3simpb 985	. . . . . . . 8 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
2		eleq1w 2227	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
3		csbeq1 3048	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
4	2, 3	ifbieq1d 3542	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 0))
5	4	cbvmptv 4078	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 0))
6		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
7		zisum.5	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
8	7	ralrimiva 2539	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
9	8	ad3antrrr 484	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
10		nfcsb1v 3078	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
11	10	nfel1 2319	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
12		csbeq1a 3054	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
13	12	eleq1d 2235	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
14	11, 13	rspc 2824	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
15	6, 9, 14	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
16		simplr 520	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
17		zisum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
18	17	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
19		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
20		zisum.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
21		zisum.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
22	20, 21	sseqtrdi 3190	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
23	22	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
24		zisum.dc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴)
25	21	raleqi 2665	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴)
26	24, 25	sylib 121	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴)
27		eleq1w 2227	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑖 → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
28	27	dcbid 828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑖 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑖 ∈ 𝐴))
29	28	cbvralv 2692	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
30	26, 29	sylib 121	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
31	30	r19.21bi 2554	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
32	31	adantlr 469	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
33	32	adantlr 469	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
34	33	adantlr 469	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
35		simp-4l 531	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝜑)
36		simpr 109	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ (ℤ_≥‘𝑀))
37	22	ssneld 3144	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ 𝑖 ∈ (ℤ_≥‘𝑀) → ¬ 𝑖 ∈ 𝐴))
38	35, 36, 37	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ 𝐴)
39	38	olcd 724	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
40		df-dc 825	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ 𝐴 ↔ (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
41	39, 40	sylibr 133	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
42		eluzelz 9475	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘𝑚) → 𝑖 ∈ ℤ)
43		eluzdc 9548	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
44	18, 42, 43	syl2an 287	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
45		exmiddc 826	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ (ℤ_≥‘𝑀) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
46	44, 45	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
47	34, 41, 46	mpjaodan 788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ 𝐴)
48	5, 15, 16, 18, 19, 23, 47, 33	sumrbdc 11320	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
49	48	biimpd 143	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
50	49	expimpd 361	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
51	1, 50	syl5 32	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
52	51	rexlimdva 2583	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
53		uzssz 9485	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
54	22, 53	sstrdi 3154	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
55	54	ad2antrr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℤ)
56		1zzd 9218	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
57		simplr 520	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ)
58	57	nnzd 9312	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
59	56, 58	fzfigd 10366	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
60		simpr 109	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
61		f1oeng 6723	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
62	59, 60, 61	syl2anc 409	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
63	62	ensymd 6749	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
64		enfii 6840	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
65	59, 63, 64	syl2anc 409	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
66		zfz1iso 10754	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
67	55, 65, 66	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
68		simpr 109	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
69	8	ad3antrrr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
70	68, 69, 14	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
71	31	adantlr 469	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
72	71	adantlr 469	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
73		breq1 3985	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
74		fveq2 5486	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
75	74	csbeq1d 3052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
76		csbco 3055	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
77	75, 76	eqtr4di 2217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
78	73, 77	ifbieq1d 3542	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
79	78	cbvmptv 4078	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
80		eqid 2165	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑚, ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑚, ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
81		simplr 520	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
82	17	ad2antrr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
83	22	ad2antrr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
84	60	adantrr 471	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
85		simprr 522	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
86	5, 70, 72, 79, 80, 81, 82, 83, 84, 85	summodclem2a 11322	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
87	59	adantrr 471	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
88	87, 84	fihasheqf1od 10703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
89	81	nnnn0d 9167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ₀)
90		hashfz1 10696	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
91	89, 90	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
92	88, 91	eqtr3d 2200	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
93	92	breq2d 3994	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
94	93	ifbid 3541	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
95	94	mpteq2dv 4073	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
96	95	seqeq3d 10388	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
97	96	fveq1d 5488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
98	86, 97	breqtrd 4008	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
99	98	expr 373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
100	99	exlimdv 1807	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
101	67, 100	mpd 13	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
102		breq2 3986	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
103	101, 102	syl5ibrcom 156	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
104	103	expimpd 361	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
105	104	exlimdv 1807	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
106	105	rexlimdva 2583	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
107	52, 106	jaod 707	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
108	17	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
109	22	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → 𝐴 ⊆ (ℤ_≥‘𝑀))
110		eleq1w 2227	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝑥 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
111	110	dcbid 828	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
112	111	cbvralv 2692	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
113	26, 112	sylib 121	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
114	113	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
115		simpr 109	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
116		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
117	116	sseq2d 3172	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑀)))
118	116	raleqdv 2667	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴))
119		seqeq1 10383	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))))
120	119	breq1d 3992	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
121	117, 118, 120	3anbi123d 1302	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)))
122	121	rspcev 2830	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
123	108, 109, 114, 115, 122	syl13anc 1230	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
124	123	orcd 723	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
125	124	ex 114	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))))
126	107, 125	impbid 128	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
127		eluzelz 9475	. . . . . . . 8 ⊢ (𝑎 ∈ (ℤ_≥‘𝑀) → 𝑎 ∈ ℤ)
128		simpr 109	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴)
129	8	ad2antrr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3078	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑎 / 𝑘⦌𝐵
131	130	nfel1 2319	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3054	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑘⦌𝐵)
133	132	eleq1d 2235	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑎 → (𝐵 ∈ ℂ ↔ ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2824	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ))
135	128, 129, 134	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ)
136		0cnd 7892	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑎 ∈ 𝐴) → 0 ∈ ℂ)
137		eleq1w 2227	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
138	137	dcbid 828	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑎 ∈ 𝐴))
139	138	cbvralv 2692	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑎 ∈ (ℤ_≥‘𝑀)DECID 𝑎 ∈ 𝐴)
140	26, 139	sylib 121	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘𝑀)DECID 𝑎 ∈ 𝐴)
141	140	r19.21bi 2554	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → DECID 𝑎 ∈ 𝐴)
142	135, 136, 141	ifcldadc 3549	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0) ∈ ℂ)
143		eleq1w 2227	. . . . . . . . . 10 ⊢ (𝑛 = 𝑎 → (𝑛 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
144		csbeq1 3048	. . . . . . . . . 10 ⊢ (𝑛 = 𝑎 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑎 / 𝑘⦌𝐵)
145	143, 144	ifbieq1d 3542	. . . . . . . . 9 ⊢ (𝑛 = 𝑎 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
146		eqid 2165	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
147	145, 146	fvmptg 5562	. . . . . . . 8 ⊢ ((𝑎 ∈ ℤ ∧ if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0) ∈ ℂ) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
148	127, 142, 147	syl2an2 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
149	148, 142	eqeltrd 2243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) ∈ ℂ)
150		simpr 109	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
151	53, 150	sselid 3140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℤ)
152		vex 2729	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
153		nfv 1516	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑗 ∈ 𝐴
154		nfcsb1v 3078	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
155		nfcv 2308	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
156	153, 154, 155	nfif 3548	. . . . . . . . . 10 ⊢ Ⅎ𝑘if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0)
157		eleq1w 2227	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
158		csbeq1a 3054	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
159	157, 158	ifbieq1d 3542	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
160	152, 156, 159	csbief 3089	. . . . . . . . 9 ⊢ ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0)
161		simpr 109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴)
162	8	ad2antrr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
163	154	nfel1 2319	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
164	158	eleq1d 2235	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
165	163, 164	rspc 2824	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
166	161, 162, 165	sylc 62	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
167		0cnd 7892	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑗 ∈ 𝐴) → 0 ∈ ℂ)
168	113	r19.21bi 2554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → DECID 𝑗 ∈ 𝐴)
169	166, 167, 168	ifcldadc 3549	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0) ∈ ℂ)
170	160, 169	eqeltrid 2253	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
171		nfcv 2308	. . . . . . . . . . 11 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
172		nfv 1516	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
173		nfcsb1v 3078	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
174	172, 173, 155	nfif 3548	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
175		eleq1w 2227	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
176		csbeq1a 3054	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
177	175, 176	ifbieq1d 3542	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
178	171, 174, 177	cbvmpt 4077	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
179	178	eqcomi 2169	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
180	179	fvmpts 5564	. . . . . . . 8 ⊢ ((𝑗 ∈ ℤ ∧ ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
181	151, 170, 180	syl2anc 409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
182	150, 21	eleqtrrdi 2260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ 𝑍)
183		zisum.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
184	183	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
185	184	adantr 274	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
186		nfcsb1v 3078	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)
187	186	nfeq2 2320	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)
188		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
189		csbeq1a 3054	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 0) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
190	188, 189	eqeq12d 2180	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0) ↔ (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)))
191	187, 190	rspc 2824	. . . . . . . 8 ⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0) → (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)))
192	182, 185, 191	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
193	181, 192	eqtr4d 2201	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = (𝐹‘𝑗))
194		addcl 7878	. . . . . . 7 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ)
195	194	adantl 275	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 + 𝑏) ∈ ℂ)
196	17, 149, 193, 195	seq3feq 10407	. . . . 5 ⊢ (𝜑 → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑀( + , 𝐹))
197	196	breq1d 3992	. . . 4 ⊢ (𝜑 → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , 𝐹) ⇝ 𝑥))
198	126, 197	bitrd 187	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ seq𝑀( + , 𝐹) ⇝ 𝑥))
199	198	iotabidv 5174	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (℩𝑥seq𝑀( + , 𝐹) ⇝ 𝑥))
200		df-sumdc 11295	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
201		df-fv 5196	. 2 ⊢ ( ⇝ ‘seq𝑀( + , 𝐹)) = (℩𝑥seq𝑀( + , 𝐹) ⇝ 𝑥)
202	199, 200, 201	3eqtr4g 2224	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 698 DECID wdc 824 ∧ w3a 968 = wceq 1343 ∃wex 1480 ∈ wcel 2136 ∀wral 2444 ∃wrex 2445 ⦋csb 3045 ⊆ wss 3116 ifcif 3520 class class class wbr 3982 ↦ cmpt 4043 ℩cio 5151 –1-1-onto→wf1o 5187 ‘cfv 5188 Isom wiso 5189 (class class class)co 5842 ≈ cen 6704 Fincfn 6706 ℂcc 7751 0cc0 7753 1c1 7754 + caddc 7756 < clt 7933 ≤ cle 7934 ℕcn 8857 ℕ₀cn0 9114 ℤcz 9191 ℤ_≥cuz 9466 ...cfz 9944 seqcseq 10380 ♯chash 10688 ⇝ cli 11219 Σcsu 11294

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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-oadd 6388 df-er 6501 df-en 6707 df-dom 6708 df-fin 6709 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-fz 9945 df-fzo 10078 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-sumdc 11295

This theorem is referenced by: isum 11326 sum0 11329 isumz 11330 isumss 11332 fsumsersdc 11336

W3C validator