Theorem sinccvg

Description: ( ( sinx ) / x ) ~> 1 as (real) x ~> 0 . (Contributed by Paul Chapman, 10-Nov-2012) (Proof shortened by Mario Carneiro, 21-May-2014)

	Ref	Expression
Assertion	sinccvg	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → ( ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) ) ∘ 𝐹 ) ⇝ 1 )

Proof

Step	Hyp	Ref	Expression
1		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
2		1zzd	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → 1 ∈ ℤ )
3		1rp	⊢ 1 ∈ ℝ+
4	3	a1i	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → 1 ∈ ℝ+ )
5		eqidd	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
6		simpr	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → 𝐹 ⇝ 0 )
7	1 2 4 5 6	climi0	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 )
8		simpll	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) → 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) )
9		simplr	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) → 𝐹 ⇝ 0 )
10		eqid	⊢ ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) )
11		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) )
12		simprl	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) → 𝑗 ∈ ℕ )
13		simprr	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 )
14		2fveq3	⊢ ( 𝑘 = 𝑛 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) )
15	14	breq1d	⊢ ( 𝑘 = 𝑛 → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ↔ ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) < 1 ) )
16	15	rspccva	⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) < 1 )
17	13 16	sylan	⊢ ( ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) < 1 )
18	8 9 10 11 12 17	sinccvglem	⊢ ( ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) ∧ ( 𝑗 ∈ ℕ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 ) ) → ( ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) ) ∘ 𝐹 ) ⇝ 1 )
19	7 18	rexlimddv	⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝐹 ⇝ 0 ) → ( ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) ) ∘ 𝐹 ) ⇝ 1 )