Metamath Proof Explorer

Theorem esumlub

Description: The extended sum is the lowest upper bound for the partial sums. (Contributed by Thierry Arnoux, 19-Oct-2017) (Proof shortened by AV, 12-Dec-2019)

Ref Expression
Hypotheses esumlub.f ⊢ Ⅎ 𝑘 𝜑
esumlub.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumlub.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumlub.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
esumlub.3 ⊢ ( 𝜑 → 𝑋 < Σ* 𝑘 ∈ 𝐴 𝐵 )
Assertion esumlub ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < Σ* 𝑘 ∈ 𝑎 𝐵 )

Proof

Step Hyp Ref Expression
1 esumlub.f ⊢ Ⅎ 𝑘 𝜑
2 esumlub.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 esumlub.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4 esumlub.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
5 esumlub.3 ⊢ ( 𝜑 → 𝑋 < Σ* 𝑘 ∈ 𝐴 𝐵 )
6 nfcv ⊢ Ⅎ 𝑘 𝐴
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
8 1 6 2 3 7 esumval ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) , ℝ* , < ) )
9 8 breq2d ⊢ ( 𝜑 → ( 𝑋 < Σ* 𝑘 ∈ 𝐴 𝐵 ↔ 𝑋 < sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) , ℝ* , < ) ) )
10 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
11 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
12 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
14 inss2 ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ Fin
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
16 14 15 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑥 ∈ Fin )
17 nfv ⊢ Ⅎ 𝑘 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin )
18 1 17 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
19 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝜑 )
20 inss1 ⊢ ( 𝒫 𝐴 ∩ Fin ) ⊆ 𝒫 𝐴
21 20 sseli ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑥 ∈ 𝒫 𝐴 )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
23 22 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑥 ⊆ 𝐴 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝑥 )
25 23 24 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐴 )
26 19 25 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
27 26 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑘 ∈ 𝑥 → 𝐵 ∈ ( 0 [,] +∞ ) ) )
28 18 27 ralrimi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑘 ∈ 𝑥 𝐵 ∈ ( 0 [,] +∞ ) )
29 11 13 16 28 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
30 10 29 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ∈ ℝ* )
31 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ∈ ℝ* )
32 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) )
33 32 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) ⊆ ℝ* )
34 31 33 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) ⊆ ℝ* )
35 supxrlub ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) ⊆ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑋 < sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) , ℝ* , < ) ↔ ∃ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) 𝑋 < 𝑦 ) )
36 34 4 35 syl2anc ⊢ ( 𝜑 → ( 𝑋 < sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) , ℝ* , < ) ↔ ∃ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) 𝑋 < 𝑦 ) )
37 9 36 bitrd ⊢ ( 𝜑 → ( 𝑋 < Σ* 𝑘 ∈ 𝐴 𝐵 ↔ ∃ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) 𝑋 < 𝑦 ) )
38 5 37 mpbid ⊢ ( 𝜑 → ∃ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) 𝑋 < 𝑦 )
39 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ∈ V
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ∈ V )
41 mpteq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) )
42 41 oveq2d ⊢ ( 𝑥 = 𝑎 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) )
43 42 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) = ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) )
44 43 39 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) )
45 44 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑦 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ) → 𝑦 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) )
47 46 breq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ) → ( 𝑋 < 𝑦 ↔ 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ) )
48 40 45 47 rexxfr2d ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 𝐵 ) ) ) 𝑋 < 𝑦 ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ) )
49 38 48 mpbid ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) )
50 nfv ⊢ Ⅎ 𝑘 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin )
51 1 50 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
53 14 52 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ Fin )
54 simpll ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝜑 )
55 20 sseli ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑎 ∈ 𝒫 𝐴 )
56 55 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝑎 ∈ 𝒫 𝐴 )
57 56 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝑎 ⊆ 𝐴 )
58 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝑘 ∈ 𝑎 )
59 57 58 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝑘 ∈ 𝐴 )
60 54 59 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑎 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
61 51 53 60 gsumesum ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) = Σ* 𝑘 ∈ 𝑎 𝐵 )
62 61 breq2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) ↔ 𝑋 < Σ* 𝑘 ∈ 𝑎 𝐵 ) )
63 62 biimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) → 𝑋 < Σ* 𝑘 ∈ 𝑎 𝐵 ) )
64 63 reximdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑎 ↦ 𝐵 ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < Σ* 𝑘 ∈ 𝑎 𝐵 ) )
65 49 64 mpd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑋 < Σ* 𝑘 ∈ 𝑎 𝐵 )