Theorem summo 14674

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 6411	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (ℤ≥‘𝑚) = (ℤ≥‘𝑛))
2	1	sseq2d 3837	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑛)))
3		seqeq1 13030	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
4	3	breq1d 4861	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
5	2, 4	anbi12d 618	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
6	5	cbvrexv 3368	. . . . . . 7 ⊢ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))
7		reeanv 3302	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
8		simprlr 789	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑚( + , 𝐹) ⇝ 𝑥)
9		summo.1	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0))
10		simpll 774	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝜑)
11		summo.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
12	10, 11	sylan 571	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
13		simplrl 786	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑚 ∈ ℤ)
14		simplrr 787	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑛 ∈ ℤ)
15		simprll 788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ≥‘𝑚))
16		simprrl 790	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ≥‘𝑛))
17	9, 12, 13, 14, 15, 16	sumrb 14670	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
18	8, 17	mpbid 223	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
19		simprrr 791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
20		climuni 14509	. . . . . . . . . . . 12 ⊢ ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
21	18, 19, 20	syl2anc 575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
22	21	exp31 408	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
23	22	rexlimdvv 3232	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
24	7, 23	syl5bir 234	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
25	24	expdimp 442	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
26	6, 25	syl5bi 233	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
27		summo.3	. . . . . . 7 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
28	9, 11, 27	summolem2 14673	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
29	26, 28	jaod 877	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
30	9, 11, 27	summolem2 14673	. . . . . . . 8 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
31		equcom 2115	. . . . . . . 8 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
32	30, 31	syl6ib 242	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
33	32	impancom 441	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
34		oveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
35		f1oeq2 6347	. . . . . . . . . . . 12 ⊢ ((1...𝑚) = (1...𝑛) → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴))
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑛)–1-1-onto→𝐴))
37		fveq2 6411	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
38	37	eqeq2d 2823	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
39	36, 38	anbi12d 618	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
40	39	exbidv 2012	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛))))
41		f1oeq1 6346	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑓:(1...𝑛)–1-1-onto→𝐴 ↔ 𝑔:(1...𝑛)–1-1-onto→𝐴))
42		fveq1 6410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑛) = (𝑔‘𝑛))
43	42	csbeq1d 3742	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑔 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑛) / 𝑘⦌𝐵)
44	43	mpteq2dv 4946	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))
45	27, 44	syl5eq 2859	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))
46	45	seqeq3d 13035	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵)))
47	46	fveq1d 6413	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))
48	47	eqeq2d 2823	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
49	41, 48	anbi12d 618	. . . . . . . . . 10 ⊢ (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
50	49	cbvexvw 2138	. . . . . . . . 9 ⊢ (∃𝑓(𝑓:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
51	40, 50	syl6bb 278	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
52	51	cbvrexv 3368	. . . . . . 7 ⊢ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
53		reeanv 3302	. . . . . . . . 9 ⊢ (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
54		eeanv 2358	. . . . . . . . . . 11 ⊢ (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
55		an4 638	. . . . . . . . . . . . 13 ⊢ (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) ↔ ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))))
56		simpll 774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝜑)
57	56, 11	sylan 571	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
58		fveq2 6411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗))
59	58	csbeq1d 3742	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
60	59	cbvmptv 4951	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
61	27, 60	eqtri 2835	. . . . . . . . . . . . . . . 16 ⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵)
62		fveq2 6411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑗 → (𝑔‘𝑛) = (𝑔‘𝑗))
63	62	csbeq1d 3742	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑗 → ⦋(𝑔‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
64	63	cbvmptv 4951	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵) = (𝑗 ∈ ℕ ↦ ⦋(𝑔‘𝑗) / 𝑘⦌𝐵)
65		simplr 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ))
66		simprl 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑓:(1...𝑚)–1-1-onto→𝐴)
67		simprr 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → 𝑔:(1...𝑛)–1-1-onto→𝐴)
68	9, 57, 61, 64, 65, 66, 67	summolem3 14671	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))
69		eqeq12 2826	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)))
70	68, 69	syl5ibrcom 238	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → 𝑥 = 𝑦))
71	70	expimpd 443	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑔:(1...𝑛)–1-1-onto→𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
72	55, 71	syl5bi 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
73	72	exlimdvv 2025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓∃𝑔((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
74	54, 73	syl5bir 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
75	74	rexlimdvva 3233	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
76	53, 75	syl5bir 234	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛))) → 𝑥 = 𝑦))
77	76	expdimp 442	. . . . . . 7 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵))‘𝑛)) → 𝑥 = 𝑦))
78	52, 77	syl5bi 233	. . . . . 6 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
79	33, 78	jaod 877	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
80	29, 79	jaodan 971	. . . 4 ⊢ ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
81	80	expimpd 443	. . 3 ⊢ (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
82	81	alrimivv 2019	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
83		breq2 4855	. . . . . 6 ⊢ (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
84	83	anbi2d 616	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
85	84	rexbidv 3247	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
86		eqeq1 2817	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
87	86	anbi2d 616	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
88	87	exbidv 2012	. . . . 5 ⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
89	88	rexbidv 3247	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚))))
90	85, 89	orbi12d 933	. . 3 ⊢ (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))))
91	90	mo4 2687	. 2 ⊢ (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥∀𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
92	82, 91	sylibr 225	1 ⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , 𝐺)‘𝑚))))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∨ wo 865  ∀wal 1635   = wceq 1637  ∃wex 1859   ∈ wcel 2157  ∃*wmo 2633  ∃wrex 3104  ⦋csb 3735   ⊆ wss 3776  ifcif 4286   class class class wbr 4851   ↦ cmpt 4930  –1-1-onto→wf1o 6103  ‘cfv 6104  (class class class)co 6877  ℂcc 10222  0cc0 10224  1c1 10225   + caddc 10227  ℕcn 11308  ℤcz 11646  ℤ_≥cuz 11907  ...cfz 12552  seqcseq 13027   ⇝ cli 14441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-oadd 7803  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-sup 8590  df-oi 8657  df-card 9051  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-n0 11563  df-z 11647  df-uz 11908  df-rp 12050  df-fz 12553  df-fzo 12693  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445

This theorem is referenced by:  fsum  14677