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	⊢ ( 𝜑 → 𝐺 ⇝ 𝐴 )

Metamath Proof Explorer

Theorem climsqz2

Proof