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

Theorem xrge0gsumle 23007
Description: A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.)
Hypotheses
Ref Expression
xrge0gsumle.g 𝐺 = (ℝ*𝑠s (0[,]+∞))
xrge0gsumle.a (𝜑𝐴𝑉)
xrge0gsumle.f (𝜑𝐹:𝐴⟶(0[,]+∞))
xrge0gsumle.b (𝜑𝐵 ∈ (𝒫 𝐴 ∩ Fin))
xrge0gsumle.c (𝜑𝐶𝐵)
Assertion
Ref Expression
xrge0gsumle (𝜑 → (𝐺 Σg (𝐹𝐶)) ≤ (𝐺 Σg (𝐹𝐵)))

Proof of Theorem xrge0gsumle
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 iccssxr 12545 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
2 xrge0gsumle.g . . . . . . . . . 10 𝐺 = (ℝ*𝑠s (0[,]+∞))
3 xrsbas 20123 . . . . . . . . . 10 * = (Base‘ℝ*𝑠)
42, 3ressbas2 16295 . . . . . . . . 9 ((0[,]+∞) ⊆ ℝ* → (0[,]+∞) = (Base‘𝐺))
51, 4ax-mp 5 . . . . . . . 8 (0[,]+∞) = (Base‘𝐺)
6 eqid 2826 . . . . . . . . . 10 (ℝ*𝑠s (ℝ* ∖ {-∞})) = (ℝ*𝑠s (ℝ* ∖ {-∞}))
76xrge0subm 20148 . . . . . . . . 9 (0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠s (ℝ* ∖ {-∞})))
8 xrex 12110 . . . . . . . . . . . . 13 * ∈ V
9 difexg 5034 . . . . . . . . . . . . 13 (ℝ* ∈ V → (ℝ* ∖ {-∞}) ∈ V)
108, 9ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) ∈ V
11 simpl 476 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
12 ge0nemnf 12293 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ≠ -∞)
1311, 12jca 509 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → (𝑥 ∈ ℝ*𝑥 ≠ -∞))
14 elxrge0 12572 . . . . . . . . . . . . . 14 (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
15 eldifsn 4537 . . . . . . . . . . . . . 14 (𝑥 ∈ (ℝ* ∖ {-∞}) ↔ (𝑥 ∈ ℝ*𝑥 ≠ -∞))
1613, 14, 153imtr4i 284 . . . . . . . . . . . . 13 (𝑥 ∈ (0[,]+∞) → 𝑥 ∈ (ℝ* ∖ {-∞}))
1716ssriv 3832 . . . . . . . . . . . 12 (0[,]+∞) ⊆ (ℝ* ∖ {-∞})
18 ressabs 16304 . . . . . . . . . . . 12 (((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})) → ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞)))
1910, 17, 18mp2an 685 . . . . . . . . . . 11 ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞))
202, 19eqtr4i 2853 . . . . . . . . . 10 𝐺 = ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞))
216xrs10 20146 . . . . . . . . . 10 0 = (0g‘(ℝ*𝑠s (ℝ* ∖ {-∞})))
2220, 21subm0 17710 . . . . . . . . 9 ((0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠s (ℝ* ∖ {-∞}))) → 0 = (0g𝐺))
237, 22ax-mp 5 . . . . . . . 8 0 = (0g𝐺)
24 xrge0cmn 20149 . . . . . . . . . 10 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
252, 24eqeltri 2903 . . . . . . . . 9 𝐺 ∈ CMnd
2625a1i 11 . . . . . . . 8 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
27 elfpw 8538 . . . . . . . . . 10 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠𝐴𝑠 ∈ Fin))
2827simprbi 492 . . . . . . . . 9 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin)
2928adantl 475 . . . . . . . 8 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin)
30 xrge0gsumle.f . . . . . . . . 9 (𝜑𝐹:𝐴⟶(0[,]+∞))
3127simplbi 493 . . . . . . . . 9 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠𝐴)
32 fssres 6308 . . . . . . . . 9 ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠𝐴) → (𝐹𝑠):𝑠⟶(0[,]+∞))
3330, 31, 32syl2an 591 . . . . . . . 8 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑠):𝑠⟶(0[,]+∞))
34 c0ex 10351 . . . . . . . . . 10 0 ∈ V
3534a1i 11 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V)
3633, 29, 35fdmfifsupp 8555 . . . . . . . 8 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑠) finSupp 0)
375, 23, 26, 29, 33, 36gsumcl 18670 . . . . . . 7 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑠)) ∈ (0[,]+∞))
381, 37sseldi 3826 . . . . . 6 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑠)) ∈ ℝ*)
3938fmpttd 6635 . . . . 5 (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ*)
4039frnd 6286 . . . 4 (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
41 0ss 4198 . . . . . . 7 ∅ ⊆ 𝐴
42 0fin 8458 . . . . . . 7 ∅ ∈ Fin
43 elfpw 8538 . . . . . . 7 (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
4441, 42, 43mpbir2an 704 . . . . . 6 ∅ ∈ (𝒫 𝐴 ∩ Fin)
45 0cn 10349 . . . . . 6 0 ∈ ℂ
46 eqid 2826 . . . . . . 7 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))
47 reseq2 5625 . . . . . . . . . 10 (𝑠 = ∅ → (𝐹𝑠) = (𝐹 ↾ ∅))
48 res0 5634 . . . . . . . . . 10 (𝐹 ↾ ∅) = ∅
4947, 48syl6eq 2878 . . . . . . . . 9 (𝑠 = ∅ → (𝐹𝑠) = ∅)
5049oveq2d 6922 . . . . . . . 8 (𝑠 = ∅ → (𝐺 Σg (𝐹𝑠)) = (𝐺 Σg ∅))
5123gsum0 17632 . . . . . . . 8 (𝐺 Σg ∅) = 0
5250, 51syl6eq 2878 . . . . . . 7 (𝑠 = ∅ → (𝐺 Σg (𝐹𝑠)) = 0)
5346, 52elrnmpt1s 5607 . . . . . 6 ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))))
5444, 45, 53mp2an 685 . . . . 5 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))
5554a1i 11 . . . 4 (𝜑 → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))))
5640, 55sseldd 3829 . . 3 (𝜑 → 0 ∈ ℝ*)
5725a1i 11 . . . . 5 (𝜑𝐺 ∈ CMnd)
58 xrge0gsumle.b . . . . . . 7 (𝜑𝐵 ∈ (𝒫 𝐴 ∩ Fin))
59 elfpw 8538 . . . . . . . 8 (𝐵 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐵𝐴𝐵 ∈ Fin))
6059simprbi 492 . . . . . . 7 (𝐵 ∈ (𝒫 𝐴 ∩ Fin) → 𝐵 ∈ Fin)
6158, 60syl 17 . . . . . 6 (𝜑𝐵 ∈ Fin)
62 diffi 8462 . . . . . 6 (𝐵 ∈ Fin → (𝐵𝐶) ∈ Fin)
6361, 62syl 17 . . . . 5 (𝜑 → (𝐵𝐶) ∈ Fin)
6459simplbi 493 . . . . . . . 8 (𝐵 ∈ (𝒫 𝐴 ∩ Fin) → 𝐵𝐴)
6558, 64syl 17 . . . . . . 7 (𝜑𝐵𝐴)
6665ssdifssd 3976 . . . . . 6 (𝜑 → (𝐵𝐶) ⊆ 𝐴)
6730, 66fssresd 6309 . . . . 5 (𝜑 → (𝐹 ↾ (𝐵𝐶)):(𝐵𝐶)⟶(0[,]+∞))
6834a1i 11 . . . . . 6 (𝜑 → 0 ∈ V)
6967, 63, 68fdmfifsupp 8555 . . . . 5 (𝜑 → (𝐹 ↾ (𝐵𝐶)) finSupp 0)
705, 23, 57, 63, 67, 69gsumcl 18670 . . . 4 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ (0[,]+∞))
711, 70sseldi 3826 . . 3 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ ℝ*)
72 xrge0gsumle.c . . . . . 6 (𝜑𝐶𝐵)
73 ssfi 8450 . . . . . 6 ((𝐵 ∈ Fin ∧ 𝐶𝐵) → 𝐶 ∈ Fin)
7461, 72, 73syl2anc 581 . . . . 5 (𝜑𝐶 ∈ Fin)
7572, 65sstrd 3838 . . . . . 6 (𝜑𝐶𝐴)
7630, 75fssresd 6309 . . . . 5 (𝜑 → (𝐹𝐶):𝐶⟶(0[,]+∞))
7776, 74, 68fdmfifsupp 8555 . . . . 5 (𝜑 → (𝐹𝐶) finSupp 0)
785, 23, 57, 74, 76, 77gsumcl 18670 . . . 4 (𝜑 → (𝐺 Σg (𝐹𝐶)) ∈ (0[,]+∞))
791, 78sseldi 3826 . . 3 (𝜑 → (𝐺 Σg (𝐹𝐶)) ∈ ℝ*)
80 elxrge0 12572 . . . . 5 ((𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ (0[,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ ℝ* ∧ 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))))
8180simprbi 492 . . . 4 ((𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ (0[,]+∞) → 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵𝐶))))
8270, 81syl 17 . . 3 (𝜑 → 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵𝐶))))
83 xleadd2a 12373 . . 3 (((0 ∈ ℝ* ∧ (𝐺 Σg (𝐹 ↾ (𝐵𝐶))) ∈ ℝ* ∧ (𝐺 Σg (𝐹𝐶)) ∈ ℝ*) ∧ 0 ≤ (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))) → ((𝐺 Σg (𝐹𝐶)) +𝑒 0) ≤ ((𝐺 Σg (𝐹𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))))
8456, 71, 79, 82, 83syl31anc 1498 . 2 (𝜑 → ((𝐺 Σg (𝐹𝐶)) +𝑒 0) ≤ ((𝐺 Σg (𝐹𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))))
85 xaddid1 12361 . . 3 ((𝐺 Σg (𝐹𝐶)) ∈ ℝ* → ((𝐺 Σg (𝐹𝐶)) +𝑒 0) = (𝐺 Σg (𝐹𝐶)))
8679, 85syl 17 . 2 (𝜑 → ((𝐺 Σg (𝐹𝐶)) +𝑒 0) = (𝐺 Σg (𝐹𝐶)))
87 ovex 6938 . . . . 5 (0[,]+∞) ∈ V
88 xrsadd 20124 . . . . . 6 +𝑒 = (+g‘ℝ*𝑠)
892, 88ressplusg 16353 . . . . 5 ((0[,]+∞) ∈ V → +𝑒 = (+g𝐺))
9087, 89ax-mp 5 . . . 4 +𝑒 = (+g𝐺)
9130, 65fssresd 6309 . . . 4 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
9291, 61, 68fdmfifsupp 8555 . . . 4 (𝜑 → (𝐹𝐵) finSupp 0)
93 disjdif 4264 . . . . 5 (𝐶 ∩ (𝐵𝐶)) = ∅
9493a1i 11 . . . 4 (𝜑 → (𝐶 ∩ (𝐵𝐶)) = ∅)
95 undif2 4268 . . . . 5 (𝐶 ∪ (𝐵𝐶)) = (𝐶𝐵)
96 ssequn1 4011 . . . . . 6 (𝐶𝐵 ↔ (𝐶𝐵) = 𝐵)
9772, 96sylib 210 . . . . 5 (𝜑 → (𝐶𝐵) = 𝐵)
9895, 97syl5req 2875 . . . 4 (𝜑𝐵 = (𝐶 ∪ (𝐵𝐶)))
995, 23, 90, 57, 58, 91, 92, 94, 98gsumsplit 18682 . . 3 (𝜑 → (𝐺 Σg (𝐹𝐵)) = ((𝐺 Σg ((𝐹𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹𝐵) ↾ (𝐵𝐶)))))
10072resabs1d 5665 . . . . 5 (𝜑 → ((𝐹𝐵) ↾ 𝐶) = (𝐹𝐶))
101100oveq2d 6922 . . . 4 (𝜑 → (𝐺 Σg ((𝐹𝐵) ↾ 𝐶)) = (𝐺 Σg (𝐹𝐶)))
102 difss 3965 . . . . . 6 (𝐵𝐶) ⊆ 𝐵
103 resabs1 5664 . . . . . 6 ((𝐵𝐶) ⊆ 𝐵 → ((𝐹𝐵) ↾ (𝐵𝐶)) = (𝐹 ↾ (𝐵𝐶)))
104102, 103mp1i 13 . . . . 5 (𝜑 → ((𝐹𝐵) ↾ (𝐵𝐶)) = (𝐹 ↾ (𝐵𝐶)))
105104oveq2d 6922 . . . 4 (𝜑 → (𝐺 Σg ((𝐹𝐵) ↾ (𝐵𝐶))) = (𝐺 Σg (𝐹 ↾ (𝐵𝐶))))
106101, 105oveq12d 6924 . . 3 (𝜑 → ((𝐺 Σg ((𝐹𝐵) ↾ 𝐶)) +𝑒 (𝐺 Σg ((𝐹𝐵) ↾ (𝐵𝐶)))) = ((𝐺 Σg (𝐹𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))))
10799, 106eqtr2d 2863 . 2 (𝜑 → ((𝐺 Σg (𝐹𝐶)) +𝑒 (𝐺 Σg (𝐹 ↾ (𝐵𝐶)))) = (𝐺 Σg (𝐹𝐵)))
10884, 86, 1073brtr3d 4905 1 (𝜑 → (𝐺 Σg (𝐹𝐶)) ≤ (𝐺 Σg (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wcel 2166  wne 3000  Vcvv 3415  cdif 3796  cun 3797  cin 3798  wss 3799  c0 4145  𝒫 cpw 4379  {csn 4398   class class class wbr 4874  cmpt 4953  ran crn 5344  cres 5345  wf 6120  cfv 6124  (class class class)co 6906  Fincfn 8223  cc 10251  0cc0 10253  +∞cpnf 10389  -∞cmnf 10390  *cxr 10391  cle 10393   +𝑒 cxad 12231  [,]cicc 12467  Basecbs 16223  s cress 16224  +gcplusg 16306  0gc0g 16454   Σg cgsu 16455  *𝑠cxrs 16514  SubMndcsubmnd 17688  CMndccmn 18547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-iin 4744  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-of 7158  df-om 7328  df-1st 7429  df-2nd 7430  df-supp 7561  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-oadd 7831  df-er 8010  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-fsupp 8546  df-oi 8685  df-card 9079  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-nn 11352  df-2 11415  df-3 11416  df-4 11417  df-5 11418  df-6 11419  df-7 11420  df-8 11421  df-9 11422  df-n0 11620  df-z 11706  df-dec 11823  df-uz 11970  df-xadd 12234  df-icc 12471  df-fz 12621  df-fzo 12762  df-seq 13097  df-hash 13412  df-struct 16225  df-ndx 16226  df-slot 16227  df-base 16229  df-sets 16230  df-ress 16231  df-plusg 16319  df-mulr 16320  df-tset 16325  df-ple 16326  df-ds 16328  df-0g 16456  df-gsum 16457  df-xrs 16516  df-mre 16600  df-mrc 16601  df-acs 16603  df-mgm 17596  df-sgrp 17638  df-mnd 17649  df-submnd 17690  df-cntz 18101  df-cmn 18549
This theorem is referenced by:  xrge0tsms  23008  xrge0tsmsd  30331
  Copyright terms: Public domain W3C validator