This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climle.5 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
climle.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climle.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
climle.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
Assertion climle ( 𝜑 → 𝐴 ≤ 𝐵 )

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climle.5 ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
5 climle.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6 climle.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
7 climle.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
8 1 fvexi ⊢ 𝑍 ∈ V
9 8 mptex ⊢ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ V
10 9 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ∈ V )
11 6 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
12 5 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
13 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐺 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑘 ) )
14 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
15 13 14 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
16 eqid ⊢ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) )
17 ovex ⊢ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ∈ V
18 15 16 17 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
20 1 2 4 10 3 11 12 19 climsub ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ⇝ ( 𝐵 − 𝐴 ) )
21 6 5 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
22 19 21 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) ∈ ℝ )
23 6 5 subge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
24 7 23 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
25 24 19 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐺 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) )
26 1 2 20 22 25 climge0 ⊢ ( 𝜑 → 0 ≤ ( 𝐵 − 𝐴 ) )
27 1 2 4 6 climrecl ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
28 1 2 3 5 climrecl ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
29 27 28 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝐵 − 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )
30 26 29 mpbid ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )