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

Proof

Step Hyp Ref Expression
1 cvgcmp.1 ⊢ Z = ℤ ≥ M
2 cvgcmp.2 ⊢ φ → N ∈ Z
3 cvgcmp.3 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
4 cvgcmp.4 ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
5 cvgcmpub.5 ⊢ φ → seq M + F ⇝ A
6 cvgcmpub.6 ⊢ φ → seq M + G ⇝ B
7 cvgcmpub.7 ⊢ φ ∧ k ∈ Z → G ⁡ k ≤ F ⁡ k
8 2 1 eleqtrdi ⊢ φ → N ∈ ℤ ≥ M
9 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
10 8 9 syl ⊢ φ → M ∈ ℤ
11 1 10 4 serfre ⊢ φ → seq M + G : Z ⟶ ℝ
12 11 ffvelrnda ⊢ φ ∧ n ∈ Z → seq M + G ⁡ n ∈ ℝ
13 1 10 3 serfre ⊢ φ → seq M + F : Z ⟶ ℝ
14 13 ffvelrnda ⊢ φ ∧ n ∈ Z → seq M + F ⁡ n ∈ ℝ
15 simpr ⊢ φ ∧ n ∈ Z → n ∈ Z
16 15 1 eleqtrdi ⊢ φ ∧ n ∈ Z → n ∈ ℤ ≥ M
17 simpl ⊢ φ ∧ n ∈ Z → φ
18 elfzuz ⊢ k ∈ M … n → k ∈ ℤ ≥ M
19 18 1 eleqtrrdi ⊢ k ∈ M … n → k ∈ Z
20 17 19 4 syl2an ⊢ φ ∧ n ∈ Z ∧ k ∈ M … n → G ⁡ k ∈ ℝ
21 17 19 3 syl2an ⊢ φ ∧ n ∈ Z ∧ k ∈ M … n → F ⁡ k ∈ ℝ
22 17 19 7 syl2an ⊢ φ ∧ n ∈ Z ∧ k ∈ M … n → G ⁡ k ≤ F ⁡ k
23 16 20 21 22 serle ⊢ φ ∧ n ∈ Z → seq M + G ⁡ n ≤ seq M + F ⁡ n
24 1 10 6 5 12 14 23 climle ⊢ φ → B ≤ A