Metamath Proof Explorer

Theorem esumgect

Description: "Send n to +oo " in an inequality with an extended sum. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses esumsup.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
esumsup.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
esumgect.1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ 𝐵 )
Assertion esumgect ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 esumsup.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
2 esumsup.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3 esumgect.1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ 𝐵 )
4 1 2 esumsup ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) )
5 nfv ⊢ Ⅎ 𝑛 𝜑
6 nfcv ⊢ Ⅎ 𝑛 𝑧
7 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
8 7 nfrn ⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
9 6 8 nfel ⊢ Ⅎ 𝑛 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
10 5 9 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
11 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
12 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → 𝜑 )
13 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → 𝑛 ∈ ℕ )
14 12 13 3 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ 𝐵 )
15 11 14 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → 𝑧 ≤ 𝐵 )
16 eqid ⊢ ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
17 esumex ⊢ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ V
18 16 17 elrnmpti ⊢ ( 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
19 18 biimpi ⊢ ( 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → ∃ 𝑛 ∈ ℕ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) → ∃ 𝑛 ∈ ℕ 𝑧 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
21 10 15 20 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) → 𝑧 ≤ 𝐵 )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) 𝑧 ≤ 𝐵 )
23 ovexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ V )
24 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
25 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
26 25 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
27 26 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
28 24 27 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
29 28 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
30 nfcv ⊢ Ⅎ 𝑘 ( 1 ... 𝑛 )
31 30 esumcl ⊢ ( ( ( 1 ... 𝑛 ) ∈ V ∧ ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
32 23 29 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) )
34 16 rnmptss ⊢ ( ∀ 𝑛 ∈ ℕ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( 0 [,] +∞ ) → ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ⊆ ( 0 [,] +∞ ) )
35 33 34 syl ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ⊆ ( 0 [,] +∞ ) )
36 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
37 35 36 sstrdi ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ⊆ ℝ* )
38 36 1 sselid ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
39 supxrleub ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) 𝑧 ≤ 𝐵 ) )
40 37 38 39 syl2anc ⊢ ( 𝜑 → ( sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) 𝑧 ≤ 𝐵 ) )
41 22 40 mpbird ⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) ≤ 𝐵 )
42 4 41 eqbrtrd ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 ≤ 𝐵 )