Metamath Proof Explorer

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 ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → x ∈ ℝ ∖ 0 ⟼ sin ⁡ x x ∘ F ⇝ 1

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1zzd ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → 1 ∈ ℤ
3 1rp ⊢ 1 ∈ ℝ +
4 3 a1i ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → 1 ∈ ℝ +
5 eqidd ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ k ∈ ℕ → F ⁡ k = F ⁡ k
6 simpr ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → F ⇝ 0
7 1 2 4 5 6 climi0 ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → ∃ j ∈ ℕ ∀ k ∈ ℤ ≥ j F ⁡ k < 1
8 simpll ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 → F : ℕ ⟶ ℝ ∖ 0
9 simplr ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 → F ⇝ 0
10 eqid ⊢ x ∈ ℝ ∖ 0 ⟼ sin ⁡ x x = x ∈ ℝ ∖ 0 ⟼ sin ⁡ x x
11 eqid ⊢ x ∈ ℂ ⟼ 1 − x 2 3 = x ∈ ℂ ⟼ 1 − x 2 3
12 simprl ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 → j ∈ ℕ
13 simprr ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 → ∀ k ∈ ℤ ≥ j F ⁡ k < 1
14 2fveq3 ⊢ k = n → F ⁡ k = F ⁡ n
15 14 breq1d ⊢ k = n → F ⁡ k < 1 ↔ F ⁡ n < 1
16 15 rspccva ⊢ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 ∧ n ∈ ℤ ≥ j → F ⁡ n < 1
17 13 16 sylan ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 ∧ n ∈ ℤ ≥ j → F ⁡ n < 1
18 8 9 10 11 12 17 sinccvglem ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 ∧ j ∈ ℕ ∧ ∀ k ∈ ℤ ≥ j F ⁡ k < 1 → x ∈ ℝ ∖ 0 ⟼ sin ⁡ x x ∘ F ⇝ 1
19 7 18 rexlimddv ⊢ F : ℕ ⟶ ℝ ∖ 0 ∧ F ⇝ 0 → x ∈ ℝ ∖ 0 ⟼ sin ⁡ x x ∘ F ⇝ 1