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 ( 𝜑𝐴𝐵 )