MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  summo Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 fveq2 6411 . . . . . . . . . 10 (𝑚 = 𝑛 → (ℤ𝑚) = (ℤ𝑛))
21sseq2d 3837 . . . . . . . . 9 (𝑚 = 𝑛 → (𝐴 ⊆ (ℤ𝑚) ↔ 𝐴 ⊆ (ℤ𝑛)))
3 seqeq1 13030 . . . . . . . . . 10 (𝑚 = 𝑛 → seq𝑚( + , 𝐹) = seq𝑛( + , 𝐹))
43breq1d 4861 . . . . . . . . 9 (𝑚 = 𝑛 → (seq𝑚( + , 𝐹) ⇝ 𝑦 ↔ seq𝑛( + , 𝐹) ⇝ 𝑦))
52, 4anbi12d 618 . . . . . . . 8 (𝑚 = 𝑛 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ↔ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)))
65cbvrexv 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 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1210, 11sylan 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𝑛( + , 𝐹) ⇝ 𝑦))) → 𝐴 ⊆ (ℤ𝑛))
179, 12, 13, 14, 15, 16sumrb 14670 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑛( + , 𝐹) ⇝ 𝑥))
188, 17mpbid 223 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑥)
19 simprrr 791 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → seq𝑛( + , 𝐹) ⇝ 𝑦)
20 climuni 14509 . . . . . . . . . . . 12 ((seq𝑛( + , 𝐹) ⇝ 𝑥 ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦)
2118, 19, 20syl2anc 575 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ)) ∧ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦))) → 𝑥 = 𝑦)
2221exp31 408 . . . . . . . . . 10 (𝜑 → ((𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦)))
2322rexlimdvv 3232 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℤ ∃𝑛 ∈ ℤ ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
247, 23syl5bir 234 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∧ ∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦)) → 𝑥 = 𝑦))
2524expdimp 442 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑛 ∈ ℤ (𝐴 ⊆ (ℤ𝑛) ∧ seq𝑛( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
266, 25syl5bi 233 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) → 𝑥 = 𝑦))
27 summo.3 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)
289, 11, 27summolem2 14673 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
2926, 28jaod 877 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
309, 11, 27summolem2 14673 . . . . . . . 8 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑦 = 𝑥))
31 equcom 2115 . . . . . . . 8 (𝑦 = 𝑥𝑥 = 𝑦)
3230, 31syl6ib 242 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
3332impancom 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𝐴))
3634, 35syl 17 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑛)–1-1-onto𝐴))
37 fveq2 6411 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (seq1( + , 𝐺)‘𝑚) = (seq1( + , 𝐺)‘𝑛))
3837eqeq2d 2823 . . . . . . . . . . 11 (𝑚 = 𝑛 → (𝑦 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑛)))
3936, 38anbi12d 618 . . . . . . . . . 10 (𝑚 = 𝑛 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛))))
4039exbidv 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 (𝑓 = 𝑔 → (𝑓𝑛) = (𝑔𝑛))
4342csbeq1d 3742 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑔(𝑓𝑛) / 𝑘𝐵 = (𝑔𝑛) / 𝑘𝐵)
4443mpteq2dv 4946 . . . . . . . . . . . . . . 15 (𝑓 = 𝑔 → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))
4527, 44syl5eq 2859 . . . . . . . . . . . . . 14 (𝑓 = 𝑔𝐺 = (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))
4645seqeq3d 13035 . . . . . . . . . . . . 13 (𝑓 = 𝑔 → seq1( + , 𝐺) = seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵)))
4746fveq1d 6413 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (seq1( + , 𝐺)‘𝑛) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))
4847eqeq2d 2823 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑦 = (seq1( + , 𝐺)‘𝑛) ↔ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)))
4941, 48anbi12d 618 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))))
5049cbvexvw 2138 . . . . . . . . 9 (∃𝑓(𝑓:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑛)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)))
5140, 50syl6bb 278 . . . . . . . 8 (𝑚 = 𝑛 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))))
5251cbvrexv 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𝐴)) → 𝜑)
5756, 11sylan 571 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
58 fveq2 6411 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → (𝑓𝑛) = (𝑓𝑗))
5958csbeq1d 3742 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑗) / 𝑘𝐵)
6059cbvmptv 4951 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
6127, 60eqtri 2835 . . . . . . . . . . . . . . . 16 𝐺 = (𝑗 ∈ ℕ ↦ (𝑓𝑗) / 𝑘𝐵)
62 fveq2 6411 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑗 → (𝑔𝑛) = (𝑔𝑗))
6362csbeq1d 3742 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑗(𝑔𝑛) / 𝑘𝐵 = (𝑔𝑗) / 𝑘𝐵)
6463cbvmptv 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𝐴)
689, 57, 61, 64, 65, 66, 67summolem3 14671 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))
69 eqeq12 2826 . . . . . . . . . . . . . . 15 ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)) → (𝑥 = 𝑦 ↔ (seq1( + , 𝐺)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)))
7068, 69syl5ibrcom 238 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ (𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴)) → ((𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)) → 𝑥 = 𝑦))
7170expimpd 443 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑔:(1...𝑛)–1-1-onto𝐴) ∧ (𝑥 = (seq1( + , 𝐺)‘𝑚) ∧ 𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7255, 71syl5bi 233 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7372exlimdvv 2025 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (∃𝑓𝑔((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ (𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7454, 73syl5bir 234 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → ((∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7574rexlimdvva 3233 . . . . . . . . 9 (𝜑 → (∃𝑚 ∈ ℕ ∃𝑛 ∈ ℕ (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7653, 75syl5bir 234 . . . . . . . 8 (𝜑 → ((∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ∧ ∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛))) → 𝑥 = 𝑦))
7776expdimp 442 . . . . . . 7 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑛 ∈ ℕ ∃𝑔(𝑔:(1...𝑛)–1-1-onto𝐴𝑦 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑔𝑛) / 𝑘𝐵))‘𝑛)) → 𝑥 = 𝑦))
7852, 77syl5bi 233 . . . . . 6 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦))
7933, 78jaod 877 . . . . 5 ((𝜑 ∧ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
8029, 79jaodan 971 . . . 4 ((𝜑 ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))) → 𝑥 = 𝑦))
8180expimpd 443 . . 3 (𝜑 → (((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
8281alrimivv 2019 . 2 (𝜑 → ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
83 breq2 4855 . . . . . 6 (𝑥 = 𝑦 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑚( + , 𝐹) ⇝ 𝑦))
8483anbi2d 616 . . . . 5 (𝑥 = 𝑦 → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
8584rexbidv 3247 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦)))
86 eqeq1 2817 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = (seq1( + , 𝐺)‘𝑚) ↔ 𝑦 = (seq1( + , 𝐺)‘𝑚)))
8786anbi2d 616 . . . . . 6 (𝑥 = 𝑦 → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
8887exbidv 2012 . . . . 5 (𝑥 = 𝑦 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
8988rexbidv 3247 . . . 4 (𝑥 = 𝑦 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚))))
9085, 89orbi12d 933 . . 3 (𝑥 = 𝑦 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))))
9190mo4 2687 . 2 (∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ↔ ∀𝑥𝑦(((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑦) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑦 = (seq1( + , 𝐺)‘𝑚)))) → 𝑥 = 𝑦))
9282, 91sylibr 225 1 (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , 𝐺)‘𝑚))))
Colors of variables: wff setvar class
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-ontowf1o 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
  Copyright terms: Public domain W3C validator