Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumesum Structured version   Visualization version   GIF version

Theorem gsumesum 30502
Description: Relate a group sum on (ℝ*𝑠s (0[,]+∞)) to a finite extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017.) (Proof shortened by AV, 12-Dec-2019.)
Hypotheses
Ref Expression
gsumesum.0 𝑘𝜑
gsumesum.1 (𝜑𝐴 ∈ Fin)
gsumesum.2 ((𝜑𝑘𝐴) → 𝐵 ∈ (0[,]+∞))
Assertion
Ref Expression
gsumesum (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = Σ*𝑘𝐴𝐵)
Distinct variable group:   𝐴,𝑘
Allowed substitution hints:   𝜑(𝑘)   𝐵(𝑘)

Proof of Theorem gsumesum
Dummy variables 𝑎 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumesum.0 . . 3 𝑘𝜑
2 nfcv 2906 . . 3 𝑘𝐴
3 gsumesum.1 . . 3 (𝜑𝐴 ∈ Fin)
4 gsumesum.2 . . 3 ((𝜑𝑘𝐴) → 𝐵 ∈ (0[,]+∞))
5 eqidd 2765 . . 3 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))
61, 2, 3, 4, 5esumval 30489 . 2 (𝜑 → Σ*𝑘𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))), ℝ*, < ))
7 xrltso 12173 . . . 4 < Or ℝ*
87a1i 11 . . 3 (𝜑 → < Or ℝ*)
9 iccssxr 12457 . . . 4 (0[,]+∞) ⊆ ℝ*
10 xrge0base 30066 . . . . 5 (0[,]+∞) = (Base‘(ℝ*𝑠s (0[,]+∞)))
11 xrge0cmn 20060 . . . . . 6 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
1211a1i 11 . . . . 5 (𝜑 → (ℝ*𝑠s (0[,]+∞)) ∈ CMnd)
134ex 401 . . . . . 6 (𝜑 → (𝑘𝐴𝐵 ∈ (0[,]+∞)))
141, 13ralrimi 3103 . . . . 5 (𝜑 → ∀𝑘𝐴 𝐵 ∈ (0[,]+∞))
1510, 12, 3, 14gsummptcl 18631 . . . 4 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ (0[,]+∞))
169, 15sseldi 3758 . . 3 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ℝ*)
17 pwidg 4329 . . . . . . 7 (𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴)
183, 17syl 17 . . . . . 6 (𝜑𝐴 ∈ 𝒫 𝐴)
1918, 3elind 3959 . . . . 5 (𝜑𝐴 ∈ (𝒫 𝐴 ∩ Fin))
20 eqidd 2765 . . . . 5 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
21 mpteq1 4895 . . . . . . 7 (𝑥 = 𝐴 → (𝑘𝑥𝐵) = (𝑘𝐴𝐵))
2221oveq2d 6857 . . . . . 6 (𝑥 = 𝐴 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
2322rspceeqv 3478 . . . . 5 ((𝐴 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))
2419, 20, 23syl2anc 579 . . . 4 (𝜑 → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))
25 eqid 2764 . . . . 5 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))
26 ovex 6873 . . . . 5 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) ∈ V
2725, 26elrnmpti 5544 . . . 4 (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))
2824, 27sylibr 225 . . 3 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))))
29 simpr 477 . . . . . 6 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → 𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))))
30 mpteq1 4895 . . . . . . . . 9 (𝑥 = 𝑎 → (𝑘𝑥𝐵) = (𝑘𝑎𝐵))
3130oveq2d 6857 . . . . . . . 8 (𝑥 = 𝑎 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
3231cbvmptv 4908 . . . . . . 7 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
33 ovex 6873 . . . . . . 7 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∈ V
3432, 33elrnmpti 5544 . . . . . 6 (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
3529, 34sylib 209 . . . . 5 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
3611a1i 11 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (ℝ*𝑠s (0[,]+∞)) ∈ CMnd)
37 inss2 3992 . . . . . . . . . . . 12 (𝒫 𝐴 ∩ Fin) ⊆ Fin
38 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
3937, 38sseldi 3758 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ Fin)
40 nfv 2009 . . . . . . . . . . . . 13 𝑘 𝑎 ∈ (𝒫 𝐴 ∩ Fin)
411, 40nfan 1998 . . . . . . . . . . . 12 𝑘(𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin))
42 simpll 783 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑎) → 𝜑)
43 inss1 3991 . . . . . . . . . . . . . . . . . 18 (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
4443sseli 3756 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
4544elpwid 4326 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎𝐴)
4645ad2antlr 718 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑎) → 𝑎𝐴)
47 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑎) → 𝑘𝑎)
4846, 47sseldd 3761 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑎) → 𝑘𝐴)
4942, 48, 4syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑎) → 𝐵 ∈ (0[,]+∞))
5049ex 401 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘𝑎𝐵 ∈ (0[,]+∞)))
5141, 50ralrimi 3103 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘𝑎 𝐵 ∈ (0[,]+∞))
5210, 36, 39, 51gsummptcl 18631 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∈ (0[,]+∞))
539, 52sseldi 3758 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∈ ℝ*)
54 diffi 8398 . . . . . . . . . . . . 13 (𝐴 ∈ Fin → (𝐴𝑎) ∈ Fin)
553, 54syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑎) ∈ Fin)
5655adantr 472 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐴𝑎) ∈ Fin)
57 simpll 783 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴𝑎)) → 𝜑)
58 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴𝑎)) → 𝑘 ∈ (𝐴𝑎))
5958eldifad 3743 . . . . . . . . . . . . . 14 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴𝑎)) → 𝑘𝐴)
6057, 59, 4syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ (𝐴𝑎)) → 𝐵 ∈ (0[,]+∞))
6160ex 401 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘 ∈ (𝐴𝑎) → 𝐵 ∈ (0[,]+∞)))
6241, 61ralrimi 3103 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘 ∈ (𝐴𝑎)𝐵 ∈ (0[,]+∞))
6310, 36, 56, 62gsummptcl 18631 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ (0[,]+∞))
649, 63sseldi 3758 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ ℝ*)
65 elxrge0 12484 . . . . . . . . . . 11 (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ (0[,]+∞) ↔ (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ ℝ* ∧ 0 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
6665simprbi 490 . . . . . . . . . 10 (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ (0[,]+∞) → 0 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)))
6763, 66syl 17 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)))
68 xraddge02 29904 . . . . . . . . . 10 ((((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∈ ℝ* ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ ℝ*) → (0 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)))))
6968imp 395 . . . . . . . . 9 (((((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∈ ℝ* ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)) ∈ ℝ*) ∧ 0 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
7053, 64, 67, 69syl21anc 866 . . . . . . . 8 ((𝜑𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
7170adantlr 706 . . . . . . 7 (((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
72 simpll 783 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝜑)
7345adantl 473 . . . . . . . 8 (((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎𝐴)
74 xrge00 30067 . . . . . . . . . 10 0 = (0g‘(ℝ*𝑠s (0[,]+∞)))
75 xrge0plusg 30068 . . . . . . . . . 10 +𝑒 = (+g‘(ℝ*𝑠s (0[,]+∞)))
7611a1i 11 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (ℝ*𝑠s (0[,]+∞)) ∈ CMnd)
773adantr 472 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝐴 ∈ Fin)
78 eqid 2764 . . . . . . . . . . . 12 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
791, 4, 78fmptdf 6576 . . . . . . . . . . 11 (𝜑 → (𝑘𝐴𝐵):𝐴⟶(0[,]+∞))
8079adantr 472 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (𝑘𝐴𝐵):𝐴⟶(0[,]+∞))
8178fnmpt 6197 . . . . . . . . . . . . 13 (∀𝑘𝐴 𝐵 ∈ (0[,]+∞) → (𝑘𝐴𝐵) Fn 𝐴)
8214, 81syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑘𝐴𝐵) Fn 𝐴)
83 c0ex 10286 . . . . . . . . . . . . 13 0 ∈ V
8483a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 ∈ V)
8582, 3, 84fndmfifsupp 8494 . . . . . . . . . . 11 (𝜑 → (𝑘𝐴𝐵) finSupp 0)
8685adantr 472 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (𝑘𝐴𝐵) finSupp 0)
87 disjdif 4199 . . . . . . . . . . 11 (𝑎 ∩ (𝐴𝑎)) = ∅
8887a1i 11 . . . . . . . . . 10 ((𝜑𝑎𝐴) → (𝑎 ∩ (𝐴𝑎)) = ∅)
89 undif 4208 . . . . . . . . . . . . 13 (𝑎𝐴 ↔ (𝑎 ∪ (𝐴𝑎)) = 𝐴)
9089biimpi 207 . . . . . . . . . . . 12 (𝑎𝐴 → (𝑎 ∪ (𝐴𝑎)) = 𝐴)
9190eqcomd 2770 . . . . . . . . . . 11 (𝑎𝐴𝐴 = (𝑎 ∪ (𝐴𝑎)))
9291adantl 473 . . . . . . . . . 10 ((𝜑𝑎𝐴) → 𝐴 = (𝑎 ∪ (𝐴𝑎)))
9310, 74, 75, 76, 77, 80, 86, 88, 92gsumsplit 18593 . . . . . . . . 9 ((𝜑𝑎𝐴) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = (((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ 𝑎)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ (𝐴𝑎)))))
94 resmpt 5625 . . . . . . . . . . . 12 (𝑎𝐴 → ((𝑘𝐴𝐵) ↾ 𝑎) = (𝑘𝑎𝐵))
9594oveq2d 6857 . . . . . . . . . . 11 (𝑎𝐴 → ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ 𝑎)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
9695adantl 473 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ 𝑎)) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)))
97 difss 3898 . . . . . . . . . . . . 13 (𝐴𝑎) ⊆ 𝐴
98 resmpt 5625 . . . . . . . . . . . . 13 ((𝐴𝑎) ⊆ 𝐴 → ((𝑘𝐴𝐵) ↾ (𝐴𝑎)) = (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))
9997, 98ax-mp 5 . . . . . . . . . . . 12 ((𝑘𝐴𝐵) ↾ (𝐴𝑎)) = (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)
10099oveq2i 6852 . . . . . . . . . . 11 ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ (𝐴𝑎))) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))
101100a1i 11 . . . . . . . . . 10 ((𝜑𝑎𝐴) → ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ (𝐴𝑎))) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵)))
10296, 101oveq12d 6859 . . . . . . . . 9 ((𝜑𝑎𝐴) → (((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ 𝑎)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg ((𝑘𝐴𝐵) ↾ (𝐴𝑎)))) = (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
10393, 102eqtrd 2798 . . . . . . . 8 ((𝜑𝑎𝐴) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
10472, 73, 103syl2anc 579 . . . . . . 7 (((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) +𝑒 ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘 ∈ (𝐴𝑎) ↦ 𝐵))))
10571, 104breqtrrd 4836 . . . . . 6 (((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
106105ralrimiva 3112 . . . . 5 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → ∀𝑎 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
107 r19.29r 3219 . . . . . 6 ((∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∧ ∀𝑎 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))))
108 breq1 4811 . . . . . . . 8 (𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) → (𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ↔ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))))
109108biimpar 469 . . . . . . 7 ((𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))) → 𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
110109rexlimivw 3175 . . . . . 6 (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∧ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))) → 𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
111107, 110syl 17 . . . . 5 ((∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ∧ ∀𝑎 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑎𝐵)) ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))) → 𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
11235, 106, 111syl2anc 579 . . . 4 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → 𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
11316adantr 472 . . . . 5 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ℝ*)
11411a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (ℝ*𝑠s (0[,]+∞)) ∈ CMnd)
115 simpr 477 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin))
11637, 115sseldi 3758 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin)
117 nfv 2009 . . . . . . . . . . . 12 𝑘 𝑥 ∈ (𝒫 𝐴 ∩ Fin)
1181, 117nfan 1998 . . . . . . . . . . 11 𝑘(𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin))
119 simpll 783 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝜑)
12043sseli 3756 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴)
121120ad2antlr 718 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝑥 ∈ 𝒫 𝐴)
122121elpwid 4326 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝑥𝐴)
123 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝑘𝑥)
124122, 123sseldd 3761 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝑘𝐴)
125119, 124, 4syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘𝑥) → 𝐵 ∈ (0[,]+∞))
126125ex 401 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘𝑥𝐵 ∈ (0[,]+∞)))
127118, 126ralrimi 3103 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘𝑥 𝐵 ∈ (0[,]+∞))
12810, 114, 116, 127gsummptcl 18631 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) ∈ (0[,]+∞))
1299, 128sseldi 3758 . . . . . . . 8 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) ∈ ℝ*)
130129ralrimiva 3112 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) ∈ ℝ*)
13125rnmptss 6581 . . . . . . 7 (∀𝑥 ∈ (𝒫 𝐴 ∩ Fin)((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)) ∈ ℝ* → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) ⊆ ℝ*)
132130, 131syl 17 . . . . . 6 (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))) ⊆ ℝ*)
133132sselda 3760 . . . . 5 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → 𝑦 ∈ ℝ*)
134 xrltnle 10358 . . . . . 6 ((((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ℝ*𝑦 ∈ ℝ*) → (((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) < 𝑦 ↔ ¬ 𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵))))
135134con2bid 345 . . . . 5 ((((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ∈ ℝ*𝑦 ∈ ℝ*) → (𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ↔ ¬ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) < 𝑦))
136113, 133, 135syl2anc 579 . . . 4 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → (𝑦 ≤ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) ↔ ¬ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) < 𝑦))
137112, 136mpbid 223 . . 3 ((𝜑𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵)))) → ¬ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) < 𝑦)
1388, 16, 28, 137supmax 8579 . 2 (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝑥𝐵))), ℝ*, < ) = ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)))
1396, 138eqtr2d 2799 1 (𝜑 → ((ℝ*𝑠s (0[,]+∞)) Σg (𝑘𝐴𝐵)) = Σ*𝑘𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wnf 1878  wcel 2155  wral 3054  wrex 3055  Vcvv 3349  cdif 3728  cun 3729  cin 3730  wss 3731  c0 4078  𝒫 cpw 4314   class class class wbr 4808  cmpt 4887   Or wor 5196  ran crn 5277  cres 5278   Fn wfn 6062  wf 6063  (class class class)co 6841  Fincfn 8159   finSupp cfsupp 8481  supcsup 8552  0cc0 10188  +∞cpnf 10324  *cxr 10326   < clt 10327  cle 10328   +𝑒 cxad 12143  [,]cicc 12379  s cress 16132   Σg cgsu 16368  *𝑠cxrs 16427  CMndccmn 18458  Σ*cesum 30470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-map 8061  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-fi 8523  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-q 11989  df-xadd 12146  df-ioo 12380  df-ioc 12381  df-ico 12382  df-icc 12383  df-fz 12533  df-fzo 12673  df-seq 13008  df-hash 13321  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-tset 16234  df-ple 16235  df-ds 16237  df-rest 16350  df-topn 16351  df-0g 16369  df-gsum 16370  df-topgen 16371  df-ordt 16428  df-xrs 16429  df-mre 16513  df-mrc 16514  df-acs 16516  df-ps 17467  df-tsr 17468  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-cntz 18014  df-cmn 18460  df-fbas 20015  df-fg 20016  df-top 20977  df-topon 20994  df-topsp 21016  df-bases 21029  df-ntr 21103  df-nei 21181  df-cn 21310  df-haus 21398  df-fil 21928  df-fm 22020  df-flim 22021  df-flf 22022  df-tsms 22208  df-esum 30471
This theorem is referenced by:  esumlub  30503
  Copyright terms: Public domain W3C validator