Theorem summo 15735

Description: A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
summo.1	⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
summo.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
summo.3	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)

Assertion

Ref	Expression
summo	⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))

Distinct variable groups:   𝑓,𝑘,𝑚,𝑛,𝑥,𝐴   𝑓,𝐹,𝑘,𝑚,𝑛,𝑥   𝑘,𝐺,𝑚,𝑛,𝑥   𝜑,𝑘,𝑚,𝑛   𝐵,𝑓,𝑚,𝑛,𝑥   𝜑,𝑥,𝑓

Allowed substitution hints:   𝐵(𝑘)   𝐺(𝑓)

Proof of Theorem summo

Dummy variables 𝑔 𝑗 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6862	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (ℤ≥‘𝑚) = (ℤ≥‘𝑛))
2	1	sseq2d 3966	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑛)))
3		seqeq1 14011	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
4	3	breq1d 5107	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
5	2, 4	anbi12d 641	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
6	5	cbvrexvw 3240	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
7		reeanv 3233	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
8		simprlr 789	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
9		summo.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
10		summo.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
11	10	ad4ant14 762	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
12		simplrl 786	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
13		simplrr 787	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
14		simprll 788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ≥‘𝑚))
15		simprrl 790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ≥‘𝑛))
16	9, 11, 12, 13, 14, 15	sumrb 15731	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
17	8, 16	mpbid 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
18		simprrr 791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
19		climuni 15570	. . . . . . . . . . . 12 ⊢ ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
20	17, 18, 19	syl2anc 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
21	20	exp31 423	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
22	21	rexlimdvv 3217	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
23	7, 22	biimtrrid 245	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
24	23	expdimp 456	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
25	6, 24	biimtrid 244	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
26		summo.3	. . . . . . 7 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
27	9, 10, 26	summolem2 15734	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
28	25, 27	jaod 870	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
29	9, 10, 26	summolem2 15734	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
30		equcom 2037	. . . . . . . 8 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
31	29, 30	imbitrdi 253	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
32	31	impancom 455	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
33		oveq2 7399	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
34	33	f1oeq2d 6797	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴))
35		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
36	35	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
37	34, 36	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
38	37	exbidv 1940	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
39		f1oeq1 6789	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑛)–1-1-onto→𝐴))
40		fveq1 6861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑛) = (𝑔‘𝑛))
41	40	csbeq1d 3854	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑛) / 𝑘⦌𝐵)
42	41	mpteq2dv 5191	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))
43	26, 42	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))
44	43	seqeq3d 14016	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵)))
45	44	fveq1d 6864	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))
46	45	eqeq2d 2772	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
47	39, 46	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
48	47	cbvexvw 2056	. . . . . . . . 9 ⊢ (∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
49	38, 48	bitrdi 289	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
50	49	cbvrexvw 3240	. . . . . . 7 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
51		reeanv 3233	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
52		exdistrv 1974	. . . . . . . . . . 11 ⊢ (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
53		an4 666	. . . . . . . . . . . . 13 ⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
54	10	ad4ant14 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
55		fveq2 6862	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
56	55	csbeq1d 3854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
57	56	cbvmptv 5201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
58	26, 57	eqtri 2784	. . . . . . . . . . . . . . . 16 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
59		fveq2 6862	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
60	59	csbeq1d 3854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → ⦋(𝑔‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
61	60	cbvmptv 5201	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
62		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ))
63		simprl 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
64		simprr 782	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑔:(1...𝑛)–1-1-onto→𝐴)
65	9, 54, 58, 61, 62, 63, 64	summolem3 15732	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))
66		eqeq12 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
67	65, 66	syl5ibrcom 249	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → 𝑥 = 𝑦))
68	67	expimpd 457	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
69	53, 68	biimtrid 244	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
70	69	exlimdvv 1953	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
71	52, 70	biimtrrid 245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
72	71	rexlimdvva 3218	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
73	51, 72	biimtrrid 245	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
74	73	expdimp 456	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → 𝑥 = 𝑦))
75	50, 74	biimtrid 244	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
76	32, 75	jaod 870	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
77	28, 76	jaodan 970	. . . 4 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
78	77	expimpd 457	. . 3 ⊢ (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
79	78	alrimivv 1947	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
80		breq2 5101	. . . . . 6 ⊢ (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
81	80	anbi2d 639	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
82	81	rexbidv 3185	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
83		eqeq1 2765	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
84	83	anbi2d 639	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
85	84	exbidv 1940	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
86	85	rexbidv 3185	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
87	82, 86	orbi12d 929	. . 3 ⊢ (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))))
88	87	mo4 2592	. 2 ⊢ (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
89	79, 88	sylibr 236	1 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃*wmo 2563  ∃wrex 3085  ⦋csb 3850   ⊆ wss 3902  ifcif 4477   class class class wbr 5097   ↦ cmpt 5178  –1-1-onto→wf1o 6515  ‘cfv 6516  (class class class)co 7391  ℂcc 11065  0cc0 11067  1c1 11068   + caddc 11070  ℕcn 12204  ℤcz 12562  ℤ_≥cuz 12833  ...cfz 13506  seqcseq 14008   ⇝ cli 15502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-inf2 9590  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144  ax-pre-sup 11145

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-1st 7965  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-1o 8431  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9382  df-oi 9452  df-card 9891  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-div 11839  df-nn 12205  df-2 12274  df-3 12275  df-n0 12476  df-z 12563  df-uz 12834  df-rp 12988  df-fz 13507  df-fzo 13654  df-seq 14009  df-exp 14069  df-hash 14338  df-cj 15117  df-re 15118  df-im 15119  df-sqrt 15253  df-abs 15254  df-clim 15506

This theorem is referenced by:  fsum  15738