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⁡xx∘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∈ℤ≥jF⁡k<1
8 simpll ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1→F:ℕ⟶ℝ∖0
9 simplr ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1→F⇝0
10 eqid ⊢x∈ℝ∖0⟼sin⁡xx=x∈ℝ∖0⟼sin⁡xx
11 eqid ⊢x∈ℂ⟼1−x23=x∈ℂ⟼1−x23
12 simprl ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1→j∈ℕ
13 simprr ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1→∀k∈ℤ≥jF⁡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∈ℤ≥jF⁡k<1∧n∈ℤ≥j→F⁡n<1
17 13 16 sylan ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1∧n∈ℤ≥j→F⁡n<1
18 8 9 10 11 12 17 sinccvglem ⊢F:ℕ⟶ℝ∖0∧F⇝0∧j∈ℕ∧∀k∈ℤ≥jF⁡k<1→x∈ℝ∖0⟼sin⁡xx∘F⇝1
19 7 18 rexlimddv ⊢F:ℕ⟶ℝ∖0∧F⇝0→x∈ℝ∖0⟼sin⁡xx∘F⇝1