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 ⊢ Z = ℤ ≥ M
iserle.2 ⊢ φ → M ∈ ℤ
iserle.4 ⊢ φ → seq M + F ⇝ A
iserle.5 ⊢ φ → seq M + G ⇝ B
iserle.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
iserle.7 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
iserle.8 ⊢ φ ∧ k ∈ Z → F ⁡ k ≤ G ⁡ k
Assertion iserle ⊢ φ → A ≤ B

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ Z = ℤ ≥ M
2 iserle.2 ⊢ φ → M ∈ ℤ
3 iserle.4 ⊢ φ → seq M + F ⇝ A
4 iserle.5 ⊢ φ → seq M + G ⇝ B
5 iserle.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
6 iserle.7 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
7 iserle.8 ⊢ φ ∧ k ∈ Z → F ⁡ k ≤ G ⁡ k
8 1 2 5 serfre ⊢ φ → seq M + F : Z ⟶ ℝ
9 8 ffvelcdmda ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ∈ ℝ
10 1 2 6 serfre ⊢ φ → seq M + G : Z ⟶ ℝ
11 10 ffvelcdmda ⊢ φ ∧ j ∈ Z → seq M + G ⁡ j ∈ ℝ
12 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
13 12 1 eleqtrdi ⊢ φ ∧ j ∈ Z → j ∈ ℤ ≥ M
14 simpll ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → φ
15 elfzuz ⊢ k ∈ M … j → k ∈ ℤ ≥ M
16 15 1 eleqtrrdi ⊢ k ∈ M … j → k ∈ Z
17 16 adantl ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → k ∈ Z
18 14 17 5 syl2anc ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → F ⁡ k ∈ ℝ
19 14 17 6 syl2anc ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → G ⁡ k ∈ ℝ
20 14 17 7 syl2anc ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j → F ⁡ k ≤ G ⁡ k
21 13 18 19 20 serle ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ≤ seq M + G ⁡ j
22 1 2 3 4 9 11 21 climle ⊢ φ → A ≤ B