Metamath Proof Explorer

Theorem cvgcmpub

Description: An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014)

Ref Expression
Hypotheses cvgcmp.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
cvgcmp.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
cvgcmp.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
cvgcmp.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
cvgcmpub.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
cvgcmpub.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ 𝐵 )
cvgcmpub.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion cvgcmpub ( 𝜑 → 𝐵 ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 cvgcmp.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 cvgcmp.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 cvgcmp.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4 cvgcmp.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
5 cvgcmpub.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
6 cvgcmpub.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ 𝐵 )
7 cvgcmpub.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
8 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
10 8 9 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
11 1 10 4 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℝ )
12 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
13 1 10 3 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
14 13 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
16 15 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
17 simpl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝜑 )
18 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
19 18 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
20 17 19 4 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
21 17 19 3 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
22 17 19 7 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
23 16 20 21 22 serle ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
24 1 10 6 5 12 14 23 climle ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )