Theorem sin01bnd 13784

Description: Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)

Assertion

Ref	Expression
sin01bnd	|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )

Proof of Theorem sin01bnd

Dummy variables k n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0xr 9641	. . . . . . . . 9 |- 0 e. RR*
2		1re 9596	. . . . . . . . 9 |- 1 e. RR
3		elioc2 11588	. . . . . . . . 9 |- ( ( 0 e. RR* /\ 1 e. RR ) -> ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) ) )
4	1, 2, 3	mp2an 672	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) <-> ( A e. RR /\ 0 < A /\ A <_ 1 ) )
5	4	simp1bi 1011	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> A e. RR )
6		eqid 2467	. . . . . . . 8 |- ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
7	6	resin4p 13737	. . . . . . 7 |- ( A e. RR -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
8	5, 7	syl 16	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
9	8	eqcomd 2475	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) = ( sin ` A ) )
10	5	resincld 13742	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> ( sin ` A ) e. RR )
11	10	recnd 9623	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( sin ` A ) e. CC )
12		3nn0 10814	. . . . . . . . . 10 |- 3 e. NN0
13		reexpcl 12152	. . . . . . . . . 10 |- ( ( A e. RR /\ 3 e. NN0 ) -> ( A ^ 3 ) e. RR )
14	5, 12, 13	sylancl 662	. . . . . . . . 9 |- ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) e. RR )
15		6nn 10698	. . . . . . . . 9 |- 6 e. NN
16		nndivre 10572	. . . . . . . . 9 |- ( ( ( A ^ 3 ) e. RR /\ 6 e. NN ) -> ( ( A ^ 3 ) / 6 ) e. RR )
17	14, 15, 16	sylancl 662	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) e. RR )
18	5, 17	resubcld 9988	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 6 ) ) e. RR )
19	18	recnd 9623	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( A - ( ( A ^ 3 ) / 6 ) ) e. CC )
20		ax-icn 9552	. . . . . . . . . 10 |- _i e. CC
21	5	recnd 9623	. . . . . . . . . 10 |- ( A e. ( 0 (,] 1 ) -> A e. CC )
22		mulcl 9577	. . . . . . . . . 10 |- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
23	20, 21, 22	sylancr 663	. . . . . . . . 9 |- ( A e. ( 0 (,] 1 ) -> ( _i x. A ) e. CC )
24		4nn0 10815	. . . . . . . . 9 |- 4 e. NN0
25	6	eftlcl 13706	. . . . . . . . 9 |- ( ( ( _i x. A ) e. CC /\ 4 e. NN0 ) -> sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
26	23, 24, 25	sylancl 662	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC )
27	26	imcld 12994	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
28	27	recnd 9623	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. CC )
29	11, 19, 28	subaddd 9949	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) = ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) <-> ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) = ( sin ` A ) ) )
30	9, 29	mpbird 232	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) = ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
31	30	fveq2d 5870	. . 3 |- ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) = ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) )
32	28	abscld 13233	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) e. RR )
33	26	abscld 13233	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) e. RR )
34		absimle 13108	. . . . 5 |- ( sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) e. CC -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) <_ ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
35	26, 34	syl 16	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) <_ ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) )
36		reexpcl 12152	. . . . . . 7 |- ( ( A e. RR /\ 4 e. NN0 ) -> ( A ^ 4 ) e. RR )
37	5, 24, 36	sylancl 662	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( A ^ 4 ) e. RR )
38		nndivre 10572	. . . . . 6 |- ( ( ( A ^ 4 ) e. RR /\ 6 e. NN ) -> ( ( A ^ 4 ) / 6 ) e. RR )
39	37, 15, 38	sylancl 662	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) e. RR )
40	6	ef01bndlem 13783	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 4 ) / 6 ) )
41	12	a1i 11	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> 3 e. NN0 )
42		4nn 10696	. . . . . . . . . 10 |- 4 e. NN
43	42	nnzi 10889	. . . . . . . . 9 |- 4 e. ZZ
44		3re 10610	. . . . . . . . . 10 |- 3 e. RR
45		4re 10613	. . . . . . . . . 10 |- 4 e. RR
46		3lt4 10706	. . . . . . . . . 10 |- 3 < 4
47	44, 45, 46	ltleii 9708	. . . . . . . . 9 |- 3 <_ 4
48		3nn 10695	. . . . . . . . . . 11 |- 3 e. NN
49	48	nnzi 10889	. . . . . . . . . 10 |- 3 e. ZZ
50	49	eluz1i 11090	. . . . . . . . 9 |- ( 4 e. ( ZZ>= ` 3 ) <-> ( 4 e. ZZ /\ 3 <_ 4 ) )
51	43, 47, 50	mpbir2an 918	. . . . . . . 8 |- 4 e. ( ZZ>= ` 3 )
52	51	a1i 11	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> 4 e. ( ZZ>= ` 3 ) )
53	4	simp2bi 1012	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> 0 < A )
54		0re 9597	. . . . . . . . 9 |- 0 e. RR
55		ltle 9674	. . . . . . . . 9 |- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
56	54, 5, 55	sylancr 663	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> ( 0 < A -> 0 <_ A ) )
57	53, 56	mpd 15	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> 0 <_ A )
58	4	simp3bi 1013	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> A <_ 1 )
59	5, 41, 52, 57, 58	leexp2rd 12312	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( A ^ 4 ) <_ ( A ^ 3 ) )
60		6re 10617	. . . . . . . 8 |- 6 e. RR
61	60	a1i 11	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> 6 e. RR )
62		6pos 10635	. . . . . . . 8 |- 0 < 6
63	62	a1i 11	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> 0 < 6 )
64		lediv1 10408	. . . . . . 7 |- ( ( ( A ^ 4 ) e. RR /\ ( A ^ 3 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( A ^ 4 ) <_ ( A ^ 3 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) ) )
65	37, 14, 61, 63, 64	syl112anc 1232	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) <_ ( A ^ 3 ) <-> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) ) )
66	59, 65	mpbid 210	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 4 ) / 6 ) <_ ( ( A ^ 3 ) / 6 ) )
67	33, 39, 17, 40, 66	ltletrd 9742	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) < ( ( A ^ 3 ) / 6 ) )
68	32, 33, 17, 35, 67	lelttrd 9740	. . 3 |- ( A e. ( 0 (,] 1 ) -> ( abs ` ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) ) ` k ) ) ) < ( ( A ^ 3 ) / 6 ) )
69	31, 68	eqbrtrd 4467	. 2 |- ( A e. ( 0 (,] 1 ) -> ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) )
70	10, 18, 17	absdifltd 13231	. . 3 |- ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) <-> ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) /\ ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) ) ) )
71	17	recnd 9623	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) e. CC )
72	21, 71, 71	subsub4d 9962	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) ) )
73	14	recnd 9623	. . . . . . . . . . 11 |- ( A e. ( 0 (,] 1 ) -> ( A ^ 3 ) e. CC )
74		3cn 10611	. . . . . . . . . . . . 13 |- 3 e. CC
75		3ne0 10631	. . . . . . . . . . . . 13 |- 3 =/= 0
76	74, 75	pm3.2i 455	. . . . . . . . . . . 12 |- ( 3 e. CC /\ 3 =/= 0 )
77		2cnne0 10751	. . . . . . . . . . . 12 |- ( 2 e. CC /\ 2 =/= 0 )
78		divdiv1 10256	. . . . . . . . . . . 12 |- ( ( ( A ^ 3 ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
79	76, 77, 78	mp3an23 1316	. . . . . . . . . . 11 |- ( ( A ^ 3 ) e. CC -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
80	73, 79	syl 16	. . . . . . . . . 10 |- ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 3 ) / 2 ) = ( ( A ^ 3 ) / ( 3 x. 2 ) ) )
81		3t2e6 10688	. . . . . . . . . . 11 |- ( 3 x. 2 ) = 6
82	81	oveq2i 6296	. . . . . . . . . 10 |- ( ( A ^ 3 ) / ( 3 x. 2 ) ) = ( ( A ^ 3 ) / 6 )
83	80, 82	syl6req 2525	. . . . . . . . 9 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 6 ) = ( ( ( A ^ 3 ) / 3 ) / 2 ) )
84	83, 83	oveq12d 6303	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) = ( ( ( ( A ^ 3 ) / 3 ) / 2 ) + ( ( ( A ^ 3 ) / 3 ) / 2 ) ) )
85		nndivre 10572	. . . . . . . . . . 11 |- ( ( ( A ^ 3 ) e. RR /\ 3 e. NN ) -> ( ( A ^ 3 ) / 3 ) e. RR )
86	14, 48, 85	sylancl 662	. . . . . . . . . 10 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) e. RR )
87	86	recnd 9623	. . . . . . . . 9 |- ( A e. ( 0 (,] 1 ) -> ( ( A ^ 3 ) / 3 ) e. CC )
88	87	2halvesd 10785	. . . . . . . 8 |- ( A e. ( 0 (,] 1 ) -> ( ( ( ( A ^ 3 ) / 3 ) / 2 ) + ( ( ( A ^ 3 ) / 3 ) / 2 ) ) = ( ( A ^ 3 ) / 3 ) )
89	84, 88	eqtrd 2508	. . . . . . 7 |- ( A e. ( 0 (,] 1 ) -> ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) = ( ( A ^ 3 ) / 3 ) )
90	89	oveq2d 6301	. . . . . 6 |- ( A e. ( 0 (,] 1 ) -> ( A - ( ( ( A ^ 3 ) / 6 ) + ( ( A ^ 3 ) / 6 ) ) ) = ( A - ( ( A ^ 3 ) / 3 ) ) )
91	72, 90	eqtrd 2508	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) = ( A - ( ( A ^ 3 ) / 3 ) ) )
92	91	breq1d 4457	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) <-> ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) ) )
93	21, 71	npcand 9935	. . . . 5 |- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) = A )
94	93	breq2d 4459	. . . 4 |- ( A e. ( 0 (,] 1 ) -> ( ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) <-> ( sin ` A ) < A ) )
95	92, 94	anbi12d 710	. . 3 |- ( A e. ( 0 (,] 1 ) -> ( ( ( ( A - ( ( A ^ 3 ) / 6 ) ) - ( ( A ^ 3 ) / 6 ) ) < ( sin ` A ) /\ ( sin ` A ) < ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( ( A ^ 3 ) / 6 ) ) ) <-> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) ) )
96	70, 95	bitrd 253	. 2 |- ( A e. ( 0 (,] 1 ) -> ( ( abs ` ( ( sin ` A ) - ( A - ( ( A ^ 3 ) / 6 ) ) ) ) < ( ( A ^ 3 ) / 6 ) <-> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) ) )
97	69, 96	mpbid 210	1 |- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   class class class wbr 4447   |-> cmpt 4505   ` cfv 5588  (class class class)co 6285   CCcc 9491   RRcr 9492   0cc0 9493   1c1 9494   _ici 9495   + caddc 9496   x. cmul 9498   RR*cxr 9628   < clt 9629   <_ cle 9630   - cmin 9806   / cdiv 10207   NNcn 10537   2c2 10586   3c3 10587   4c4 10588   6c6 10590   NN0cn0 10796   ZZcz 10865   ZZ>=cuz 11083   (,]cioc 11531   ^cexp 12135   !cfa 12322   Imcim 12897   abscabs 13033   sum_csu 13474   sincsin 13664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-inf2 8059  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570  ax-pre-sup 9571  ax-addf 9572  ax-mulf 9573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7043  df-rdg 7077  df-1o 7131  df-oadd 7135  df-er 7312  df-pm 7424  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-sup 7902  df-oi 7936  df-card 8321  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-n0 10797  df-z 10866  df-uz 11084  df-rp 11222  df-ioc 11535  df-ico 11536  df-fz 11674  df-fzo 11794  df-fl 11898  df-seq 12077  df-exp 12136  df-fac 12323  df-hash 12375  df-shft 12866  df-cj 12898  df-re 12899  df-im 12900  df-sqrt 13034  df-abs 13035  df-limsup 13260  df-clim 13277  df-rlim 13278  df-sum 13475  df-ef 13668  df-sin 13670

This theorem is referenced by:  sinltx  13788  sin01gt0  13789  tangtx  22723  sinccvglem  28789