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

Theorem fsum2dlemstep 10824
Description: Lemma for fsum2d 10825- 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 108 . . . 4 ((𝜑𝜓) → 𝜓)
2 fsum2d.7 . . . 4 (𝜓 ↔ Σ𝑗𝑥 Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
31, 2sylib 120 . . 3 ((𝜑𝜓) → Σ𝑗𝑥 Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷)
4 nfcv 2228 . . . . . 6 𝑚Σ𝑘𝐵 𝐶
5 nfcsb1v 2963 . . . . . . 7 𝑗𝑚 / 𝑗𝐵
6 nfcsb1v 2963 . . . . . . 7 𝑗𝑚 / 𝑗𝐶
75, 6nfsum 10742 . . . . . 6 𝑗Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
8 csbeq1a 2941 . . . . . . 7 (𝑗 = 𝑚𝐵 = 𝑚 / 𝑗𝐵)
9 csbeq1a 2941 . . . . . . . 8 (𝑗 = 𝑚𝐶 = 𝑚 / 𝑗𝐶)
109adantr 270 . . . . . . 7 ((𝑗 = 𝑚𝑘𝐵) → 𝐶 = 𝑚 / 𝑗𝐶)
118, 10sumeq12dv 10757 . . . . . 6 (𝑗 = 𝑚 → Σ𝑘𝐵 𝐶 = Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶)
124, 7, 11cbvsumi 10747 . . . . 5 Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶
13 fsum2d.6 . . . . . . . . 9 (𝜑 → (𝑥 ∪ {𝑦}) ⊆ 𝐴)
1413unssbd 3178 . . . . . . . 8 (𝜑 → {𝑦} ⊆ 𝐴)
15 vex 2622 . . . . . . . . 9 𝑦 ∈ V
1615snss 3566 . . . . . . . 8 (𝑦𝐴 ↔ {𝑦} ⊆ 𝐴)
1714, 16sylibr 132 . . . . . . 7 (𝜑𝑦𝐴)
18 fsum2d.3 . . . . . . . . . 10 ((𝜑𝑗𝐴) → 𝐵 ∈ Fin)
1918ralrimiva 2446 . . . . . . . . 9 (𝜑 → ∀𝑗𝐴 𝐵 ∈ Fin)
20 nfcsb1v 2963 . . . . . . . . . . 11 𝑗𝑦 / 𝑗𝐵
2120nfel1 2239 . . . . . . . . . 10 𝑗𝑦 / 𝑗𝐵 ∈ Fin
22 csbeq1a 2941 . . . . . . . . . . 11 (𝑗 = 𝑦𝐵 = 𝑦 / 𝑗𝐵)
2322eleq1d 2156 . . . . . . . . . 10 (𝑗 = 𝑦 → (𝐵 ∈ Fin ↔ 𝑦 / 𝑗𝐵 ∈ Fin))
2421, 23rspc 2716 . . . . . . . . 9 (𝑦𝐴 → (∀𝑗𝐴 𝐵 ∈ Fin → 𝑦 / 𝑗𝐵 ∈ Fin))
2517, 19, 24sylc 61 . . . . . . . 8 (𝜑𝑦 / 𝑗𝐵 ∈ Fin)
26 fsum2d.4 . . . . . . . . . . 11 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ ℂ)
2726ralrimivva 2455 . . . . . . . . . 10 (𝜑 → ∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ)
28 nfcsb1v 2963 . . . . . . . . . . . . 13 𝑗𝑦 / 𝑗𝐶
2928nfel1 2239 . . . . . . . . . . . 12 𝑗𝑦 / 𝑗𝐶 ∈ ℂ
3020, 29nfralxy 2414 . . . . . . . . . . 11 𝑗𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ
31 csbeq1a 2941 . . . . . . . . . . . . 13 (𝑗 = 𝑦𝐶 = 𝑦 / 𝑗𝐶)
3231eleq1d 2156 . . . . . . . . . . . 12 (𝑗 = 𝑦 → (𝐶 ∈ ℂ ↔ 𝑦 / 𝑗𝐶 ∈ ℂ))
3322, 32raleqbidv 2574 . . . . . . . . . . 11 (𝑗 = 𝑦 → (∀𝑘𝐵 𝐶 ∈ ℂ ↔ ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3430, 33rspc 2716 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑗𝐴𝑘𝐵 𝐶 ∈ ℂ → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ))
3517, 27, 34sylc 61 . . . . . . . . 9 (𝜑 → ∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
3635r19.21bi 2461 . . . . . . . 8 ((𝜑𝑘𝑦 / 𝑗𝐵) → 𝑦 / 𝑗𝐶 ∈ ℂ)
3725, 36fsumcl 10790 . . . . . . 7 (𝜑 → Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ)
38 csbeq1 2936 . . . . . . . . 9 (𝑚 = 𝑦𝑚 / 𝑗𝐵 = 𝑦 / 𝑗𝐵)
39 csbeq1 2936 . . . . . . . . . 10 (𝑚 = 𝑦𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4039adantr 270 . . . . . . . . 9 ((𝑚 = 𝑦𝑘𝑚 / 𝑗𝐵) → 𝑚 / 𝑗𝐶 = 𝑦 / 𝑗𝐶)
4138, 40sumeq12dv 10757 . . . . . . . 8 (𝑚 = 𝑦 → Σ𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4241sumsn 10801 . . . . . . 7 ((𝑦𝐴 ∧ Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ) → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
4317, 37, 42syl2anc 403 . . . . . 6 (𝜑 → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶)
44 nfcv 2228 . . . . . . . 8 𝑚𝑦 / 𝑗𝐶
45 nfcsb1v 2963 . . . . . . . 8 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶
46 csbeq1a 2941 . . . . . . . 8 (𝑘 = 𝑚𝑦 / 𝑗𝐶 = 𝑚 / 𝑘𝑦 / 𝑗𝐶)
4744, 45, 46cbvsumi 10747 . . . . . . 7 Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶
48 csbeq1 2936 . . . . . . . . 9 (𝑚 = (2nd𝑧) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
49 snfig 6529 . . . . . . . . . . 11 (𝑦 ∈ V → {𝑦} ∈ Fin)
5049elv 2623 . . . . . . . . . 10 {𝑦} ∈ Fin
51 xpfi 6638 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ 𝑦 / 𝑗𝐵 ∈ Fin) → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
5250, 25, 51sylancr 405 . . . . . . . . 9 (𝜑 → ({𝑦} × 𝑦 / 𝑗𝐵) ∈ Fin)
53 2ndconst 5987 . . . . . . . . . 10 (𝑦𝐴 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
5417, 53syl 14 . . . . . . . . 9 (𝜑 → (2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵)):({𝑦} × 𝑦 / 𝑗𝐵)–1-1-onto𝑦 / 𝑗𝐵)
55 fvres 5329 . . . . . . . . . 10 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5655adantl 271 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((2nd ↾ ({𝑦} × 𝑦 / 𝑗𝐵))‘𝑧) = (2nd𝑧))
5745nfel1 2239 . . . . . . . . . . 11 𝑘𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ
5846eleq1d 2156 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝑦 / 𝑗𝐶 ∈ ℂ ↔ 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
5957, 58rspc 2716 . . . . . . . . . 10 (𝑚𝑦 / 𝑗𝐵 → (∀𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 ∈ ℂ → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ))
6035, 59mpan9 275 . . . . . . . . 9 ((𝜑𝑚𝑦 / 𝑗𝐵) → 𝑚 / 𝑘𝑦 / 𝑗𝐶 ∈ ℂ)
6148, 52, 54, 56, 60fsumf1o 10778 . . . . . . . 8 (𝜑 → Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
62 elxp 4455 . . . . . . . . . . . 12 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)))
63 nfv 1466 . . . . . . . . . . . . . . 15 𝑗 𝑧 = ⟨𝑚, 𝑘
64 nfv 1466 . . . . . . . . . . . . . . . 16 𝑗 𝑚 ∈ {𝑦}
6520nfcri 2222 . . . . . . . . . . . . . . . 16 𝑗 𝑘𝑦 / 𝑗𝐵
6664, 65nfan 1502 . . . . . . . . . . . . . . 15 𝑗(𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)
6763, 66nfan 1502 . . . . . . . . . . . . . 14 𝑗(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
6867nfex 1573 . . . . . . . . . . . . 13 𝑗𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵))
69 nfv 1466 . . . . . . . . . . . . 13 𝑚𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))
70 opeq1 3622 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
7170eqeq2d 2099 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → (𝑧 = ⟨𝑚, 𝑘⟩ ↔ 𝑧 = ⟨𝑗, 𝑘⟩))
72 eqtr2 2106 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 = 𝑗𝑚 = 𝑦) → 𝑗 = 𝑦)
7372, 22syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝑚 = 𝑗𝑚 = 𝑦) → 𝐵 = 𝑦 / 𝑗𝐵)
7473eleq2d 2157 . . . . . . . . . . . . . . . . . 18 ((𝑚 = 𝑗𝑚 = 𝑦) → (𝑘𝐵𝑘𝑦 / 𝑗𝐵))
7574pm5.32da 440 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → ((𝑚 = 𝑦𝑘𝐵) ↔ (𝑚 = 𝑦𝑘𝑦 / 𝑗𝐵)))
76 velsn 3463 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ {𝑦} ↔ 𝑚 = 𝑦)
7776anbi1i 446 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑚 = 𝑦𝑘𝑦 / 𝑗𝐵))
7875, 77syl6rbbr 197 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑚 = 𝑦𝑘𝐵)))
79 equequ1 1645 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑗 → (𝑚 = 𝑦𝑗 = 𝑦))
8079anbi1d 453 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑗 → ((𝑚 = 𝑦𝑘𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
8178, 80bitrd 186 . . . . . . . . . . . . . . 15 (𝑚 = 𝑗 → ((𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵) ↔ (𝑗 = 𝑦𝑘𝐵)))
8271, 81anbi12d 457 . . . . . . . . . . . . . 14 (𝑚 = 𝑗 → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ (𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8382exbidv 1753 . . . . . . . . . . . . 13 (𝑚 = 𝑗 → (∃𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵))))
8468, 69, 83cbvex 1686 . . . . . . . . . . . 12 (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑦} ∧ 𝑘𝑦 / 𝑗𝐵)) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
8562, 84bitri 182 . . . . . . . . . . 11 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) ↔ ∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)))
86 nfv 1466 . . . . . . . . . . . 12 𝑗𝜑
87 nfcv 2228 . . . . . . . . . . . . . 14 𝑗(2nd𝑧)
8887, 28nfcsb 2965 . . . . . . . . . . . . 13 𝑗(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
8988nfeq2 2240 . . . . . . . . . . . 12 𝑗 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
90 nfv 1466 . . . . . . . . . . . . 13 𝑘𝜑
91 nfcsb1v 2963 . . . . . . . . . . . . . 14 𝑘(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
9291nfeq2 2240 . . . . . . . . . . . . 13 𝑘 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶
93 fsum2d.1 . . . . . . . . . . . . . . . 16 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐷 = 𝐶)
9493ad2antlr 473 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = 𝐶)
9531ad2antrl 474 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐶 = 𝑦 / 𝑗𝐶)
96 fveq2 5305 . . . . . . . . . . . . . . . . . 18 (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd𝑧) = (2nd ‘⟨𝑗, 𝑘⟩))
97 vex 2622 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
98 vex 2622 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ V
9997, 98op2nd 5918 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨𝑗, 𝑘⟩) = 𝑘
10096, 99syl6req 2137 . . . . . . . . . . . . . . . . 17 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd𝑧))
101100ad2antlr 473 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑘 = (2nd𝑧))
102 csbeq1a 2941 . . . . . . . . . . . . . . . 16 (𝑘 = (2nd𝑧) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
103101, 102syl 14 . . . . . . . . . . . . . . 15 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝑦 / 𝑗𝐶 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
10494, 95, 1033eqtrd 2124 . . . . . . . . . . . . . 14 (((𝜑𝑧 = ⟨𝑗, 𝑘⟩) ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
105104expl 370 . . . . . . . . . . . . 13 (𝜑 → ((𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10690, 92, 105exlimd 1533 . . . . . . . . . . . 12 (𝜑 → (∃𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10786, 89, 106exlimd 1533 . . . . . . . . . . 11 (𝜑 → (∃𝑗𝑘(𝑧 = ⟨𝑗, 𝑘⟩ ∧ (𝑗 = 𝑦𝑘𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
10885, 107syl5bi 150 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶))
109108imp 122 . . . . . . . . 9 ((𝜑𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝐷 = (2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
110109sumeq2dv 10753 . . . . . . . 8 (𝜑 → Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)(2nd𝑧) / 𝑘𝑦 / 𝑗𝐶)
11161, 110eqtr4d 2123 . . . . . . 7 (𝜑 → Σ𝑚 𝑦 / 𝑗𝐵𝑚 / 𝑘𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11247, 111syl5eq 2132 . . . . . 6 (𝜑 → Σ𝑘 𝑦 / 𝑗𝐵𝑦 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11343, 112eqtrd 2120 . . . . 5 (𝜑 → Σ𝑚 ∈ {𝑦𝑘 𝑚 / 𝑗𝐵𝑚 / 𝑗𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
11412, 113syl5eq 2132 . . . 4 (𝜑 → Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
115114adantr 270 . . 3 ((𝜑𝜓) → Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶 = Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷)
1163, 115oveq12d 5670 . 2 ((𝜑𝜓) → (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶) = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
117 fsum2d.5 . . . . 5 (𝜑 → ¬ 𝑦𝑥)
118 disjsn 3504 . . . . 5 ((𝑥 ∩ {𝑦}) = ∅ ↔ ¬ 𝑦𝑥)
119117, 118sylibr 132 . . . 4 (𝜑 → (𝑥 ∩ {𝑦}) = ∅)
120 eqidd 2089 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) = (𝑥 ∪ {𝑦}))
121 fsum2dlemstep.x . . . . 5 (𝜑𝑥 ∈ Fin)
12250a1i 9 . . . . 5 (𝜑 → {𝑦} ∈ Fin)
123 unfidisj 6630 . . . . 5 ((𝑥 ∈ Fin ∧ {𝑦} ∈ Fin ∧ (𝑥 ∩ {𝑦}) = ∅) → (𝑥 ∪ {𝑦}) ∈ Fin)
124121, 122, 119, 123syl3anc 1174 . . . 4 (𝜑 → (𝑥 ∪ {𝑦}) ∈ Fin)
12513sselda 3025 . . . . 5 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝑗𝐴)
12626anassrs 392 . . . . . 6 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
12718, 126fsumcl 10790 . . . . 5 ((𝜑𝑗𝐴) → Σ𝑘𝐵 𝐶 ∈ ℂ)
128125, 127syldan 276 . . . 4 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → Σ𝑘𝐵 𝐶 ∈ ℂ)
129119, 120, 124, 128fsumsplit 10797 . . 3 (𝜑 → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶))
130129adantr 270 . 2 ((𝜑𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = (Σ𝑗𝑥 Σ𝑘𝐵 𝐶 + Σ𝑗 ∈ {𝑦𝑘𝐵 𝐶))
131 eliun 3734 . . . . . . . . . 10 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ↔ ∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵))
132 xp1st 5936 . . . . . . . . . . . . . 14 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
133 elsni 3464 . . . . . . . . . . . . . 14 ((1st𝑧) ∈ {𝑗} → (1st𝑧) = 𝑗)
134132, 133syl 14 . . . . . . . . . . . . 13 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
135134adantl 271 . . . . . . . . . . . 12 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) = 𝑗)
136 simpl 107 . . . . . . . . . . . 12 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → 𝑗𝑥)
137135, 136eqeltrd 2164 . . . . . . . . . . 11 ((𝑗𝑥𝑧 ∈ ({𝑗} × 𝐵)) → (1st𝑧) ∈ 𝑥)
138137rexlimiva 2484 . . . . . . . . . 10 (∃𝑗𝑥 𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
139131, 138sylbi 119 . . . . . . . . 9 (𝑧 𝑗𝑥 ({𝑗} × 𝐵) → (1st𝑧) ∈ 𝑥)
140 xp1st 5936 . . . . . . . . 9 (𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵) → (1st𝑧) ∈ {𝑦})
141139, 140anim12i 331 . . . . . . . 8 ((𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)) → ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
142 elin 3183 . . . . . . . 8 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ↔ (𝑧 𝑗𝑥 ({𝑗} × 𝐵) ∧ 𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)))
143 elin 3183 . . . . . . . 8 ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ ((1st𝑧) ∈ 𝑥 ∧ (1st𝑧) ∈ {𝑦}))
144141, 142, 1433imtr4i 199 . . . . . . 7 (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → (1st𝑧) ∈ (𝑥 ∩ {𝑦}))
145119eleq2d 2157 . . . . . . . 8 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) ↔ (1st𝑧) ∈ ∅))
146 noel 3290 . . . . . . . . 9 ¬ (1st𝑧) ∈ ∅
147146pm2.21i 610 . . . . . . . 8 ((1st𝑧) ∈ ∅ → 𝑧 ∈ ∅)
148145, 147syl6bi 161 . . . . . . 7 (𝜑 → ((1st𝑧) ∈ (𝑥 ∩ {𝑦}) → 𝑧 ∈ ∅))
149144, 148syl5 32 . . . . . 6 (𝜑 → (𝑧 ∈ ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) → 𝑧 ∈ ∅))
150149ssrdv 3031 . . . . 5 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅)
151 ss0 3323 . . . . 5 (( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) ⊆ ∅ → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
152150, 151syl 14 . . . 4 (𝜑 → ( 𝑗𝑥 ({𝑗} × 𝐵) ∩ ({𝑦} × 𝑦 / 𝑗𝐵)) = ∅)
153 iunxun 3809 . . . . . 6 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵))
154 nfcv 2228 . . . . . . . . 9 𝑚({𝑗} × 𝐵)
155 nfcv 2228 . . . . . . . . . 10 𝑗{𝑚}
156155, 5nfxp 4464 . . . . . . . . 9 𝑗({𝑚} × 𝑚 / 𝑗𝐵)
157 sneq 3457 . . . . . . . . . 10 (𝑗 = 𝑚 → {𝑗} = {𝑚})
158157, 8xpeq12d 4463 . . . . . . . . 9 (𝑗 = 𝑚 → ({𝑗} × 𝐵) = ({𝑚} × 𝑚 / 𝑗𝐵))
159154, 156, 158cbviun 3767 . . . . . . . 8 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵)
160 sneq 3457 . . . . . . . . . 10 (𝑚 = 𝑦 → {𝑚} = {𝑦})
161160, 38xpeq12d 4463 . . . . . . . . 9 (𝑚 = 𝑦 → ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵))
16215, 161iunxsn 3806 . . . . . . . 8 𝑚 ∈ {𝑦} ({𝑚} × 𝑚 / 𝑗𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
163159, 162eqtri 2108 . . . . . . 7 𝑗 ∈ {𝑦} ({𝑗} × 𝐵) = ({𝑦} × 𝑦 / 𝑗𝐵)
164163uneq2i 3151 . . . . . 6 ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑦} ({𝑗} × 𝐵)) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
165153, 164eqtri 2108 . . . . 5 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵))
166165a1i 9 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) = ( 𝑗𝑥 ({𝑗} × 𝐵) ∪ ({𝑦} × 𝑦 / 𝑗𝐵)))
167 snfig 6529 . . . . . . . 8 (𝑗 ∈ V → {𝑗} ∈ Fin)
168167elv 2623 . . . . . . 7 {𝑗} ∈ Fin
169125, 18syldan 276 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → 𝐵 ∈ Fin)
170 xpfi 6638 . . . . . . 7 (({𝑗} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑗} × 𝐵) ∈ Fin)
171168, 169, 170sylancr 405 . . . . . 6 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ({𝑗} × 𝐵) ∈ Fin)
172171ralrimiva 2446 . . . . 5 (𝜑 → ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
173 disjsnxp 6002 . . . . . 6 Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)
174173a1i 9 . . . . 5 (𝜑Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵))
175 iunfidisj 6653 . . . . 5 (((𝑥 ∪ {𝑦}) ∈ Fin ∧ ∀𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin ∧ Disj 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
176124, 172, 174, 175syl3anc 1174 . . . 4 (𝜑 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ∈ Fin)
177 eliun 3734 . . . . . 6 (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) ↔ ∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵))
178 elxp 4455 . . . . . . . 8 (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)))
179 simprl 498 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑚, 𝑘⟩)
180 simprrl 506 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 ∈ {𝑗})
181 elsni 3464 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑗} → 𝑚 = 𝑗)
182180, 181syl 14 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑚 = 𝑗)
183182opeq1d 3628 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → ⟨𝑚, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
184179, 183eqtrd 2120 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑧 = ⟨𝑗, 𝑘⟩)
185184, 93syl 14 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 = 𝐶)
186 simpll 496 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝜑)
187125adantr 270 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑗𝐴)
188 simprrr 507 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝑘𝐵)
189186, 187, 188, 26syl12anc 1172 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐶 ∈ ℂ)
190185, 189eqeltrd 2164 . . . . . . . . . 10 (((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) ∧ (𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵))) → 𝐷 ∈ ℂ)
191190ex 113 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → ((𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
192191exlimdvv 1825 . . . . . . . 8 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (∃𝑚𝑘(𝑧 = ⟨𝑚, 𝑘⟩ ∧ (𝑚 ∈ {𝑗} ∧ 𝑘𝐵)) → 𝐷 ∈ ℂ))
193178, 192syl5bi 150 . . . . . . 7 ((𝜑𝑗 ∈ (𝑥 ∪ {𝑦})) → (𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
194193rexlimdva 2489 . . . . . 6 (𝜑 → (∃𝑗 ∈ (𝑥 ∪ {𝑦})𝑧 ∈ ({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
195177, 194syl5bi 150 . . . . 5 (𝜑 → (𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵) → 𝐷 ∈ ℂ))
196195imp 122 . . . 4 ((𝜑𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)) → 𝐷 ∈ ℂ)
197152, 166, 176, 196fsumsplit 10797 . . 3 (𝜑 → Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
198197adantr 270 . 2 ((𝜑𝜓) → Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷 = (Σ𝑧 𝑗𝑥 ({𝑗} × 𝐵)𝐷 + Σ𝑧 ∈ ({𝑦} × 𝑦 / 𝑗𝐵)𝐷))
199116, 130, 1983eqtr4d 2130 1 ((𝜑𝜓) → Σ𝑗 ∈ (𝑥 ∪ {𝑦})Σ𝑘𝐵 𝐶 = Σ𝑧 𝑗 ∈ (𝑥 ∪ {𝑦})({𝑗} × 𝐵)𝐷)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103   = wceq 1289  wex 1426  wcel 1438  wral 2359  wrex 2360  Vcvv 2619  csb 2933  cun 2997  cin 2998  wss 2999  c0 3286  {csn 3446  cop 3449   ciun 3730  Disj wdisj 3822   × cxp 4436  cres 4440  1-1-ontowf1o 5014  cfv 5015  (class class class)co 5652  1st c1st 5909  2nd c2nd 5910  Fincfn 6455  cc 7346   + caddc 7351  Σcsu 10738
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 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403  ax-cnex 7434  ax-resscn 7435  ax-1cn 7436  ax-1re 7437  ax-icn 7438  ax-addcl 7439  ax-addrcl 7440  ax-mulcl 7441  ax-mulrcl 7442  ax-addcom 7443  ax-mulcom 7444  ax-addass 7445  ax-mulass 7446  ax-distr 7447  ax-i2m1 7448  ax-0lt1 7449  ax-1rid 7450  ax-0id 7451  ax-rnegex 7452  ax-precex 7453  ax-cnre 7454  ax-pre-ltirr 7455  ax-pre-ltwlin 7456  ax-pre-lttrn 7457  ax-pre-apti 7458  ax-pre-ltadd 7459  ax-pre-mulgt0 7460  ax-pre-mulext 7461  ax-arch 7462  ax-caucvg 7463
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rmo 2367  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-if 3394  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-disj 3823  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-id 4120  df-po 4123  df-iso 4124  df-iord 4193  df-on 4195  df-ilim 4196  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-isom 5024  df-riota 5608  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-irdg 6135  df-frec 6156  df-1o 6181  df-oadd 6185  df-er 6290  df-en 6456  df-dom 6457  df-fin 6458  df-pnf 7522  df-mnf 7523  df-xr 7524  df-ltxr 7525  df-le 7526  df-sub 7653  df-neg 7654  df-reap 8050  df-ap 8057  df-div 8138  df-inn 8421  df-2 8479  df-3 8480  df-4 8481  df-n0 8672  df-z 8749  df-uz 9018  df-q 9103  df-rp 9133  df-fz 9423  df-fzo 9550  df-iseq 9849  df-seq3 9850  df-exp 9951  df-ihash 10180  df-cj 10272  df-re 10273  df-im 10274  df-rsqrt 10427  df-abs 10428  df-clim 10663  df-isum 10739
This theorem is referenced by:  fsum2d  10825
  Copyright terms: Public domain W3C validator