Metamath Proof Explorer

Theorem sinccvglem

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

Ref Expression
Hypotheses sinccvg.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) )
sinccvg.2 ⊢ ( 𝜑 → 𝐹 ⇝ 0 )
sinccvg.3 ⊢ 𝐺 = ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) )
sinccvg.4 ⊢ 𝐻 = ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) )
sinccvg.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
sinccvg.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 )
Assertion sinccvglem ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ⇝ 1 )

Proof

Step Hyp Ref Expression
1 sinccvg.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) )
2 sinccvg.2 ⊢ ( 𝜑 → 𝐹 ⇝ 0 )
3 sinccvg.3 ⊢ 𝐺 = ( 𝑥 ∈ ( ℝ ∖ { 0 } ) ↦ ( ( sin ‘ 𝑥 ) / 𝑥 ) )
4 sinccvg.4 ⊢ 𝐻 = ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) )
5 sinccvg.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 sinccvg.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 )
7 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
8 5 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 4 funmpt2 ⊢ Fun 𝐻
10 nnex ⊢ ℕ ∈ V
11 fex ⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ ℕ ∈ V ) → 𝐹 ∈ V )
12 1 10 11 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
13 cofunexg ⊢ ( ( Fun 𝐻 ∧ 𝐹 ∈ V ) → ( 𝐻 ∘ 𝐹 ) ∈ V )
14 9 12 13 sylancr ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ V )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) )
16 eluznn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ )
17 5 16 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ )
18 15 17 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ ∖ { 0 } ) )
19 eldifsn ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ ∖ { 0 } ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
20 18 19 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
21 20 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
23 ax-1cn ⊢ 1 ∈ ℂ
24 sqcl ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
25 3cn ⊢ 3 ∈ ℂ
26 3ne0 ⊢ 3 ≠ 0
27 divcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( ( 𝑥 ↑ 2 ) / 3 ) ∈ ℂ )
28 25 26 27 mp3an23 ⊢ ( ( 𝑥 ↑ 2 ) ∈ ℂ → ( ( 𝑥 ↑ 2 ) / 3 ) ∈ ℂ )
29 24 28 syl ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) / 3 ) ∈ ℂ )
30 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) / 3 ) ∈ ℂ ) → ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) ∈ ℂ )
31 23 29 30 sylancr ⊢ ( 𝑥 ∈ ℂ → ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) ∈ ℂ )
32 4 31 fmpti ⊢ 𝐻 : ℂ ⟶ ℂ
33 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
34 33 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
35 34 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
36 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
37 35 35 36 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
38 33 sqcn ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
39 38 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 2 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
40 33 divccn ⊢ ( ( 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 3 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
41 25 26 40 mp2an ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 3 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
42 41 a1i ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 3 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
43 oveq1 ⊢ ( 𝑦 = ( 𝑥 ↑ 2 ) → ( 𝑦 / 3 ) = ( ( 𝑥 ↑ 2 ) / 3 ) )
44 35 39 35 42 43 cnmpt11 ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 2 ) / 3 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
45 33 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
46 45 a1i ⊢ ( ⊤ → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
47 35 37 44 46 cnmpt12f ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
48 47 mptru ⊢ ( 𝑥 ∈ ℂ ↦ ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
49 33 cncfcn1 ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
50 48 4 49 3eltr4i ⊢ 𝐻 ∈ ( ℂ –cn→ ℂ )
51 cncfi ⊢ ( ( 𝐻 ∈ ( ℂ –cn→ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 0 ) ) < 𝑧 → ( abs ‘ ( ( 𝐻 ‘ 𝑤 ) − ( 𝐻 ‘ 0 ) ) ) < 𝑦 ) )
52 50 51 mp3an1 ⊢ ( ( 0 ∈ ℂ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 0 ) ) < 𝑧 → ( abs ‘ ( ( 𝐻 ‘ 𝑤 ) − ( 𝐻 ‘ 0 ) ) ) < 𝑦 ) )
53 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑘 ) ) )
54 1 53 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑘 ) ) )
55 17 54 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝐹 ‘ 𝑘 ) ) )
56 7 2 14 8 22 32 52 55 climcn1lem ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ⇝ ( 𝐻 ‘ 0 ) )
57 0cn ⊢ 0 ∈ ℂ
58 sq0i ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 2 ) = 0 )
59 58 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 2 ) / 3 ) = ( 0 / 3 ) )
60 25 26 div0i ⊢ ( 0 / 3 ) = 0
61 59 60 eqtrdi ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 2 ) / 3 ) = 0 )
62 61 oveq2d ⊢ ( 𝑥 = 0 → ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) = ( 1 − 0 ) )
63 1m0e1 ⊢ ( 1 − 0 ) = 1
64 62 63 eqtrdi ⊢ ( 𝑥 = 0 → ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) = 1 )
65 1ex ⊢ 1 ∈ V
66 64 4 65 fvmpt ⊢ ( 0 ∈ ℂ → ( 𝐻 ‘ 0 ) = 1 )
67 57 66 ax-mp ⊢ ( 𝐻 ‘ 0 ) = 1
68 56 67 breqtrdi ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ⇝ 1 )
69 3 funmpt2 ⊢ Fun 𝐺
70 cofunexg ⊢ ( ( Fun 𝐺 ∧ 𝐹 ∈ V ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
71 69 12 70 sylancr ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
72 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( 𝑥 ↑ 2 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) )
73 72 oveq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( ( 𝑥 ↑ 2 ) / 3 ) = ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) )
74 73 oveq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( 1 − ( ( 𝑥 ↑ 2 ) / 3 ) ) = ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) )
75 ovex ⊢ ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) ∈ V
76 74 4 75 fvmpt ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( 𝐻 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) )
77 22 76 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐻 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) )
78 55 77 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) = ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) )
79 1re ⊢ 1 ∈ ℝ
80 21 resqcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) ∈ ℝ )
81 3nn ⊢ 3 ∈ ℕ
82 nndivre ⊢ ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ∈ ℝ )
83 80 81 82 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ∈ ℝ )
84 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ∈ ℝ ) → ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) ∈ ℝ )
85 79 83 84 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) ∈ ℝ )
86 78 85 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
87 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ℝ ∖ { 0 } ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
88 1 87 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
89 17 88 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) )
90 fveq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( sin ‘ 𝑥 ) = ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) )
91 id ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → 𝑥 = ( 𝐹 ‘ 𝑘 ) )
92 90 91 oveq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( ( sin ‘ 𝑥 ) / 𝑥 ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
93 ovex ⊢ ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ∈ V
94 92 3 93 fvmpt ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℝ ∖ { 0 } ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
95 18 94 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
96 89 95 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
97 21 resincld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
98 20 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
99 97 21 98 redivcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
100 96 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
101 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ∈ ℂ )
102 83 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ∈ ℂ )
103 22 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
104 103 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
105 101 102 104 subdird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) − ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
106 104 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
107 df-3 ⊢ 3 = ( 2 + 1 )
108 107 oveq2i ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) = ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ ( 2 + 1 ) )
109 2nn0 ⊢ 2 ∈ ℕ0
110 expp1 ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ ( 2 + 1 ) ) = ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
111 104 109 110 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ ( 2 + 1 ) ) = ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
112 absresq ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) )
113 21 112 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) )
114 113 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
115 111 114 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ ( 2 + 1 ) ) = ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
116 108 115 eqtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) = ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
117 116 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) = ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / 3 ) )
118 80 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) ∈ ℂ )
119 25 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 3 ∈ ℂ )
120 26 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 3 ≠ 0 )
121 118 104 119 120 div23d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / 3 ) = ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
122 117 121 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) )
123 106 122 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 1 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) − ( ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) ) )
124 105 123 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) ) )
125 22 98 absrpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ+ )
126 125 rpgt0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
127 ltle ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 1 ) )
128 103 79 127 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 1 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 1 ) )
129 6 128 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 1 )
130 0xr ⊢ 0 ∈ ℝ*
131 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 0 (,] 1 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 1 ) ) )
132 130 79 131 mp2an ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 0 (,] 1 ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ 1 ) )
133 103 126 129 132 syl3anbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 0 (,] 1 ) )
134 sin01bnd ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ( 0 (,] 1 ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) ) < ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
135 133 134 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) ) < ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
136 135 simpld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) − ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↑ 3 ) / 3 ) ) < ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
137 124 136 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
138 103 resincld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
139 85 138 125 ltmuldivd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) < ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
140 137 139 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) < ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
141 fveq2 ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) → ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) )
142 id ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
143 141 142 oveq12d ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
144 143 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) )
145 sinneg ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) = - ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) )
146 22 145 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) = - ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) )
147 146 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) = ( - ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) )
148 97 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
149 148 22 98 div2negd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( - ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
150 147 149 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
151 fveq2 ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) → ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) )
152 id ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) )
153 151 152 oveq12d ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) )
154 153 eqeq1d ⊢ ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) → ( ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( sin ‘ - ( 𝐹 ‘ 𝑘 ) ) / - ( 𝐹 ‘ 𝑘 ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) )
155 150 154 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) )
156 21 absord ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) ∨ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = - ( 𝐹 ‘ 𝑘 ) ) )
157 144 155 156 mpjaod ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) = ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
158 140 157 breqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) < ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
159 85 99 158 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 1 − ( ( ( 𝐹 ‘ 𝑘 ) ↑ 2 ) / 3 ) ) ≤ ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) )
160 159 78 96 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑘 ) ≤ ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) )
161 79 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 1 ∈ ℝ )
162 135 simprd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
163 104 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) · 1 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
164 162 163 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) · 1 ) )
165 138 161 125 ltdivmuld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 1 ↔ ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) · 1 ) ) )
166 164 165 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) / ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) < 1 )
167 157 166 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) < 1 )
168 99 161 167 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( sin ‘ ( 𝐹 ‘ 𝑘 ) ) / ( 𝐹 ‘ 𝑘 ) ) ≤ 1 )
169 96 168 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐺 ∘ 𝐹 ) ‘ 𝑘 ) ≤ 1 )
170 7 8 68 71 86 100 160 169 climsqz ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ⇝ 1 )