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	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℝ )
13	1 10 3	serfre	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
14	13	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 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	⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )