Metamath Proof Explorer

Theorem iserle

Description: Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007) (Revised by Mario Carneiro, 3-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iserle.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iserle.4 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
4 iserle.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ 𝐵 )
5 iserle.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6 iserle.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
7 iserle.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
8 1 2 5 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
9 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
10 1 2 6 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℝ )
11 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℝ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
13 12 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
14 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝜑 )
15 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
16 15 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
17 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
18 14 17 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
19 14 17 6 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
20 14 17 7 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
21 13 18 19 20 serle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) )
22 1 2 3 4 9 11 21 climle ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )