zsumdc - Intuitionistic Logic Explorer

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

Theorem zsumdc 11950

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 1021	. . . . . . . 8 ⊢ ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
2		eleq1w 2292	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
3		csbeq1 3130	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
4	2, 3	ifbieq1d 3628	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑖 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 0))
5	4	cbvmptv 4185	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑖 ∈ ℤ ↦ if(𝑖 ∈ 𝐴, ⦋𝑖 / 𝑘⦌𝐵, 0))
6		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
7		zisum.5	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
8	7	ralrimiva 2605	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
9	8	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
10		nfcsb1v 3160	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵
11	10	nfel1 2385	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ
12		csbeq1a 3136	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑘⦌𝐵)
13	12	eleq1d 2300	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑖 → (𝐵 ∈ ℂ ↔ ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
14	11, 13	rspc 2904	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ))
15	6, 9, 14	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
16		simplr 529	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑚 ∈ ℤ)
17		zisum.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
18	17	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝑀 ∈ ℤ)
19		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑚))
20		zisum.3	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
21		zisum.1	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑀)
22	20, 21	sseqtrdi 3275	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))
23	22	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → 𝐴 ⊆ (ℤ_≥‘𝑀))
24		zisum.dc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴)
25	21	raleqi 2734	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 ∈ 𝑍 DECID 𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴)
26	24, 25	sylib 122	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴)
27		eleq1w 2292	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑖 → (𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴))
28	27	dcbid 845	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑖 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑖 ∈ 𝐴))
29	28	cbvralv 2767	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
30	26, 29	sylib 122	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑖 ∈ (ℤ_≥‘𝑀)DECID 𝑖 ∈ 𝐴)
31	30	r19.21bi 2620	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
32	31	adantlr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
33	32	adantlr 477	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
34	33	adantlr 477	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
35		simp-4l 543	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → 𝜑)
36		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ (ℤ_≥‘𝑀))
37	22	ssneld 3229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ 𝑖 ∈ (ℤ_≥‘𝑀) → ¬ 𝑖 ∈ 𝐴))
38	35, 36, 37	sylc 62	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → ¬ 𝑖 ∈ 𝐴)
39	38	olcd 741	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
40		df-dc 842	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ 𝐴 ↔ (𝑖 ∈ 𝐴 ∨ ¬ 𝑖 ∈ 𝐴))
41	39, 40	sylibr 134	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) ∧ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
42		eluzelz 9765	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘𝑚) → 𝑖 ∈ ℤ)
43		eluzdc 9844	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
44	18, 42, 43	syl2an 289	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ (ℤ_≥‘𝑀))
45		exmiddc 843	. . . . . . . . . . . . 13 ⊢ (DECID 𝑖 ∈ (ℤ_≥‘𝑀) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
46	44, 45	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → (𝑖 ∈ (ℤ_≥‘𝑀) ∨ ¬ 𝑖 ∈ (ℤ_≥‘𝑀)))
47	34, 41, 46	mpjaodan 805	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) ∧ 𝑖 ∈ (ℤ_≥‘𝑚)) → DECID 𝑖 ∈ 𝐴)
48	5, 15, 16, 18, 19, 23, 47, 33	sumrbdc 11945	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
49	48	biimpd 144	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℤ) ∧ 𝐴 ⊆ (ℤ_≥‘𝑚)) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
50	49	expimpd 363	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
51	1, 50	syl5 32	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
52	51	rexlimdva 2650	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
53		uzssz 9776	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
54	22, 53	sstrdi 3239	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ⊆ ℤ)
55	54	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ⊆ ℤ)
56		1zzd 9506	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 1 ∈ ℤ)
57		simplr 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℕ)
58	57	nnzd 9601	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑚 ∈ ℤ)
59	56, 58	fzfigd 10694	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ∈ Fin)
60		simpr 110	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
61		f1oeng 6930	. . . . . . . . . . . . . . 15 ⊢ (((1...𝑚) ∈ Fin ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
62	59, 60, 61	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (1...𝑚) ≈ 𝐴)
63	62	ensymd 6957	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ≈ (1...𝑚))
64		enfii 7061	. . . . . . . . . . . . 13 ⊢ (((1...𝑚) ∈ Fin ∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin)
65	59, 63, 64	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝐴 ∈ Fin)
66		zfz1iso 11106	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
67	55, 65, 66	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → ∃𝑔 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
68		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴)
69	8	ad3antrrr 492	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
70	68, 69, 14	sylc 62	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ 𝐴) → ⦋𝑖 / 𝑘⦌𝐵 ∈ ℂ)
71	31	adantlr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
72	71	adantlr 477	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) ∧ 𝑖 ∈ (ℤ_≥‘𝑀)) → DECID 𝑖 ∈ 𝐴)
73		breq1 4091	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
74		fveq2 5639	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
75	74	csbeq1d 3134	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
76		csbco 3137	. . . . . . . . . . . . . . . . . 18 ⊢ ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵
77	75, 76	eqtr4di 2282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵)
78	73, 77	ifbieq1d 3628	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
79	78	cbvmptv 4185	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), ⦋(𝑓‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
80		eqid 2231	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑚, ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ 𝑚, ⦋(𝑔‘𝑗) / 𝑖⦌⦋𝑖 / 𝑘⦌𝐵, 0))
81		simplr 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ)
82	17	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑀 ∈ ℤ)
83	22	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ_≥‘𝑀))
84	60	adantrr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
85		simprr 533	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))
86	5, 70, 72, 79, 80, 81, 82, 83, 84, 85	summodclem2a 11947	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
87	59	adantrr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (1...𝑚) ∈ Fin)
88	87, 84	fihasheqf1od 11052	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = (♯‘𝐴))
89	81	nnnn0d 9455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ₀)
90		hashfz1 11046	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 ∈ ℕ₀ → (♯‘(1...𝑚)) = 𝑚)
91	89, 90	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘(1...𝑚)) = 𝑚)
92	88, 91	eqtr3d 2266	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (♯‘𝐴) = 𝑚)
93	92	breq2d 4100	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ≤ (♯‘𝐴) ↔ 𝑛 ≤ 𝑚))
94	93	ifbid 3627	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0) = if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))
95	94	mpteq2dv 4180	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))
96	95	seqeq3d 10718	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0))))
97	96	fveq1d 5641	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
98	86, 97	breqtrd 4114	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))
99	98	expr 375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑔 Isom < , < ((1...(♯‘𝐴)), 𝐴) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
100	99	exlimdv 1867	. . . . . . . . . . 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 4092	. . . . . . . . . 10 ⊢ (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))
103	101, 102	syl5ibrcom 157	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
104	103	expimpd 363	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
105	104	exlimdv 1867	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
106	105	rexlimdva 2650	. . . . . 6 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
107	52, 106	jaod 724	. . . . 5 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
108	17	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → 𝑀 ∈ ℤ)
109	22	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → 𝐴 ⊆ (ℤ_≥‘𝑀))
110		eleq1w 2292	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝑥 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
111	110	dcbid 845	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑗 ∈ 𝐴))
112	111	cbvralv 2767	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
113	26, 112	sylib 122	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
114	113	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴)
115		simpr 110	. . . . . . . 8 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)
116		fveq2 5639	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → (ℤ_≥‘𝑚) = (ℤ_≥‘𝑀))
117	116	sseq2d 3257	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (𝐴 ⊆ (ℤ_≥‘𝑚) ↔ 𝐴 ⊆ (ℤ_≥‘𝑀)))
118	116	raleqdv 2736	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ↔ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴))
119		seqeq1 10713	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑀 → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))))
120	119	breq1d 4098	. . . . . . . . . 10 ⊢ (𝑚 = 𝑀 → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
121	117, 118, 120	3anbi123d 1348	. . . . . . . . 9 ⊢ (𝑚 = 𝑀 → ((𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)))
122	121	rspcev 2910	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ (𝐴 ⊆ (ℤ_≥‘𝑀) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑀)DECID 𝑗 ∈ 𝐴 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥)) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
123	108, 109, 114, 115, 122	syl13anc 1275	. . . . . . 7 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
124	123	orcd 740	. . . . . 6 ⊢ ((𝜑 ∧ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
125	124	ex 115	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))))
126	107, 125	impbid 129	. . . 4 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥))
127		eluzelz 9765	. . . . . . . 8 ⊢ (𝑎 ∈ (ℤ_≥‘𝑀) → 𝑎 ∈ ℤ)
128		simpr 110	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴)
129	8	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
130		nfcsb1v 3160	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑎 / 𝑘⦌𝐵
131	130	nfel1 2385	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ
132		csbeq1a 3136	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑘⦌𝐵)
133	132	eleq1d 2300	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑎 → (𝐵 ∈ ℂ ↔ ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ))
134	131, 133	rspc 2904	. . . . . . . . . 10 ⊢ (𝑎 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ))
135	128, 129, 134	sylc 62	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ 𝑎 ∈ 𝐴) → ⦋𝑎 / 𝑘⦌𝐵 ∈ ℂ)
136		0cnd 8172	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑎 ∈ 𝐴) → 0 ∈ ℂ)
137		eleq1w 2292	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
138	137	dcbid 845	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑎 ∈ 𝐴))
139	138	cbvralv 2767	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (ℤ_≥‘𝑀)DECID 𝑥 ∈ 𝐴 ↔ ∀𝑎 ∈ (ℤ_≥‘𝑀)DECID 𝑎 ∈ 𝐴)
140	26, 139	sylib 122	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ (ℤ_≥‘𝑀)DECID 𝑎 ∈ 𝐴)
141	140	r19.21bi 2620	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → DECID 𝑎 ∈ 𝐴)
142	135, 136, 141	ifcldadc 3635	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0) ∈ ℂ)
143		eleq1w 2292	. . . . . . . . . 10 ⊢ (𝑛 = 𝑎 → (𝑛 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
144		csbeq1 3130	. . . . . . . . . 10 ⊢ (𝑛 = 𝑎 → ⦋𝑛 / 𝑘⦌𝐵 = ⦋𝑎 / 𝑘⦌𝐵)
145	143, 144	ifbieq1d 3628	. . . . . . . . 9 ⊢ (𝑛 = 𝑎 → if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
146		eqid 2231	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
147	145, 146	fvmptg 5722	. . . . . . . 8 ⊢ ((𝑎 ∈ ℤ ∧ if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0) ∈ ℂ) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
148	127, 142, 147	syl2an2 598	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) = if(𝑎 ∈ 𝐴, ⦋𝑎 / 𝑘⦌𝐵, 0))
149	148, 142	eqeltrd 2308	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑎) ∈ ℂ)
150		simpr 110	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ (ℤ_≥‘𝑀))
151	53, 150	sselid 3225	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ ℤ)
152		vex 2805	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
153		nfv 1576	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑗 ∈ 𝐴
154		nfcsb1v 3160	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵
155		nfcv 2374	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
156	153, 154, 155	nfif 3634	. . . . . . . . . 10 ⊢ Ⅎ𝑘if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0)
157		eleq1w 2292	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴))
158		csbeq1a 3136	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵)
159	157, 158	ifbieq1d 3628	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0))
160	152, 156, 159	csbief 3172	. . . . . . . . 9 ⊢ ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0)
161		simpr 110	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴)
162	8	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
163	154	nfel1 2385	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ
164	158	eleq1d 2300	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
165	163, 164	rspc 2904	. . . . . . . . . . 11 ⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ))
166	161, 162, 165	sylc 62	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)
167		0cnd 8172	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) ∧ ¬ 𝑗 ∈ 𝐴) → 0 ∈ ℂ)
168	113	r19.21bi 2620	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → DECID 𝑗 ∈ 𝐴)
169	166, 167, 168	ifcldadc 3635	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 0) ∈ ℂ)
170	160, 169	eqeltrid 2318	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ)
171		nfcv 2374	. . . . . . . . . . 11 ⊢ Ⅎ𝑛if(𝑘 ∈ 𝐴, 𝐵, 0)
172		nfv 1576	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘 𝑛 ∈ 𝐴
173		nfcsb1v 3160	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘⦋𝑛 / 𝑘⦌𝐵
174	172, 173, 155	nfif 3634	. . . . . . . . . . 11 ⊢ Ⅎ𝑘if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)
175		eleq1w 2292	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ 𝐴 ↔ 𝑛 ∈ 𝐴))
176		csbeq1a 3136	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → 𝐵 = ⦋𝑛 / 𝑘⦌𝐵)
177	175, 176	ifbieq1d 3628	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑛 → if(𝑘 ∈ 𝐴, 𝐵, 0) = if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
178	171, 174, 177	cbvmpt 4184	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))
179	178	eqcomi 2235	. . . . . . . . 9 ⊢ (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
180	179	fvmpts 5724	. . . . . . . 8 ⊢ ((𝑗 ∈ ℤ ∧ ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℂ) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
181	151, 170, 180	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
182	150, 21	eleqtrrdi 2325	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → 𝑗 ∈ 𝑍)
183		zisum.4	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
184	183	ralrimiva 2605	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
185	184	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
186		nfcsb1v 3160	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)
187	186	nfeq2 2386	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)
188		fveq2 5639	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗))
189		csbeq1a 3136	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 0) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
190	188, 189	eqeq12d 2246	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0) ↔ (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)))
191	187, 190	rspc 2904	. . . . . . . 8 ⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0) → (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0)))
192	182, 185, 191	sylc 62	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑗) = ⦋𝑗 / 𝑘⦌if(𝑘 ∈ 𝐴, 𝐵, 0))
193	181, 192	eqtr4d 2267	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝑀)) → ((𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))‘𝑗) = (𝐹‘𝑗))
194		addcl 8157	. . . . . . 7 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ)
195	194	adantl 277	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 + 𝑏) ∈ ℂ)
196	17, 149, 193, 195	seq3feq 10743	. . . . 5 ⊢ (𝜑 → seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) = seq𝑀( + , 𝐹))
197	196	breq1d 4098	. . . 4 ⊢ (𝜑 → (seq𝑀( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥 ↔ seq𝑀( + , 𝐹) ⇝ 𝑥))
198	126, 197	bitrd 188	. . 3 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))) ↔ seq𝑀( + , 𝐹) ⇝ 𝑥))
199	198	iotabidv 5309	. 2 ⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚)))) = (℩𝑥seq𝑀( + , 𝐹) ⇝ 𝑥))
200		df-sumdc 11919	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ_≥‘𝑚) ∧ ∀𝑗 ∈ (ℤ_≥‘𝑚)DECID 𝑗 ∈ 𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ 𝑚, ⦋(𝑓‘𝑛) / 𝑘⦌𝐵, 0)))‘𝑚))))
201		df-fv 5334	. 2 ⊢ ( ⇝ ‘seq𝑀( + , 𝐹)) = (℩𝑥seq𝑀( + , 𝐹) ⇝ 𝑥)
202	199, 200, 201	3eqtr4g 2289	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = ( ⇝ ‘seq𝑀( + , 𝐹)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 715 DECID wdc 841 ∧ w3a 1004 = wceq 1397 ∃wex 1540 ∈ wcel 2202 ∀wral 2510 ∃wrex 2511 ⦋csb 3127 ⊆ wss 3200 ifcif 3605 class class class wbr 4088 ↦ cmpt 4150 ℩cio 5284 –1-1-onto→wf1o 5325 ‘cfv 5326 Isom wiso 5327 (class class class)co 6018 ≈ cen 6907 Fincfn 6909 ℂcc 8030 0cc0 8032 1c1 8033 + caddc 8035 < clt 8214 ≤ cle 8215 ℕcn 9143 ℕ₀cn0 9402 ℤcz 9479 ℤ_≥cuz 9755 ...cfz 10243 seqcseq 10710 ♯chash 11038 ⇝ cli 11843 Σcsu 11918

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4204 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 ax-cnex 8123 ax-resscn 8124 ax-1cn 8125 ax-1re 8126 ax-icn 8127 ax-addcl 8128 ax-addrcl 8129 ax-mulcl 8130 ax-mulrcl 8131 ax-addcom 8132 ax-mulcom 8133 ax-addass 8134 ax-mulass 8135 ax-distr 8136 ax-i2m1 8137 ax-0lt1 8138 ax-1rid 8139 ax-0id 8140 ax-rnegex 8141 ax-precex 8142 ax-cnre 8143 ax-pre-ltirr 8144 ax-pre-ltwlin 8145 ax-pre-lttrn 8146 ax-pre-apti 8147 ax-pre-ltadd 8148 ax-pre-mulgt0 8149 ax-pre-mulext 8150

This theorem depends on definitions: df-bi 117 df-dc 842 df-3or 1005 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-nel 2498 df-ral 2515 df-rex 2516 df-reu 2517 df-rmo 2518 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-if 3606 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-po 4393 df-iso 4394 df-iord 4463 df-on 4465 df-ilim 4466 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-f1 5331 df-fo 5332 df-f1o 5333 df-fv 5334 df-isom 5335 df-riota 5971 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1st 6303 df-2nd 6304 df-recs 6471 df-irdg 6536 df-frec 6557 df-1o 6582 df-oadd 6586 df-er 6702 df-en 6910 df-dom 6911 df-fin 6912 df-pnf 8216 df-mnf 8217 df-xr 8218 df-ltxr 8219 df-le 8220 df-sub 8352 df-neg 8353 df-reap 8755 df-ap 8762 df-div 8853 df-inn 9144 df-2 9202 df-n0 9403 df-z 9480 df-uz 9756 df-q 9854 df-rp 9889 df-fz 10244 df-fzo 10378 df-seqfrec 10711 df-exp 10802 df-ihash 11039 df-cj 11407 df-rsqrt 11563 df-abs 11564 df-clim 11844 df-sumdc 11919

This theorem is referenced by: isum 11951 sum0 11954 isumz 11955 isumss 11957 fsumsersdc 11961

W3C validator