Metamath Proof Explorer

Theorem sge0lefi

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lefi.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0lefi.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0lefi.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion sge0lefi ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sge0lefi.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0lefi.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0lefi.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
4 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6 elpwinss ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑥 ⊆ 𝑋 )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑥 ⊆ 𝑋 )
8 5 7 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
9 4 8 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
10 9 adantlr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
11 1 2 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
13 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝐴 ∈ ℝ* )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑋 ∈ 𝑉 )
15 14 5 sge0less ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ ( Σ^ ‘ 𝐹 ) )
16 15 adantlr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ ( Σ^ ‘ 𝐹 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ 𝐹 ) ≤ 𝐴 )
18 10 12 13 16 17 xrletrd ⊢ ( ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 )
19 18 ralrimiva ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 )
20 19 ex ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ≤ 𝐴 → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) )
21 1 2 sge0sup ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) )
23 vex ⊢ 𝑦 ∈ V
24 eqid ⊢ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
25 24 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
26 23 25 ax-mp ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
27 26 bilani ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
28 nfv ⊢ Ⅎ 𝑥 𝜑
29 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴
30 28 29 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 )
31 nfcv ⊢ Ⅎ 𝑥 𝑦
32 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
33 32 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
34 31 33 nfel ⊢ Ⅎ 𝑥 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
35 30 34 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) )
36 nfv ⊢ Ⅎ 𝑥 𝑦 ≤ 𝐴
37 simp3 ⊢ ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) → 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) )
38 rspa ⊢ ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 )
39 38 3adant3 ⊢ ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 )
40 37 39 eqbrtrd ⊢ ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) → 𝑦 ≤ 𝐴 )
41 40 3adant1l ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) → 𝑦 ≤ 𝐴 )
42 41 3exp ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) → 𝑦 ≤ 𝐴 ) ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) → 𝑦 ≤ 𝐴 ) ) )
44 35 36 43 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) → 𝑦 ≤ 𝐴 ) )
45 27 44 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ) → 𝑦 ≤ 𝐴 )
46 45 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) 𝑦 ≤ 𝐴 )
47 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* )
48 24 rnmptss ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
49 47 48 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
50 49 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* )
51 3 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → 𝐴 ∈ ℝ* )
52 supxrleub ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) 𝑦 ≤ 𝐴 ) )
53 50 51 52 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) 𝑦 ≤ 𝐴 ) )
54 46 53 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 )
55 22 54 eqbrtrd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) → ( Σ^ ‘ 𝐹 ) ≤ 𝐴 )
56 55 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 → ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ) )
57 20 56 impbid ⊢ ( 𝜑 → ( ( Σ^ ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹 ↾ 𝑥 ) ) ≤ 𝐴 ) )