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

Theorem fsum 14400
Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Mario Carneiro, 13-Jun-2019.)
Hypotheses
Ref Expression
fsum.1 (𝑘 = (𝐹𝑛) → 𝐵 = 𝐶)
fsum.2 (𝜑𝑀 ∈ ℕ)
fsum.3 (𝜑𝐹:(1...𝑀)–1-1-onto𝐴)
fsum.4 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
fsum.5 ((𝜑𝑛 ∈ (1...𝑀)) → (𝐺𝑛) = 𝐶)
Assertion
Ref Expression
fsum (𝜑 → Σ𝑘𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))
Distinct variable groups:   𝐵,𝑛   𝐶,𝑘   𝑘,𝑛,𝐹   𝜑,𝑘,𝑛   𝐴,𝑘,𝑛   𝑘,𝐺,𝑛   𝑘,𝑀,𝑛
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑛)

Proof of Theorem fsum
Dummy variables 𝑓 𝑖 𝑗 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sum 14367 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
2 fvex 6168 . . 3 (seq1( + , 𝐺)‘𝑀) ∈ V
3 eleq1 2686 . . . . . . . . . 10 (𝑛 = 𝑗 → (𝑛𝐴𝑗𝐴))
4 csbeq1 3522 . . . . . . . . . 10 (𝑛 = 𝑗𝑛 / 𝑘𝐵 = 𝑗 / 𝑘𝐵)
53, 4ifbieq1d 4087 . . . . . . . . 9 (𝑛 = 𝑗 → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if(𝑗𝐴, 𝑗 / 𝑘𝐵, 0))
65cbvmptv 4720 . . . . . . . 8 (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)) = (𝑗 ∈ ℤ ↦ if(𝑗𝐴, 𝑗 / 𝑘𝐵, 0))
7 fsum.4 . . . . . . . . . 10 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
87ralrimiva 2962 . . . . . . . . 9 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
9 nfcsb1v 3535 . . . . . . . . . . 11 𝑘𝑗 / 𝑘𝐵
109nfel1 2775 . . . . . . . . . 10 𝑘𝑗 / 𝑘𝐵 ∈ ℂ
11 csbeq1a 3528 . . . . . . . . . . 11 (𝑘 = 𝑗𝐵 = 𝑗 / 𝑘𝐵)
1211eleq1d 2683 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ 𝑗 / 𝑘𝐵 ∈ ℂ))
1310, 12rspc 3293 . . . . . . . . 9 (𝑗𝐴 → (∀𝑘𝐴 𝐵 ∈ ℂ → 𝑗 / 𝑘𝐵 ∈ ℂ))
148, 13mpan9 486 . . . . . . . 8 ((𝜑𝑗𝐴) → 𝑗 / 𝑘𝐵 ∈ ℂ)
15 fveq2 6158 . . . . . . . . . . 11 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
1615csbeq1d 3526 . . . . . . . . . 10 (𝑛 = 𝑖(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑖) / 𝑘𝐵)
17 csbco 3529 . . . . . . . . . 10 (𝑓𝑖) / 𝑗𝑗 / 𝑘𝐵 = (𝑓𝑖) / 𝑘𝐵
1816, 17syl6eqr 2673 . . . . . . . . 9 (𝑛 = 𝑖(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑖) / 𝑗𝑗 / 𝑘𝐵)
1918cbvmptv 4720 . . . . . . . 8 (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑖 ∈ ℕ ↦ (𝑓𝑖) / 𝑗𝑗 / 𝑘𝐵)
206, 14, 19summo 14397 . . . . . . 7 (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
21 fsum.2 . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
22 fsum.3 . . . . . . . . . . . 12 (𝜑𝐹:(1...𝑀)–1-1-onto𝐴)
23 f1of 6104 . . . . . . . . . . . 12 (𝐹:(1...𝑀)–1-1-onto𝐴𝐹:(1...𝑀)⟶𝐴)
2422, 23syl 17 . . . . . . . . . . 11 (𝜑𝐹:(1...𝑀)⟶𝐴)
25 ovex 6643 . . . . . . . . . . 11 (1...𝑀) ∈ V
26 fex 6455 . . . . . . . . . . 11 ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
2724, 25, 26sylancl 693 . . . . . . . . . 10 (𝜑𝐹 ∈ V)
28 nnuz 11683 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
2921, 28syl6eleq 2708 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘1))
30 fsum.5 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑀)) → (𝐺𝑛) = 𝐶)
31 elfznn 12328 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ)
3231adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑀)) → 𝑛 ∈ ℕ)
33 fvex 6168 . . . . . . . . . . . . . . . . 17 (𝐺𝑛) ∈ V
3430, 33syl6eqelr 2707 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝑀)) → 𝐶 ∈ V)
35 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ ↦ 𝐶) = (𝑛 ∈ ℕ ↦ 𝐶)
3635fvmpt2 6258 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ 𝐶 ∈ V) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
3732, 34, 36syl2anc 692 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶)
3830, 37eqtr4d 2658 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝑀)) → (𝐺𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
3938ralrimiva 2962 . . . . . . . . . . . . 13 (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛))
40 nffvmpt1 6166 . . . . . . . . . . . . . . 15 𝑛((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
4140nfeq2 2776 . . . . . . . . . . . . . 14 𝑛(𝐺𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)
42 fveq2 6158 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝐺𝑛) = (𝐺𝑘))
43 fveq2 6158 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
4442, 43eqeq12d 2636 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((𝐺𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) ↔ (𝐺𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
4541, 44rspc 3293 . . . . . . . . . . . . 13 (𝑘 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)(𝐺𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) → (𝐺𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)))
4639, 45mpan9 486 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...𝑀)) → (𝐺𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))
4729, 46seqfveq 12781 . . . . . . . . . . 11 (𝜑 → (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
4822, 47jca 554 . . . . . . . . . 10 (𝜑 → (𝐹:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
49 f1oeq1 6094 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto𝐴𝐹:(1...𝑀)–1-1-onto𝐴))
50 fveq1 6157 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝐹 → (𝑓𝑛) = (𝐹𝑛))
5150csbeq1d 3526 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹(𝑓𝑛) / 𝑘𝐵 = (𝐹𝑛) / 𝑘𝐵)
52 fvex 6168 . . . . . . . . . . . . . . . . . 18 (𝐹𝑛) ∈ V
53 fsum.1 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝐹𝑛) → 𝐵 = 𝐶)
5452, 53csbie 3545 . . . . . . . . . . . . . . . . 17 (𝐹𝑛) / 𝑘𝐵 = 𝐶
5551, 54syl6eq 2671 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹(𝑓𝑛) / 𝑘𝐵 = 𝐶)
5655mpteq2dv 4715 . . . . . . . . . . . . . . 15 (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵) = (𝑛 ∈ ℕ ↦ 𝐶))
5756seqeq3d 12765 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵)) = seq1( + , (𝑛 ∈ ℕ ↦ 𝐶)))
5857fveq1d 6160 . . . . . . . . . . . . 13 (𝑓 = 𝐹 → (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))
5958eqeq2d 2631 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))
6049, 59anbi12d 746 . . . . . . . . . . 11 (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))))
6160spcegv 3284 . . . . . . . . . 10 (𝐹 ∈ V → ((𝐹:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)) → ∃𝑓(𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀))))
6227, 48, 61sylc 65 . . . . . . . . 9 (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀)))
63 oveq2 6623 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀))
64 f1oeq2 6095 . . . . . . . . . . . . 13 ((1...𝑚) = (1...𝑀) → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑀)–1-1-onto𝐴))
6563, 64syl 17 . . . . . . . . . . . 12 (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑀)–1-1-onto𝐴))
66 fveq2 6158 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀))
6766eqeq2d 2631 . . . . . . . . . . . 12 (𝑚 = 𝑀 → ((seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀)))
6865, 67anbi12d 746 . . . . . . . . . . 11 (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀))))
6968exbidv 1847 . . . . . . . . . 10 (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀))))
7069rspcev 3299 . . . . . . . . 9 ((𝑀 ∈ ℕ ∧ ∃𝑓(𝑓:(1...𝑀)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
7121, 62, 70syl2anc 692 . . . . . . . 8 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
7271olcd 408 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
73 breq2 4627 . . . . . . . . . . . . . 14 (𝑥 = (seq1( + , 𝐺)‘𝑀) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)))
7473anbi2d 739 . . . . . . . . . . . . 13 (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
7574rexbidv 3047 . . . . . . . . . . . 12 (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀))))
76 eqeq1 2625 . . . . . . . . . . . . . . 15 (𝑥 = (seq1( + , 𝐺)‘𝑀) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚) ↔ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))
7776anbi2d 739 . . . . . . . . . . . . . 14 (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
7877exbidv 1847 . . . . . . . . . . . . 13 (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
7978rexbidv 3047 . . . . . . . . . . . 12 (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))
8075, 79orbi12d 745 . . . . . . . . . . 11 (𝑥 = (seq1( + , 𝐺)‘𝑀) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))))
8180moi2 3374 . . . . . . . . . 10 ((((seq1( + , 𝐺)‘𝑀) ∈ V ∧ ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
822, 81mpanl1 715 . . . . . . . . 9 ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
8382ancom2s 843 . . . . . . . 8 ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))))) → 𝑥 = (seq1( + , 𝐺)‘𝑀))
8483expr 642 . . . . . . 7 ((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ (seq1( + , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴 ∧ (seq1( + , 𝐺)‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) → 𝑥 = (seq1( + , 𝐺)‘𝑀)))
8520, 72, 84syl2anc 692 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) → 𝑥 = (seq1( + , 𝐺)‘𝑀)))
8672, 80syl5ibrcom 237 . . . . . 6 (𝜑 → (𝑥 = (seq1( + , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))))
8785, 86impbid 202 . . . . 5 (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
8887adantr 481 . . . 4 ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚))) ↔ 𝑥 = (seq1( + , 𝐺)‘𝑀)))
8988iota5 5840 . . 3 ((𝜑 ∧ (seq1( + , 𝐺)‘𝑀) ∈ V) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
902, 89mpan2 706 . 2 (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑓𝑛) / 𝑘𝐵))‘𝑚)))) = (seq1( + , 𝐺)‘𝑀))
911, 90syl5eq 2667 1 (𝜑 → Σ𝑘𝐴 𝐵 = (seq1( + , 𝐺)‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wex 1701  wcel 1987  ∃*wmo 2470  wral 2908  wrex 2909  Vcvv 3190  csb 3519  wss 3560  ifcif 4064   class class class wbr 4623  cmpt 4683  cio 5818  wf 5853  1-1-ontowf1o 5856  cfv 5857  (class class class)co 6615  cc 9894  0cc0 9896  1c1 9897   + caddc 9899  cn 10980  cz 11337  cuz 11647  ...cfz 12284  seqcseq 12757  cli 14165  Σcsu 14366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-oadd 7524  df-er 7702  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-oi 8375  df-card 8725  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-z 11338  df-uz 11648  df-rp 11793  df-fz 12285  df-fzo 12423  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-sum 14367
This theorem is referenced by:  sumz  14402  fsumf1o  14403  fsumcl2lem  14411  fsumadd  14419  sumsnf  14422  sumsn  14424  fsummulc2  14463  fsumconst  14469  fsumrelem  14485  gsumfsum  19753  sumsnd  38707
  Copyright terms: Public domain W3C validator