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