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

Theorem fsum2dlemstep 11426
Description: Lemma for fsum2d 11427- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
Hypotheses
Ref Expression
fsum2d.1 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
fsum2d.2 (𝜑𝐴 ∈ Fin)
fsum2d.3 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
fsum2d.4 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
fsum2d.5 (𝜑 → ¬ 𝑦𝑥)
fsum2d.6 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
fsum2dlemstep.x (𝜑𝑥 ∈ Fin)
fsum2d.7 (𝜓 ↔ Σ𝑗𝑥 Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
Assertion
Ref Expression
fsum2dlemstep ((𝜑𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Distinct variable groups:   𝑗,𝑘,𝑥,𝑦,𝑧,𝐴   𝐵,𝑘,𝑥,𝑦,𝑧   𝐷,𝑗,𝑘,𝑥,𝑦   𝑥,𝐶,𝑦,𝑧   𝜑,𝑗,𝑘,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦,𝑧,𝑗,𝑘)   𝐵(𝑗)   𝐶(𝑗,𝑘)   𝐷(𝑧)

Proof of Theorem fsum2dlemstep
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4 ((𝜑𝜓) → 𝜓)
2 fsum2d.7 . . . 4 (𝜓 ↔ Σ𝑗𝑥 Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
31, 2sylib 122 . . 3 ((𝜑𝜓) → Σ𝑗𝑥 Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
4 nfcv 2319 . . . . . 6 𝑚Σ𝑘𝐵 𝐶
5 nfcsb1v 3090 . . . . . . 7 𝑗𝑚 / 𝑗𝐵
6 nfcsb1v 3090 . . . . . . 7 𝑗𝑚 / 𝑗𝐶
75, 6nfsum 11349 . . . . . 6 𝑗Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
8 csbeq1a 3066 . . . . . . 7 (𝑗 = 𝑚𝐵 = 𝑚 / 𝑗𝐵)
9 csbeq1a 3066 . . . . . . . 8 (𝑗 = 𝑚𝐶 = 𝑚 / 𝑗𝐶)
109adantr 276 . . . . . . 7 ((𝑗 = 𝑚𝑘𝐵) → 𝐶 = 𝑚 / 𝑗𝐶)
118, 10sumeq12dv 11364 . . . . . 6 (𝑗 = 𝑚 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶)
124, 7, 11cbvsumi 11354 . . . . 5 Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
13 fsum2d.6 . . . . . . . . 9 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
1413unssbd 3313 . . . . . . . 8 (𝜑 → {𝑦} ⊆ 𝐴)
15 vex 2740 . . . . . . . . 9 𝑦 ∈ V
1615snss 3726 . . . . . . . 8 (𝑦𝐴 ↔ {𝑦} ⊆ 𝐴)
1714, 16sylibr 134 . . . . . . 7 (𝜑𝑦𝐴)
18 fsum2d.3 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
1918ralrimiva 2550 . . . . . . . . 9 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
20 nfcsb1v 3090 . . . . . . . . . . 11 𝑗𝑦 / 𝑗𝐵
2120nfel1 2330 . . . . . . . . . 10 𝑗𝑦 / 𝑗𝐵 ∈ Fin
22 csbeq1a 3066 . . . . . . . . . . 11 (𝑗 = 𝑦𝐵 = 𝑦 / 𝑗𝐵)
2322eleq1d 2246 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ 𝑦 / 𝑗𝐵 ∈ Fin))
2421, 23rspc 2835 . . . . . . . . 9 (𝑦𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑦 / 𝑗𝐵 ∈ Fin))
2517, 19, 24sylc 62 . . . . . . . 8 (𝜑𝑦 / 𝑗𝐵 ∈ Fin)
26 fsum2d.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
2726ralrimivva 2559 . . . . . . . . . 10 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ)
28 nfcsb1v 3090 . . . . . . . . . . . . 13 𝑗𝑦 / 𝑗𝐶
2928nfel1 2330 . . . . . . . . . . . 12 𝑗𝑦 / 𝑗𝐶 ∈ ℂ
3020, 29nfralxy 2515 . . . . . . . . . . 11 𝑗𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ
31 csbeq1a 3066 . . . . . . . . . . . . 13 (𝑗 = 𝑦𝐶 = 𝑦 / 𝑗𝐶)
3231eleq1d 2246 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ 𝑦 / 𝑗𝐶 ∈ ℂ))
3322, 32raleqbidv 2684 . . . . . . . . . . 11 (𝑗 = 𝑦 → (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3430, 33rspc 2835 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3517, 27, 34sylc 62 . . . . . . . . 9 (𝜑 → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
3635r19.21bi 2565 . . . . . . . 8 ((𝜑𝑘𝑦 / 𝑗𝐵) → 𝑦 / 𝑗𝐶 ∈ ℂ)
3725, 36fsumcl 11392 . . . . . . 7 (𝜑 → Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
38 csbeq1 3060 . . . . . . . . 9 (𝑚 = 𝑦𝑚 / 𝑗𝐵 = 𝑦 / 𝑗𝐵)
39 csbeq1 3060 . . . . . . . . . 10 (𝑚 = 𝑦𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4039adantr 276 . . . . . . . . 9 ((𝑚 = 𝑦𝑘𝑚 / 𝑗𝐵) → 𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4138, 40sumeq12dv 11364 . . . . . . . 8 (𝑚 = 𝑦 → Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4241sumsn 11403 . . . . . . 7 ((𝑦𝐴 ∧ Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4317, 37, 42syl2anc 411 . . . . . 6 (𝜑 → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
44 nfcv 2319 . . . . . . . 8 𝑚𝑦 / 𝑗𝐶
45 nfcsb1v 3090 . . . . . . . 8 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶
46 csbeq1a 3066 . . . . . . . 8 (𝑘 = 𝑚𝑦 / 𝑗𝐶 = 𝑚 / 𝑘𝑦 / 𝑗𝐶)
4744, 45, 46cbvsumi 11354 . . . . . . 7 Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶
48 csbeq1 3060 . . . . . . . . 9 (𝑚 = (2nd𝑧) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
49 snfig 6808 . . . . . . . . . . 11 (𝑦 ∈ V → {𝑦} ∈ Fin)
5049elv 2741 . . . . . . . . . 10 {𝑦} ∈ Fin
51 xpfi 6923 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑗𝐵 ∈ Fin) → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
5250, 25, 51sylancr 414 . . . . . . . . 9 (𝜑 → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
53 2ndconst 6217 . . . . . . . . . 10 (𝑦𝐴 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
5417, 53syl 14 . . . . . . . . 9 (𝜑 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
55 fvres 5535 . . . . . . . . . 10 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5655adantl 277 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5745nfel1 2330 . . . . . . . . . . 11 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ
5846eleq1d 2246 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝑦 / 𝑗𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
5957, 58rspc 2835 . . . . . . . . . 10 (𝑚𝑦 / 𝑗𝐵 → (∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
6035, 59mpan9 281 . . . . . . . . 9 ((𝜑𝑚𝑦 / 𝑗𝐵) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ)
6148, 52, 54, 56, 60fsumf1o 11382 . . . . . . . 8 (𝜑 → Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
62 elxp 4640 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)))
63 nfv 1528 . . . . . . . . . . . . . . 15 𝑗 𝑧 = ⟨𝑚, 𝑘
64 nfv 1528 . . . . . . . . . . . . . . . 16 𝑗 𝑚 ∈ {𝑦}
6520nfcri 2313 . . . . . . . . . . . . . . . 16 𝑗 𝑘𝑦 / 𝑗𝐵
6664, 65nfan 1565 . . . . . . . . . . . . . . 15 𝑗(𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)
6763, 66nfan 1565 . . . . . . . . . . . . . 14 𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
6867nfex 1637 . . . . . . . . . . . . 13 𝑗𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
69 nfv 1528 . . . . . . . . . . . . 13 𝑚𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))
70 opeq1 3776 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
7170eqeq2d 2189 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
72 velsn 3608 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ {𝑦} ↔ 𝑚 = 𝑦)
7372anbi1i 458 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑚 = 𝑦𝑘𝑦 / 𝑗𝐵))
74 eqtr2 2196 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑗𝑚 = 𝑦) → 𝑗 = 𝑦)
7574, 22syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑗𝑚 = 𝑦) → 𝐵 = 𝑦 / 𝑗𝐵)
7675eleq2d 2247 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝑗𝑚 = 𝑦) → (𝑘𝐵𝑘𝑦 / 𝑗𝐵))
7776pm5.32da 452 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → ((𝑚 = 𝑦𝑘𝐵) ↔ (𝑚 = 𝑦𝑘𝑦 / 𝑗𝐵)))
7873, 77bitr4id 199 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑚 = 𝑦𝑘𝐵)))
79 equequ1 1712 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → (𝑚 = 𝑦𝑗 = 𝑦))
8079anbi1d 465 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 = 𝑦𝑘𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
8178, 80bitrd 188 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
8271, 81anbi12d 473 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8382exbidv 1825 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8468, 69, 83cbvex 1756 . . . . . . . . . . . 12 (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
8562, 84bitri 184 . . . . . . . . . . 11 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
86 nfv 1528 . . . . . . . . . . . 12 𝑗𝜑
87 nfcv 2319 . . . . . . . . . . . . . 14 𝑗(2nd𝑧)
8887, 28nfcsb 3094 . . . . . . . . . . . . 13 𝑗(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8988nfeq2 2331 . . . . . . . . . . . 12 𝑗 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
90 nfv 1528 . . . . . . . . . . . . 13 𝑘𝜑
91 nfcsb1v 3090 . . . . . . . . . . . . . 14 𝑘(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
9291nfeq2 2331 . . . . . . . . . . . . 13 𝑘 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
93 fsum2d.1 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
9493ad2antlr 489 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = 𝐶)
9531ad2antrl 490 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐶 = 𝑦 / 𝑗𝐶)
96 fveq2 5511 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
97 vex 2740 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
98 vex 2740 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
9997, 98op2nd 6142 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
10096, 99eqtr2di 2227 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd𝑧))
101100ad2antlr 489 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑘 = (2nd𝑧))
102 csbeq1a 3066 . . . . . . . . . . . . . . . 16 (𝑘 = (2nd𝑧) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
103101, 102syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10494, 95, 1033eqtrd 2214 . . . . . . . . . . . . . 14 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
105104expl 378 . . . . . . . . . . . . 13 (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10690, 92, 105exlimd 1597 . . . . . . . . . . . 12 (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10786, 89, 106exlimd 1597 . . . . . . . . . . 11 (𝜑 → (∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10885, 107biimtrid 152 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
109108imp 124 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
110109sumeq2dv 11360 . . . . . . . 8 (𝜑 → Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
11161, 110eqtr4d 2213 . . . . . . 7 (𝜑 → Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11247, 111eqtrid 2222 . . . . . 6 (𝜑 → Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11343, 112eqtrd 2210 . . . . 5 (𝜑 → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11412, 113eqtrid 2222 . . . 4 (𝜑 → Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
115114adantr 276 . . 3 ((𝜑𝜓) → Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
1163, 115oveq12d 5887 . 2 ((𝜑𝜓) → (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶) = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
117 fsum2d.5 . . . . 5 (𝜑 → ¬ 𝑦𝑥)
118 disjsn 3653 . . . . 5 ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝑥)
119117, 118sylibr 134 . . . 4 (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
120 eqidd 2178 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
121 fsum2dlemstep.x . . . . 5 (𝜑𝑥 ∈ Fin)
12250a1i 9 . . . . 5 (𝜑 → {𝑦} ∈ Fin)
123 unfidisj 6915 . . . . 5 ((𝑥 ∈ Fin ∧ {𝑦} ∈ Fin ∧ (𝑥 ∩ {𝑦}) = ∅) → (𝑥 ∪ {𝑦}) ∈ Fin)
124121, 122, 119, 123syl3anc 1238 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
12513sselda 3155 . . . . 5 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗𝐴)
12626anassrs 400 . . . . . 6 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
12718, 126fsumcl 11392 . . . . 5 ((𝜑𝑗𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
128125, 127syldan 282 . . . 4 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → Σ𝑘𝐵 𝐶 ∈ ℂ)
129119, 120, 124, 128fsumsplit 11399 . . 3 (𝜑 → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶))
130129adantr 276 . 2 ((𝜑𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶))
131 eliun 3888 . . . . . . . . . 10 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵))
132 xp1st 6160 . . . . . . . . . . . . . 14 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
133 elsni 3609 . . . . . . . . . . . . . 14 ((1st𝑧) ∈ {𝑗} → (1st𝑧) = 𝑗)
134132, 133syl 14 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
135134adantl 277 . . . . . . . . . . . 12 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) = 𝑗)
136 simpl 109 . . . . . . . . . . . 12 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → 𝑗𝑥)
137135, 136eqeltrd 2254 . . . . . . . . . . 11 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) ∈ 𝑥)
138137rexlimiva 2589 . . . . . . . . . 10 (∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
139131, 138sylbi 121 . . . . . . . . 9 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
140 xp1st 6160 . . . . . . . . 9 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → (1st𝑧) ∈ {𝑦})
141139, 140anim12i 338 . . . . . . . 8 ((𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
142 elin 3318 . . . . . . . 8 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ↔ (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)))
143 elin 3318 . . . . . . . 8 ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
144141, 142, 1433imtr4i 201 . . . . . . 7 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → (1st𝑧) ∈ (𝑥 ∩ {𝑦}))
145119eleq2d 2247 . . . . . . . 8 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st𝑧) ∈ ∅))
146 noel 3426 . . . . . . . . 9 ¬ (1st𝑧) ∈ ∅
147146pm2.21i 646 . . . . . . . 8 ((1st𝑧) ∈ ∅ → 𝑧 ∈ ∅)
148145, 147syl6bi 163 . . . . . . 7 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
149144, 148syl5 32 . . . . . 6 (𝜑 → (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝑧 ∈ ∅))
150149ssrdv 3161 . . . . 5 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅)
151 ss0 3463 . . . . 5 (( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅ → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
152150, 151syl 14 . . . 4 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
153 iunxun 3963 . . . . . 6 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
154 nfcv 2319 . . . . . . . . 9 𝑚({𝑗} × 𝐵)
155 nfcv 2319 . . . . . . . . . 10 𝑗{𝑚}
156155, 5nfxp 4650 . . . . . . . . 9 𝑗({𝑚} × 𝑚 / 𝑗𝐵)
157 sneq 3602 . . . . . . . . . 10 (𝑗 = 𝑚 → {𝑗} = {𝑚})
158157, 8xpeq12d 4648 . . . . . . . . 9 (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × 𝑚 / 𝑗𝐵))
159154, 156, 158cbviun 3921 . . . . . . . 8 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵)
160 sneq 3602 . . . . . . . . . 10 (𝑚 = 𝑦 → {𝑚} = {𝑦})
161160, 38xpeq12d 4648 . . . . . . . . 9 (𝑚 = 𝑦 → ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵))
16215, 161iunxsn 3960 . . . . . . . 8 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
163159, 162eqtri 2198 . . . . . . 7 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
164163uneq2i 3286 . . . . . 6 ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
165153, 164eqtri 2198 . . . . 5 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
166165a1i 9 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵)))
167 snfig 6808 . . . . . . . 8 (𝑗 ∈ V → {𝑗} ∈ Fin)
168167elv 2741 . . . . . . 7 {𝑗} ∈ Fin
169125, 18syldan 282 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
170 xpfi 6923 . . . . . . 7 (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
171168, 169, 170sylancr 414 . . . . . 6 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
172171ralrimiva 2550 . . . . 5 (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
173 disjsnxp 6232 . . . . . 6 Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)
174173a1i 9 . . . . 5 (𝜑Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵))
175 iunfidisj 6939 . . . . 5 (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin ∧ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
176124, 172, 174, 175syl3anc 1238 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
177 eliun 3888 . . . . . 6 (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
178 elxp 4640 . . . . . . . 8 (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)))
179 simprl 529 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
180 simprrl 539 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 ∈ {𝑗})
181 elsni 3609 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
182180, 181syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 = 𝑗)
183182opeq1d 3782 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
184179, 183eqtrd 2210 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
185184, 93syl 14 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 = 𝐶)
186 simpll 527 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝜑)
187125adantr 276 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑗𝐴)
188 simprrr 540 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑘𝐵)
189186, 187, 188, 26syl12anc 1236 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐶 ∈ ℂ)
190185, 189eqeltrd 2254 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 ∈ ℂ)
191190ex 115 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
192191exlimdvv 1897 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
193178, 192biimtrid 152 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
194193rexlimdva 2594 . . . . . 6 (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
195177, 194biimtrid 152 . . . . 5 (𝜑 → (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
196195imp 124 . . . 4 ((𝜑𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
197152, 166, 176, 196fsumsplit 11399 . . 3 (𝜑 → Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
198197adantr 276 . 2 ((𝜑𝜓) → Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
199116, 130, 1983eqtr4d 2220 1 ((𝜑𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105   = wceq 1353  wex 1492  wcel 2148  wral 2455  wrex 2456  Vcvv 2737  csb 3057  cun 3127  cin 3128  wss 3129  c0 3422  {csn 3591  cop 3594   ciun 3884  Disj wdisj 3977   × cxp 4621  cres 4625  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  1st c1st 6133  2nd c2nd 6134  Fincfn 6734  cc 7800   + caddc 7805  Σcsu 11345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-disj 3978  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-frec 6386  df-1o 6411  df-oadd 6415  df-er 6529  df-en 6735  df-dom 6736  df-fin 6737  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-fz 9996  df-fzo 10129  df-seqfrec 10432  df-exp 10506  df-ihash 10740  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-clim 11271  df-sumdc 11346
This theorem is referenced by:  fsum2d  11427
  Copyright terms: Public domain W3C validator