Metamath Proof Explorer

Theorem climle

Description: Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses climadd.1 ⊢Z=ℤ≥M
climadd.2 ⊢φ→M∈ℤ
climadd.4 ⊢φ→F⇝A
climle.5 ⊢φ→G⇝B
climle.6 ⊢φ∧k∈Z→F⁡k∈ℝ
climle.7 ⊢φ∧k∈Z→G⁡k∈ℝ
climle.8 ⊢φ∧k∈Z→F⁡k≤G⁡k
Assertion climle ⊢φ→A≤B

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢Z=ℤ≥M
2 climadd.2 ⊢φ→M∈ℤ
3 climadd.4 ⊢φ→F⇝A
4 climle.5 ⊢φ→G⇝B
5 climle.6 ⊢φ∧k∈Z→F⁡k∈ℝ
6 climle.7 ⊢φ∧k∈Z→G⁡k∈ℝ
7 climle.8 ⊢φ∧k∈Z→F⁡k≤G⁡k
8 1 fvexi ⊢Z∈V
9 8 mptex ⊢j∈Z⟼G⁡j−F⁡j∈V
10 9 a1i ⊢φ→j∈Z⟼G⁡j−F⁡j∈V
11 6 recnd ⊢φ∧k∈Z→G⁡k∈ℂ
12 5 recnd ⊢φ∧k∈Z→F⁡k∈ℂ
13 fveq2 ⊢j=k→G⁡j=G⁡k
14 fveq2 ⊢j=k→F⁡j=F⁡k
15 13 14 oveq12d ⊢j=k→G⁡j−F⁡j=G⁡k−F⁡k
16 eqid ⊢j∈Z⟼G⁡j−F⁡j=j∈Z⟼G⁡j−F⁡j
17 ovex ⊢G⁡k−F⁡k∈V
18 15 16 17 fvmpt ⊢k∈Z→j∈Z⟼G⁡j−F⁡j⁡k=G⁡k−F⁡k
19 18 adantl ⊢φ∧k∈Z→j∈Z⟼G⁡j−F⁡j⁡k=G⁡k−F⁡k
20 1 2 4 10 3 11 12 19 climsub ⊢φ→j∈Z⟼G⁡j−F⁡j⇝B−A
21 6 5 resubcld ⊢φ∧k∈Z→G⁡k−F⁡k∈ℝ
22 19 21 eqeltrd ⊢φ∧k∈Z→j∈Z⟼G⁡j−F⁡j⁡k∈ℝ
23 6 5 subge0d ⊢φ∧k∈Z→0≤G⁡k−F⁡k↔F⁡k≤G⁡k
24 7 23 mpbird ⊢φ∧k∈Z→0≤G⁡k−F⁡k
25 24 19 breqtrrd ⊢φ∧k∈Z→0≤j∈Z⟼G⁡j−F⁡j⁡k
26 1 2 20 22 25 climge0 ⊢φ→0≤B−A
27 1 2 4 6 climrecl ⊢φ→B∈ℝ
28 1 2 3 5 climrecl ⊢φ→A∈ℝ
29 27 28 subge0d ⊢φ→0≤B−A↔A≤B
30 26 29 mpbid ⊢φ→A≤B