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

Theorem sumeq2 10416
Description: Equality theorem for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
Assertion
Ref Expression
sumeq2 (∀𝑘𝐴 𝐵 = 𝐶 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Distinct variable group:   𝐴,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem sumeq2
Dummy variables 𝑓 𝑗 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 108 . . . . . . . . . . . 12 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) ∧ 𝑛𝐴) → 𝑛𝐴)
2 simp-4l 508 . . . . . . . . . . . 12 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) ∧ 𝑛𝐴) → ∀𝑘𝐴 𝐵 = 𝐶)
3 nfcsb1v 2947 . . . . . . . . . . . . . 14 𝑘𝑛 / 𝑘𝐵
4 nfcsb1v 2947 . . . . . . . . . . . . . 14 𝑘𝑛 / 𝑘𝐶
53, 4nfeq 2230 . . . . . . . . . . . . 13 𝑘𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶
6 csbeq1a 2925 . . . . . . . . . . . . . 14 (𝑘 = 𝑛𝐵 = 𝑛 / 𝑘𝐵)
7 csbeq1a 2925 . . . . . . . . . . . . . 14 (𝑘 = 𝑛𝐶 = 𝑛 / 𝑘𝐶)
86, 7eqeq12d 2097 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (𝐵 = 𝐶𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶))
95, 8rspc 2704 . . . . . . . . . . . 12 (𝑛𝐴 → (∀𝑘𝐴 𝐵 = 𝐶𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶))
101, 2, 9sylc 61 . . . . . . . . . . 11 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) ∧ 𝑛𝐴) → 𝑛 / 𝑘𝐵 = 𝑛 / 𝑘𝐶)
11 simpllr 501 . . . . . . . . . . . 12 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → 𝑚 ∈ ℤ)
12 simplrl 502 . . . . . . . . . . . 12 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → 𝐴 ⊆ (ℤ𝑚))
13 simplrr 503 . . . . . . . . . . . 12 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)
14 simpr 108 . . . . . . . . . . . 12 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
1511, 12, 13, 14sumdc 10414 . . . . . . . . . . 11 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → DECID 𝑛𝐴)
1610, 15ifeq1dadc 3396 . . . . . . . . . 10 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) ∧ 𝑛 ∈ ℤ) → if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0) = if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0))
1716mpteq2dva 3888 . . . . . . . . 9 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) → (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)))
18 iseqeq3 9596 . . . . . . . . 9 ((𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)) = (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)) → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ))
1917, 18syl 14 . . . . . . . 8 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) → seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) = seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ))
2019breq1d 3815 . . . . . . 7 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴)) → (seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥 ↔ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥))
2120pm5.32da 440 . . . . . 6 ((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) → (((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ↔ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥)))
22 df-3an 922 . . . . . 6 ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ↔ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥))
23 df-3an 922 . . . . . 6 ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥) ↔ ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥))
2421, 22, 233bitr4g 221 . . . . 5 ((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥)))
2524rexbidva 2370 . . . 4 (∀𝑘𝐴 𝐵 = 𝐶 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥)))
26 f1of 5178 . . . . . . . . . . . . . . 15 (𝑓:(1...𝑚)–1-1-onto𝐴𝑓:(1...𝑚)⟶𝐴)
2726ad3antlr 477 . . . . . . . . . . . . . 14 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑓:(1...𝑚)⟶𝐴)
28 simplr 497 . . . . . . . . . . . . . . 15 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑛 ∈ ℕ)
29 simpr 108 . . . . . . . . . . . . . . 15 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑛𝑚)
30 simp-4r 509 . . . . . . . . . . . . . . . . 17 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑚 ∈ ℕ)
3130nnzd 8619 . . . . . . . . . . . . . . . 16 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑚 ∈ ℤ)
32 fznn 9252 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℤ → (𝑛 ∈ (1...𝑚) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑚)))
3331, 32syl 14 . . . . . . . . . . . . . . 15 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → (𝑛 ∈ (1...𝑚) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑚)))
3428, 29, 33mpbir2and 886 . . . . . . . . . . . . . 14 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → 𝑛 ∈ (1...𝑚))
3527, 34ffvelrnd 5356 . . . . . . . . . . . . 13 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → (𝑓𝑛) ∈ 𝐴)
36 simp-4l 508 . . . . . . . . . . . . 13 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → ∀𝑘𝐴 𝐵 = 𝐶)
37 nfcsb1v 2947 . . . . . . . . . . . . . . 15 𝑘(𝑓𝑛) / 𝑘𝐵
38 nfcsb1v 2947 . . . . . . . . . . . . . . 15 𝑘(𝑓𝑛) / 𝑘𝐶
3937, 38nfeq 2230 . . . . . . . . . . . . . 14 𝑘(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶
40 csbeq1a 2925 . . . . . . . . . . . . . . 15 (𝑘 = (𝑓𝑛) → 𝐵 = (𝑓𝑛) / 𝑘𝐵)
41 csbeq1a 2925 . . . . . . . . . . . . . . 15 (𝑘 = (𝑓𝑛) → 𝐶 = (𝑓𝑛) / 𝑘𝐶)
4240, 41eqeq12d 2097 . . . . . . . . . . . . . 14 (𝑘 = (𝑓𝑛) → (𝐵 = 𝐶(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶))
4339, 42rspc 2704 . . . . . . . . . . . . 13 ((𝑓𝑛) ∈ 𝐴 → (∀𝑘𝐴 𝐵 = 𝐶(𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶))
4435, 36, 43sylc 61 . . . . . . . . . . . 12 (((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑛𝑚) → (𝑓𝑛) / 𝑘𝐵 = (𝑓𝑛) / 𝑘𝐶)
45 simpr 108 . . . . . . . . . . . . . 14 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
4645nnzd 8619 . . . . . . . . . . . . 13 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ)
47 simpllr 501 . . . . . . . . . . . . . 14 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℕ)
4847nnzd 8619 . . . . . . . . . . . . 13 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℤ)
49 zdcle 8575 . . . . . . . . . . . . 13 ((𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ) → DECID 𝑛𝑚)
5046, 48, 49syl2anc 403 . . . . . . . . . . . 12 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → DECID 𝑛𝑚)
5144, 50ifeq1dadc 3396 . . . . . . . . . . 11 ((((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) ∧ 𝑛 ∈ ℕ) → if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0) = if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0))
5251mpteq2dva 3888 . . . . . . . . . 10 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)))
53 iseqeq3 9596 . . . . . . . . . 10 ((𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)) = (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ))
5452, 53syl 14 . . . . . . . . 9 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ) = seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ))
5554fveq1d 5232 . . . . . . . 8 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚))
5655eqeq2d 2094 . . . . . . 7 (((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto𝐴) → (𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚) ↔ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚)))
5756pm5.32da 440 . . . . . 6 ((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚))))
5857exbidv 1748 . . . . 5 ((∀𝑘𝐴 𝐵 = 𝐶𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚))))
5958rexbidva 2370 . . . 4 (∀𝑘𝐴 𝐵 = 𝐶 → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚))))
6025, 59orbi12d 740 . . 3 (∀𝑘𝐴 𝐵 = 𝐶 → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚)))))
6160iotabidv 4938 . 2 (∀𝑘𝐴 𝐵 = 𝐶 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚)))))
62 df-isum 10410 . 2 Σ𝑘𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐵, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐵, 0)), ℂ)‘𝑚))))
63 df-isum 10410 . 2 Σ𝑘𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ𝑚) ∧ ∀𝑗 ∈ (ℤ𝑚)DECID 𝑗𝐴 ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛𝐴, 𝑛 / 𝑘𝐶, 0)), ℂ) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto𝐴𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛𝑚, (𝑓𝑛) / 𝑘𝐶, 0)), ℂ)‘𝑚))))
6461, 62, 633eqtr4g 2140 1 (∀𝑘𝐴 𝐵 = 𝐶 → Σ𝑘𝐴 𝐵 = Σ𝑘𝐴 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wo 662  DECID wdc 776  w3a 920   = wceq 1285  wex 1422  wcel 1434  wral 2353  wrex 2354  csb 2917  wss 2982  ifcif 3368   class class class wbr 3805  cmpt 3859  cio 4915  wf 4948  1-1-ontowf1o 4951  cfv 4952  (class class class)co 5564  cc 7111  0cc0 7113  1c1 7114   + caddc 7116  cle 7286  cn 8176  cz 8502  cuz 8770  ...cfz 9175  seqcseq 9591  cli 10336  Σcsu 10409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308  ax-cnex 7199  ax-resscn 7200  ax-1cn 7201  ax-1re 7202  ax-icn 7203  ax-addcl 7204  ax-addrcl 7205  ax-mulcl 7206  ax-addcom 7208  ax-addass 7210  ax-distr 7212  ax-i2m1 7213  ax-0lt1 7214  ax-0id 7216  ax-rnegex 7217  ax-cnre 7219  ax-pre-ltirr 7220  ax-pre-ltwlin 7221  ax-pre-lttrn 7222  ax-pre-ltadd 7224
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-if 3369  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-br 3806  df-opab 3860  df-mpt 3861  df-id 4076  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-f1 4957  df-f1o 4959  df-fv 4960  df-riota 5520  df-ov 5567  df-oprab 5568  df-mpt2 5569  df-recs 5975  df-frec 6061  df-pnf 7287  df-mnf 7288  df-xr 7289  df-ltxr 7290  df-le 7291  df-sub 7418  df-neg 7419  df-inn 8177  df-n0 8426  df-z 8503  df-uz 8771  df-fz 9176  df-iseq 9592  df-isum 10410
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator