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

Metamath Proof Explorer

Theorem climsqz2

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

Ref Expression
Hypotheses climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climsqz.5 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
climsqz.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
climsqz.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
climsqz2.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
climsqz2.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ ( 𝐺 ‘ 𝑘 ) )
Assertion climsqz2 ( 𝜑 → 𝐺 ⇝ 𝐴 )

Proof

Step Hyp Ref Expression
1 climadd.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climadd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climadd.4 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climsqz.5 ⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
5 climsqz.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
6 climsqz.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
7 climsqz2.8 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
8 climsqz2.9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ ( 𝐺 ‘ 𝑘 ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
11 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ⇝ 𝐴 )
13 1 9 10 11 12 climi2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
14 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
15 1 2 3 5 climrecl ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
17 6 5 16 7 lesub1dd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ≤ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
18 16 6 8 abssubge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) = ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) )
19 16 6 5 8 7 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ ( 𝐹 ‘ 𝑘 ) )
20 16 5 19 abssubge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
21 17 18 20 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
22 21 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
23 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
24 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
25 23 24 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ )
26 25 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ∈ ℂ )
27 26 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
28 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
29 28 24 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ )
30 29 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℂ )
31 30 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ )
32 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → 𝑥 ∈ ℝ )
34 lelttr ⊢ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
35 27 31 33 34 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
36 22 35 mpand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑘 ∈ 𝑍 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
37 14 36 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
38 37 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
39 38 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
40 39 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
41 13 40 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 )
43 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
44 15 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
45 6 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
46 1 2 4 43 44 45 clim2c ⊢ ( 𝜑 → ( 𝐺 ⇝ 𝐴 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( 𝐺 ‘ 𝑘 ) − 𝐴 ) ) < 𝑥 ) )
47 42 46 mpbird ⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )