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 )