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	$⊢ φ \to F : ℕ ⟶ ℝ ∖ \{0\}$
	sinccvg.2	$⊢ φ \to F ⇝ 0$
	sinccvg.3	$⊢ G = (x \in (ℝ ∖ \{0\}) ⟼ \frac{\sin x}{x})$
	sinccvg.4	$⊢ H = (x \in ℂ ⟼ 1 - (\frac{x^{2}}{3}))$
	sinccvg.5	$⊢ φ \to M \in ℕ$
	sinccvg.6	$⊢ (φ \land k \in ℤ_{\geq M}) \to \|F (k)\| < 1$
Assertion	sinccvglem	$⊢ φ \to (G \circ F) ⇝ 1$

Proof

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

Metamath Proof Explorer

Theorem sinccvglem

Proof