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 biimpi ( 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) )
28 27 adantl ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ) → ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) )
29 nfv 𝑥 𝜑
30 nfra1 𝑥𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴
31 29 30 nfan 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 )
32 nfcv 𝑥 𝑦
33 nfmpt1 𝑥 ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) )
34 33 nfrn 𝑥 ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) )
35 32 34 nfel 𝑥 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) )
36 31 35 nfan 𝑥 ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) )
37 nfv 𝑥 𝑦𝐴
38 simp3 ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) ) → 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) )
39 rspa ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 )
40 39 3adant3 ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) ) → ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 )
41 38 40 eqbrtrd ( ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) ) → 𝑦𝐴 )
42 41 3adant1l ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) ) → 𝑦𝐴 )
43 42 3exp ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) → 𝑦𝐴 ) ) )
44 43 adantr ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ) → ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) → 𝑦𝐴 ) ) )
45 36 37 44 rexlimd ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑦 = ( Σ^ ‘ ( 𝐹𝑥 ) ) → 𝑦𝐴 ) )
46 28 45 mpd ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) ∧ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ) → 𝑦𝐴 )
47 46 ralrimiva ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) 𝑦𝐴 )
48 9 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ∈ ℝ* )
49 24 rnmptss ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ∈ ℝ* → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ⊆ ℝ* )
50 48 49 syl ( 𝜑 → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ⊆ ℝ* )
51 50 adantr ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ⊆ ℝ* )
52 3 adantr ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → 𝐴 ∈ ℝ* )
53 supxrleub ( ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) ⊆ ℝ*𝐴 ∈ ℝ* ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) 𝑦𝐴 ) )
54 51 52 53 syl2anc ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → ( sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑦 ∈ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) 𝑦𝐴 ) )
55 47 54 mpbird ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ ( Σ^ ‘ ( 𝐹𝑥 ) ) ) , ℝ* , < ) ≤ 𝐴 )
56 22 55 eqbrtrd ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) → ( Σ^𝐹 ) ≤ 𝐴 )
57 56 ex ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 → ( Σ^𝐹 ) ≤ 𝐴 ) )
58 20 57 impbid ( 𝜑 → ( ( Σ^𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ( Σ^ ‘ ( 𝐹𝑥 ) ) ≤ 𝐴 ) )