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

Theorem fsumrlim 14917
Description: Limit of a finite sum of converging sequences. Note that 𝐶(𝑘) is a collection of functions with implicit parameter 𝑘, each of which converges to 𝐷(𝑘) as 𝑛 ⇝ +∞. (Contributed by Mario Carneiro, 22-May-2016.)
Hypotheses
Ref Expression
fsumrlim.1 (𝜑𝐴 ⊆ ℝ)
fsumrlim.2 (𝜑𝐵 ∈ Fin)
fsumrlim.3 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶𝑉)
fsumrlim.4 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ⇝𝑟 𝐷)
Assertion
Ref Expression
fsumrlim (𝜑 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷)
Distinct variable groups:   𝑥,𝑘,𝐴   𝐵,𝑘,𝑥   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐶(𝑥,𝑘)   𝐷(𝑥,𝑘)   𝑉(𝑥,𝑘)

Proof of Theorem fsumrlim
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3848 . 2 𝐵𝐵
2 fsumrlim.2 . . 3 (𝜑𝐵 ∈ Fin)
3 sseq1 3851 . . . . . 6 (𝑤 = ∅ → (𝑤𝐵 ↔ ∅ ⊆ 𝐵))
4 sumeq1 14796 . . . . . . . . 9 (𝑤 = ∅ → Σ𝑘𝑤 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
5 sum0 14829 . . . . . . . . 9 Σ𝑘 ∈ ∅ 𝐶 = 0
64, 5syl6eq 2877 . . . . . . . 8 (𝑤 = ∅ → Σ𝑘𝑤 𝐶 = 0)
76mpteq2dv 4968 . . . . . . 7 (𝑤 = ∅ → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ 0))
8 sumeq1 14796 . . . . . . . 8 (𝑤 = ∅ → Σ𝑘𝑤 𝐷 = Σ𝑘 ∈ ∅ 𝐷)
9 sum0 14829 . . . . . . . 8 Σ𝑘 ∈ ∅ 𝐷 = 0
108, 9syl6eq 2877 . . . . . . 7 (𝑤 = ∅ → Σ𝑘𝑤 𝐷 = 0)
117, 10breq12d 4886 . . . . . 6 (𝑤 = ∅ → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷 ↔ (𝑥𝐴 ↦ 0) ⇝𝑟 0))
123, 11imbi12d 336 . . . . 5 (𝑤 = ∅ → ((𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷) ↔ (∅ ⊆ 𝐵 → (𝑥𝐴 ↦ 0) ⇝𝑟 0)))
1312imbi2d 332 . . . 4 (𝑤 = ∅ → ((𝜑 → (𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷)) ↔ (𝜑 → (∅ ⊆ 𝐵 → (𝑥𝐴 ↦ 0) ⇝𝑟 0))))
14 sseq1 3851 . . . . . 6 (𝑤 = 𝑦 → (𝑤𝐵𝑦𝐵))
15 sumeq1 14796 . . . . . . . 8 (𝑤 = 𝑦 → Σ𝑘𝑤 𝐶 = Σ𝑘𝑦 𝐶)
1615mpteq2dv 4968 . . . . . . 7 (𝑤 = 𝑦 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶))
17 sumeq1 14796 . . . . . . 7 (𝑤 = 𝑦 → Σ𝑘𝑤 𝐷 = Σ𝑘𝑦 𝐷)
1816, 17breq12d 4886 . . . . . 6 (𝑤 = 𝑦 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷 ↔ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷))
1914, 18imbi12d 336 . . . . 5 (𝑤 = 𝑦 → ((𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷) ↔ (𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷)))
2019imbi2d 332 . . . 4 (𝑤 = 𝑦 → ((𝜑 → (𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷)) ↔ (𝜑 → (𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷))))
21 sseq1 3851 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤𝐵 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐵))
22 sumeq1 14796 . . . . . . . 8 (𝑤 = (𝑦 ∪ {𝑧}) → Σ𝑘𝑤 𝐶 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶)
2322mpteq2dv 4968 . . . . . . 7 (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶))
24 sumeq1 14796 . . . . . . 7 (𝑤 = (𝑦 ∪ {𝑧}) → Σ𝑘𝑤 𝐷 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)
2523, 24breq12d 4886 . . . . . 6 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷 ↔ (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))
2621, 25imbi12d 336 . . . . 5 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))
2726imbi2d 332 . . . 4 (𝑤 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷)) ↔ (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))))
28 sseq1 3851 . . . . . 6 (𝑤 = 𝐵 → (𝑤𝐵𝐵𝐵))
29 sumeq1 14796 . . . . . . . 8 (𝑤 = 𝐵 → Σ𝑘𝑤 𝐶 = Σ𝑘𝐵 𝐶)
3029mpteq2dv 4968 . . . . . . 7 (𝑤 = 𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) = (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶))
31 sumeq1 14796 . . . . . . 7 (𝑤 = 𝐵 → Σ𝑘𝑤 𝐷 = Σ𝑘𝐵 𝐷)
3230, 31breq12d 4886 . . . . . 6 (𝑤 = 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷 ↔ (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷))
3328, 32imbi12d 336 . . . . 5 (𝑤 = 𝐵 → ((𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷) ↔ (𝐵𝐵 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷)))
3433imbi2d 332 . . . 4 (𝑤 = 𝐵 → ((𝜑 → (𝑤𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑤 𝐶) ⇝𝑟 Σ𝑘𝑤 𝐷)) ↔ (𝜑 → (𝐵𝐵 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷))))
35 fsumrlim.1 . . . . . 6 (𝜑𝐴 ⊆ ℝ)
36 0cn 10348 . . . . . 6 0 ∈ ℂ
37 rlimconst 14652 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 0 ∈ ℂ) → (𝑥𝐴 ↦ 0) ⇝𝑟 0)
3835, 36, 37sylancl 580 . . . . 5 (𝜑 → (𝑥𝐴 ↦ 0) ⇝𝑟 0)
3938a1d 25 . . . 4 (𝜑 → (∅ ⊆ 𝐵 → (𝑥𝐴 ↦ 0) ⇝𝑟 0))
40 ssun1 4003 . . . . . . . . . 10 𝑦 ⊆ (𝑦 ∪ {𝑧})
41 sstr 3835 . . . . . . . . . 10 ((𝑦 ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → 𝑦𝐵)
4240, 41mpan 681 . . . . . . . . 9 ((𝑦 ∪ {𝑧}) ⊆ 𝐵𝑦𝐵)
4342imim1i 63 . . . . . . . 8 ((𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷))
44 sumex 14795 . . . . . . . . . . . . . 14 Σ𝑘𝑦 𝑤 / 𝑥𝐶 ∈ V
4544a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) ∧ 𝑤𝐴) → Σ𝑘𝑦 𝑤 / 𝑥𝐶 ∈ V)
46 simprr 789 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ⊆ 𝐵)
4746unssbd 4018 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → {𝑧} ⊆ 𝐵)
48 vex 3417 . . . . . . . . . . . . . . . . . . . . 21 𝑧 ∈ V
4948snss 4535 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐵 ↔ {𝑧} ⊆ 𝐵)
5047, 49sylibr 226 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧𝐵)
5150adantr 474 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧𝐵)
52 fsumrlim.3 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐶𝑉)
5352anass1rs 645 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶𝑉)
54 fsumrlim.4 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘𝐵) → (𝑥𝐴𝐶) ⇝𝑟 𝐷)
5553, 54rlimmptrcl 14715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘𝐵) ∧ 𝑥𝐴) → 𝐶 ∈ ℂ)
5655an32s 642 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
5756adantllr 710 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ ℂ)
5857ralrimiva 3175 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → ∀𝑘𝐵 𝐶 ∈ ℂ)
59 nfcsb1v 3773 . . . . . . . . . . . . . . . . . . . 20 𝑘𝑧 / 𝑘𝐶
6059nfel1 2984 . . . . . . . . . . . . . . . . . . 19 𝑘𝑧 / 𝑘𝐶 ∈ ℂ
61 csbeq1a 3766 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑧𝐶 = 𝑧 / 𝑘𝐶)
6261eleq1d 2891 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑧 → (𝐶 ∈ ℂ ↔ 𝑧 / 𝑘𝐶 ∈ ℂ))
6360, 62rspc 3520 . . . . . . . . . . . . . . . . . 18 (𝑧𝐵 → (∀𝑘𝐵 𝐶 ∈ ℂ → 𝑧 / 𝑘𝐶 ∈ ℂ))
6451, 58, 63sylc 65 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → 𝑧 / 𝑘𝐶 ∈ ℂ)
6564ralrimiva 3175 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ ℂ)
6665adantr 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → ∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ ℂ)
67 nfcsb1v 3773 . . . . . . . . . . . . . . . . 17 𝑥𝑤 / 𝑥𝑧 / 𝑘𝐶
6867nfel1 2984 . . . . . . . . . . . . . . . 16 𝑥𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ ℂ
69 csbeq1a 3766 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤𝑧 / 𝑘𝐶 = 𝑤 / 𝑥𝑧 / 𝑘𝐶)
7069eleq1d 2891 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑧 / 𝑘𝐶 ∈ ℂ ↔ 𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ ℂ))
7168, 70rspc 3520 . . . . . . . . . . . . . . 15 (𝑤𝐴 → (∀𝑥𝐴 𝑧 / 𝑘𝐶 ∈ ℂ → 𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ ℂ))
7266, 71mpan9 502 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) ∧ 𝑤𝐴) → 𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ ℂ)
73 elex 3429 . . . . . . . . . . . . . 14 (𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ ℂ → 𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
7472, 73syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) ∧ 𝑤𝐴) → 𝑤 / 𝑥𝑧 / 𝑘𝐶 ∈ V)
75 nfcv 2969 . . . . . . . . . . . . . . 15 𝑤Σ𝑘𝑦 𝐶
76 nfcv 2969 . . . . . . . . . . . . . . . 16 𝑥𝑦
77 nfcsb1v 3773 . . . . . . . . . . . . . . . 16 𝑥𝑤 / 𝑥𝐶
7876, 77nfsum 14798 . . . . . . . . . . . . . . 15 𝑥Σ𝑘𝑦 𝑤 / 𝑥𝐶
79 csbeq1a 3766 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤𝐶 = 𝑤 / 𝑥𝐶)
8079sumeq2sdv 14812 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → Σ𝑘𝑦 𝐶 = Σ𝑘𝑦 𝑤 / 𝑥𝐶)
8175, 78, 80cbvmpt 4972 . . . . . . . . . . . . . 14 (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) = (𝑤𝐴 ↦ Σ𝑘𝑦 𝑤 / 𝑥𝐶)
82 simpr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷)
8381, 82syl5eqbrr 4909 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑤𝐴 ↦ Σ𝑘𝑦 𝑤 / 𝑥𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷)
84 nfcv 2969 . . . . . . . . . . . . . . 15 𝑤𝑧 / 𝑘𝐶
8584, 67, 69cbvmpt 4972 . . . . . . . . . . . . . 14 (𝑥𝐴𝑧 / 𝑘𝐶) = (𝑤𝐴𝑤 / 𝑥𝑧 / 𝑘𝐶)
8654ralrimiva 3175 . . . . . . . . . . . . . . . . 17 (𝜑 → ∀𝑘𝐵 (𝑥𝐴𝐶) ⇝𝑟 𝐷)
8786adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑘𝐵 (𝑥𝐴𝐶) ⇝𝑟 𝐷)
88 nfcv 2969 . . . . . . . . . . . . . . . . . . 19 𝑘𝐴
8988, 59nfmpt 4969 . . . . . . . . . . . . . . . . . 18 𝑘(𝑥𝐴𝑧 / 𝑘𝐶)
90 nfcv 2969 . . . . . . . . . . . . . . . . . 18 𝑘𝑟
91 nfcsb1v 3773 . . . . . . . . . . . . . . . . . 18 𝑘𝑧 / 𝑘𝐷
9289, 90, 91nfbr 4920 . . . . . . . . . . . . . . . . 17 𝑘(𝑥𝐴𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷
9361mpteq2dv 4968 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑧 → (𝑥𝐴𝐶) = (𝑥𝐴𝑧 / 𝑘𝐶))
94 csbeq1a 3766 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑧𝐷 = 𝑧 / 𝑘𝐷)
9593, 94breq12d 4886 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑧 → ((𝑥𝐴𝐶) ⇝𝑟 𝐷 ↔ (𝑥𝐴𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷))
9692, 95rspc 3520 . . . . . . . . . . . . . . . 16 (𝑧𝐵 → (∀𝑘𝐵 (𝑥𝐴𝐶) ⇝𝑟 𝐷 → (𝑥𝐴𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷))
9750, 87, 96sylc 65 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷)
9897adantr 474 . . . . . . . . . . . . . 14 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑥𝐴𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷)
9985, 98syl5eqbrr 4909 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑤𝐴𝑤 / 𝑥𝑧 / 𝑘𝐶) ⇝𝑟 𝑧 / 𝑘𝐷)
10045, 74, 83, 99rlimadd 14750 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑤𝐴 ↦ (Σ𝑘𝑦 𝑤 / 𝑥𝐶 + 𝑤 / 𝑥𝑧 / 𝑘𝐶)) ⇝𝑟𝑘𝑦 𝐷 + 𝑧 / 𝑘𝐷))
101 simprl 787 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ¬ 𝑧𝑦)
102 disjsn 4465 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
103101, 102sylibr 226 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∩ {𝑧}) = ∅)
104103adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑦 ∩ {𝑧}) = ∅)
105 eqidd 2826 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
1062adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝐵 ∈ Fin)
107 ssfi 8449 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → (𝑦 ∪ {𝑧}) ∈ Fin)
108106, 46, 107syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ∈ Fin)
109108adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (𝑦 ∪ {𝑧}) ∈ Fin)
11046sselda 3827 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘𝐵)
111110adantlr 706 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘𝐵)
112111, 57syldan 585 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐶 ∈ ℂ)
113104, 105, 109, 112fsumsplit 14848 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶))
114 nfcv 2969 . . . . . . . . . . . . . . . . . . 19 𝑤𝐶
115 nfcsb1v 3773 . . . . . . . . . . . . . . . . . . 19 𝑘𝑤 / 𝑘𝐶
116 csbeq1a 3766 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑤𝐶 = 𝑤 / 𝑘𝐶)
117114, 115, 116cbvsumi 14804 . . . . . . . . . . . . . . . . . 18 Σ𝑘 ∈ {𝑧}𝐶 = Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐶
118 csbeq1 3760 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧𝑤 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
119118sumsn 14852 . . . . . . . . . . . . . . . . . . 19 ((𝑧𝐵𝑧 / 𝑘𝐶 ∈ ℂ) → Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
12051, 64, 119syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐶 = 𝑧 / 𝑘𝐶)
121117, 120syl5eq 2873 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑘 ∈ {𝑧}𝐶 = 𝑧 / 𝑘𝐶)
122121oveq2d 6921 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → (Σ𝑘𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶) = (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶))
123113, 122eqtrd 2861 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶))
124123mpteq2dva 4967 . . . . . . . . . . . . . 14 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑥𝐴 ↦ (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶)))
125124adantr 474 . . . . . . . . . . . . 13 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑥𝐴 ↦ (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶)))
126 nfcv 2969 . . . . . . . . . . . . . 14 𝑤𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶)
127 nfcv 2969 . . . . . . . . . . . . . . 15 𝑥 +
12878, 127, 67nfov 6935 . . . . . . . . . . . . . 14 𝑥𝑘𝑦 𝑤 / 𝑥𝐶 + 𝑤 / 𝑥𝑧 / 𝑘𝐶)
12980, 69oveq12d 6923 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶) = (Σ𝑘𝑦 𝑤 / 𝑥𝐶 + 𝑤 / 𝑥𝑧 / 𝑘𝐶))
130126, 128, 129cbvmpt 4972 . . . . . . . . . . . . 13 (𝑥𝐴 ↦ (Σ𝑘𝑦 𝐶 + 𝑧 / 𝑘𝐶)) = (𝑤𝐴 ↦ (Σ𝑘𝑦 𝑤 / 𝑥𝐶 + 𝑤 / 𝑥𝑧 / 𝑘𝐶))
131125, 130syl6eq 2877 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑤𝐴 ↦ (Σ𝑘𝑦 𝑤 / 𝑥𝐶 + 𝑤 / 𝑥𝑧 / 𝑘𝐶)))
132 eqidd 2826 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
133 rlimcl 14611 . . . . . . . . . . . . . . . . . 18 ((𝑥𝐴𝐶) ⇝𝑟 𝐷𝐷 ∈ ℂ)
13454, 133syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐵) → 𝐷 ∈ ℂ)
135134adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘𝐵) → 𝐷 ∈ ℂ)
136110, 135syldan 585 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐷 ∈ ℂ)
137103, 132, 108, 136fsumsplit 14848 . . . . . . . . . . . . . 14 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘𝑦 𝐷 + Σ𝑘 ∈ {𝑧}𝐷))
138 nfcv 2969 . . . . . . . . . . . . . . . . 17 𝑤𝐷
139 nfcsb1v 3773 . . . . . . . . . . . . . . . . 17 𝑘𝑤 / 𝑘𝐷
140 csbeq1a 3766 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑤𝐷 = 𝑤 / 𝑘𝐷)
141138, 139, 140cbvsumi 14804 . . . . . . . . . . . . . . . 16 Σ𝑘 ∈ {𝑧}𝐷 = Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐷
142135ralrimiva 3175 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑘𝐵 𝐷 ∈ ℂ)
14391nfel1 2984 . . . . . . . . . . . . . . . . . . 19 𝑘𝑧 / 𝑘𝐷 ∈ ℂ
14494eleq1d 2891 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑧 → (𝐷 ∈ ℂ ↔ 𝑧 / 𝑘𝐷 ∈ ℂ))
145143, 144rspc 3520 . . . . . . . . . . . . . . . . . 18 (𝑧𝐵 → (∀𝑘𝐵 𝐷 ∈ ℂ → 𝑧 / 𝑘𝐷 ∈ ℂ))
14650, 142, 145sylc 65 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧 / 𝑘𝐷 ∈ ℂ)
147 csbeq1 3760 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧𝑤 / 𝑘𝐷 = 𝑧 / 𝑘𝐷)
148147sumsn 14852 . . . . . . . . . . . . . . . . 17 ((𝑧𝐵𝑧 / 𝑘𝐷 ∈ ℂ) → Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐷 = 𝑧 / 𝑘𝐷)
14950, 146, 148syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑤 ∈ {𝑧}𝑤 / 𝑘𝐷 = 𝑧 / 𝑘𝐷)
150141, 149syl5eq 2873 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ {𝑧}𝐷 = 𝑧 / 𝑘𝐷)
151150oveq2d 6921 . . . . . . . . . . . . . 14 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (Σ𝑘𝑦 𝐷 + Σ𝑘 ∈ {𝑧}𝐷) = (Σ𝑘𝑦 𝐷 + 𝑧 / 𝑘𝐷))
152137, 151eqtrd 2861 . . . . . . . . . . . . 13 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘𝑦 𝐷 + 𝑧 / 𝑘𝐷))
153152adantr 474 . . . . . . . . . . . 12 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷 = (Σ𝑘𝑦 𝐷 + 𝑧 / 𝑘𝐷))
154100, 131, 1533brtr4d 4905 . . . . . . . . . . 11 (((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)
155154ex 403 . . . . . . . . . 10 ((𝜑 ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ((𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))
156155expr 450 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑧𝑦) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))
157156a2d 29 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑧𝑦) → (((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))
15843, 157syl5 34 . . . . . . 7 ((𝜑 ∧ ¬ 𝑧𝑦) → ((𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷)))
159158expcom 404 . . . . . 6 𝑧𝑦 → (𝜑 → ((𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))))
160159a2d 29 . . . . 5 𝑧𝑦 → ((𝜑 → (𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))))
161160adantl 475 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝜑 → (𝑦𝐵 → (𝑥𝐴 ↦ Σ𝑘𝑦 𝐶) ⇝𝑟 Σ𝑘𝑦 𝐷)) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ⇝𝑟 Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐷))))
16213, 20, 27, 34, 39, 161findcard2s 8470 . . 3 (𝐵 ∈ Fin → (𝜑 → (𝐵𝐵 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷)))
1632, 162mpcom 38 . 2 (𝜑 → (𝐵𝐵 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷))
1641, 163mpi 20 1 (𝜑 → (𝑥𝐴 ↦ Σ𝑘𝐵 𝐶) ⇝𝑟 Σ𝑘𝐵 𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386   = wceq 1656  wcel 2164  wral 3117  Vcvv 3414  csb 3757  cun 3796  cin 3797  wss 3798  c0 4144  {csn 4397   class class class wbr 4873  cmpt 4952  (class class class)co 6905  Fincfn 8222  cc 10250  cr 10251  0cc0 10252   + caddc 10255  𝑟 crli 14593  Σcsu 14793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330  ax-addf 10331
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-oi 8684  df-card 9078  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-n0 11619  df-z 11705  df-uz 11969  df-rp 12113  df-fz 12620  df-fzo 12761  df-seq 13096  df-exp 13155  df-hash 13411  df-cj 14216  df-re 14217  df-im 14218  df-sqrt 14352  df-abs 14353  df-clim 14596  df-rlim 14597  df-sum 14794
This theorem is referenced by:  climfsum  14926  logexprlim  25363  signsplypnf  31163
  Copyright terms: Public domain W3C validator