Theorem tangtx

Description: The tangent function is greater than its argument on positive reals in its principal domain. (Contributed by Mario Carneiro, 29-Jul-2014)

	Ref	Expression
Assertion	tangtx	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<\tan A$$

Proof

Step	Hyp	Ref	Expression
1		elioore	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\in ℝ$$
2	1	recoscld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos A\in ℝ$$
3	1 2	remulcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\cos A\in ℝ$$
4		1re	$$⊢1\in ℝ$$
5		rehalfcl	$$⊢A\in ℝ\to \frac{A}{2}\in ℝ$$
6	1 5	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}\in ℝ$$
7	6	resqcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^2\in ℝ$$
8		3nn	$$⊢3\in \mathbb{N}$$
9		nndivre	$$⊢\left({\left(\frac{A}{2}\right)}^2\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ$$
10	7 8 9	sylancl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ$$
11		resubcl	$$⊢\left(1\in ℝ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
12	4 10 11	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
13	1 12	remulcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ$$
14		2re	$$⊢2\in ℝ$$
15		remulcl	$$⊢\left(2\in ℝ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ\right)\to 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
16	14 10 15	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
17		resubcl	$$⊢\left(1\in ℝ\wedge 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ\right)\to 1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
18	4 16 17	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
19	13 18	remulcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ$$
20	1	resincld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin A\in ℝ$$
21	12	resqcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ$$
22		remulcl	$$⊢\left(2\in ℝ\wedge {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ$$
23	14 21 22	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ$$
24		resubcl	$$⊢\left(2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ\wedge 1\in ℝ\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1\in ℝ$$
25	23 4 24	sylancl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1\in ℝ$$
26	12 18	remulcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ$$
27	1	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\in ℂ$$
28		2cn	$$⊢2\in ℂ$$
29	28	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\in ℂ$$
30		2ne0	$$⊢2\ne 0$$
31	30	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\ne 0$$
32	27 29 31	divcan2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{A}{2}\right)=A$$
33	32	fveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos 2\left(\frac{A}{2}\right)=\cos A$$
34	6	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}\in ℂ$$
35		cos2t	$$⊢\frac{A}{2}\in ℂ\to \cos 2\left(\frac{A}{2}\right)=2{\cos \left(\frac{A}{2}\right)}^2-1$$
36	34 35	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos 2\left(\frac{A}{2}\right)=2{\cos \left(\frac{A}{2}\right)}^2-1$$
37	33 36	eqtr3d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos A=2{\cos \left(\frac{A}{2}\right)}^2-1$$
38	6	recoscld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos \left(\frac{A}{2}\right)\in ℝ$$
39	38	resqcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\cos \left(\frac{A}{2}\right)}^2\in ℝ$$
40		remulcl	$$⊢\left(2\in ℝ\wedge {\cos \left(\frac{A}{2}\right)}^2\in ℝ\right)\to 2{\cos \left(\frac{A}{2}\right)}^2\in ℝ$$
41	14 39 40	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\cos \left(\frac{A}{2}\right)}^2\in ℝ$$
42	4	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1\in ℝ$$
43	14	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\in ℝ$$
44		eliooord	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<A\wedge A<\frac{\mathrm{\pi }}{2}\right)$$
45	44	simpld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<A$$
46		2pos	$$⊢0<2$$
47	46	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<2$$
48	1 43 45 47	divgt0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<\frac{A}{2}$$
49		pire	$$⊢\mathrm{\pi }\in ℝ$$
50		rehalfcl	$$⊢\mathrm{\pi }\in ℝ\to \frac{\mathrm{\pi }}{2}\in ℝ$$
51	49 50	mp1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{\mathrm{\pi }}{2}\in ℝ$$
52	44	simprd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<\frac{\mathrm{\pi }}{2}$$
53		pigt2lt4	$$⊢\left(2<\mathrm{\pi }\wedge \mathrm{\pi }<4\right)$$
54	53	simpri	$$⊢\mathrm{\pi }<4$$
55		2t2e4	$$⊢2\cdot 2=4$$
56	54 55	breqtrri	$$⊢\mathrm{\pi }<2\cdot 2$$
57	14 46	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
58		ltdivmul	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{\mathrm{\pi }}{2}<2\leftrightarrow \mathrm{\pi }<2\cdot 2\right)$$
59	49 14 57 58	mp3an	$$⊢\frac{\mathrm{\pi }}{2}<2\leftrightarrow \mathrm{\pi }<2\cdot 2$$
60	56 59	mpbir	$$⊢\frac{\mathrm{\pi }}{2}<2$$
61	60	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{\mathrm{\pi }}{2}<2$$
62	1 51 43 52 61	lttrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<2$$
63	28	mullidi	$$⊢1\cdot 2=2$$
64	62 63	breqtrrdi	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<1\cdot 2$$
65		ltdivmul2	$$⊢\left(A\in ℝ\wedge 1\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{A}{2}<1\leftrightarrow A<1\cdot 2\right)$$
66	1 42 43 47 65	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}<1\leftrightarrow A<1\cdot 2\right)$$
67	64 66	mpbird	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}<1$$
68	6 42 67	ltled	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}\le 1$$
69		0xr	$$⊢0\in {ℝ}^{*}$$
70		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in ℝ\right)\to \left(\frac{A}{2}\in \left(0,1\right]\leftrightarrow \left(\frac{A}{2}\in ℝ\wedge 0<\frac{A}{2}\wedge \frac{A}{2}\le 1\right)\right)$$
71	69 4 70	mp2an	$$⊢\frac{A}{2}\in \left(0,1\right]\leftrightarrow \left(\frac{A}{2}\in ℝ\wedge 0<\frac{A}{2}\wedge \frac{A}{2}\le 1\right)$$
72	6 48 68 71	syl3anbrc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}\in \left(0,1\right]$$
73		cos01bnd	$$⊢\frac{A}{2}\in \left(0,1\right]\to \left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<\cos \left(\frac{A}{2}\right)\wedge \cos \left(\frac{A}{2}\right)<1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
74	72 73	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<\cos \left(\frac{A}{2}\right)\wedge \cos \left(\frac{A}{2}\right)<1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
75	74	simprd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos \left(\frac{A}{2}\right)<1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
76		cos01gt0	$$⊢\frac{A}{2}\in \left(0,1\right]\to 0<\cos \left(\frac{A}{2}\right)$$
77	72 76	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<\cos \left(\frac{A}{2}\right)$$
78		0re	$$⊢0\in ℝ$$
79		ltle	$$⊢\left(0\in ℝ\wedge \cos \left(\frac{A}{2}\right)\in ℝ\right)\to \left(0<\cos \left(\frac{A}{2}\right)\to 0\le \cos \left(\frac{A}{2}\right)\right)$$
80	78 38 79	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<\cos \left(\frac{A}{2}\right)\to 0\le \cos \left(\frac{A}{2}\right)\right)$$
81	77 80	mpd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0\le \cos \left(\frac{A}{2}\right)$$
82	78	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0\in ℝ$$
83	82 38 12 77 75	lttrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
84	82 12 83	ltled	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0\le 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
85	38 12 81 84	lt2sqd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\cos \left(\frac{A}{2}\right)<1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\leftrightarrow {\cos \left(\frac{A}{2}\right)}^2<{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\right)$$
86	75 85	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\cos \left(\frac{A}{2}\right)}^2<{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2$$
87		ltmul2	$$⊢\left({\cos \left(\frac{A}{2}\right)}^2\in ℝ\wedge {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({\cos \left(\frac{A}{2}\right)}^2<{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\leftrightarrow 2{\cos \left(\frac{A}{2}\right)}^2<2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\right)$$
88	39 21 43 47 87	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left({\cos \left(\frac{A}{2}\right)}^2<{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\leftrightarrow 2{\cos \left(\frac{A}{2}\right)}^2<2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2\right)$$
89	86 88	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\cos \left(\frac{A}{2}\right)}^2<2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2$$
90	41 23 42 89	ltsub1dd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\cos \left(\frac{A}{2}\right)}^2-1<2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1$$
91	37 90	eqbrtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos A<2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1$$
92		3re	$$⊢3\in ℝ$$
93		remulcl	$$⊢\left(3\in ℝ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ\right)\to 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
94	92 10 93	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
95		4re	$$⊢4\in ℝ$$
96		remulcl	$$⊢\left(4\in ℝ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ\right)\to 4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
97	95 10 96	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ$$
98	10	resqcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ$$
99		remulcl	$$⊢\left(2\in ℝ\wedge {\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ\right)\to 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ$$
100	14 98 99	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ$$
101		readdcl	$$⊢\left(1\in ℝ\wedge 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ$$
102	4 100 101	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℝ$$
103		3lt4	$$⊢3<4$$
104	92	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\in ℝ$$
105	95	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 4\in ℝ$$
106	48	gt0ne0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{A}{2}\ne 0$$
107	6 106	sqgt0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<{\left(\frac{A}{2}\right)}^2$$
108		3pos	$$⊢0<3$$
109	108	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<3$$
110	7 104 107 109	divgt0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<\frac{{\left(\frac{A}{2}\right)}^2}{3}$$
111		ltmul1	$$⊢\left(3\in ℝ\wedge 4\in ℝ\wedge \left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℝ\wedge 0<\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\to \left(3<4\leftrightarrow 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
112	104 105 10 110 111	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(3<4\leftrightarrow 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
113	103 112	mpbii	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
114	94 97 102 113	ltsub2dd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
115	42	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1\in ℂ$$
116		ax-1cn	$$⊢1\in ℂ$$
117	100	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
118		addcl	$$⊢\left(1\in ℂ\wedge 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
119	116 117 118	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
120	97	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
121	119 120	subcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
122		sq1	$$⊢1^2=1$$
123	122	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1^2=1$$
124	10	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℂ$$
125	124	mullidd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\frac{{\left(\frac{A}{2}\right)}^2}{3}$$
126	125	oveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 21\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
127	123 126	oveq12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1^2-21\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
128	127	oveq1d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1^2-21\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
129		binom2sub	$$⊢\left(1\in ℂ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℂ\right)\to {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2=1^2-21\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
130	116 124 129	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2=1^2-21\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
131	98	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
132	16	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
133	115 131 132	addsubd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
134	128 130 133	3eqtr4d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2=1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
135	134	oveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2=2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
136		addcl	$$⊢\left(1\in ℂ\wedge {\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ\right)\to 1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
137	116 131 136	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\in ℂ$$
138	29 137 132	subdid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-22\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
139	29 115 131	adddid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)=2\cdot 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
140	116	2timesi	$$⊢2\cdot 1=1+1$$
141	140	oveq1i	$$⊢2\cdot 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=1+1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
142	115 115 117	addassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=1+1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
143	141 142	eqtrid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\cdot 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=1+1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
144	139 143	eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)=1+1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
145	29 29 124	mulassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\cdot 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=22\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
146	55	oveq1i	$$⊢2\cdot 2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
147	145 146	eqtr3di	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 22\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
148	144 147	oveq12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-22\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1+\left(1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
149	115 119 120 148	assraddsubd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(1+{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-22\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1+\left(1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
150	135 138 149	3eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2=1+\left(1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
151	115 121 150	mvrladdd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1=1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-4\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
152		subcl	$$⊢\left(1\in ℂ\wedge \frac{{\left(\frac{A}{2}\right)}^2}{3}\in ℂ\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
153	116 124 152	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
154	153 115 132	subdid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cdot 1-\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
155	153	mulridd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cdot 1=1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
156	115 124 132	subdird	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=12\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
157	132	mullidd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 12\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
158	124 29 124	mul12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
159	124	sqvald	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
160	159	oveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
161	158 160	eqtr4d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
162	157 161	oveq12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 12\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
163	156 162	eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2$$
164	155 163	oveq12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cdot 1-\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-\left(2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)$$
165	115 124 132 117	subadd4d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-\left(2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)=1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-\left(\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
166		df-3	$$⊢3=2+1$$
167	28 116	addcomi	$$⊢2+1=1+2$$
168	166 167	eqtri	$$⊢3=1+2$$
169	168	oveq1i	$$⊢3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\left(1+2\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
170	125	oveq1d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
171	115 124 29 170	joinlmuladdmuld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1+2\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
172	169 171	eqtrid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
173	172	oveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-\left(\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)+2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
174	165 173	eqtr4d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-\left(2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)-2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2\right)=1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
175	154 164 174	3eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=1+2{\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)}^2-3\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
176	114 151 175	3brtr4d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2{\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)}^2-1<\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
177	2 25 26 91 176	lttrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos A<\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
178		ltmul2	$$⊢\left(\cos A\in ℝ\wedge \left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(\cos A<\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\leftrightarrow A\cos A<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\right)$$
179	2 26 1 45 178	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\cos A<\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\leftrightarrow A\cos A<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\right)$$
180	177 179	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\cos A<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
181	18	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℂ$$
182	27 153 181	mulassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
183	180 182	breqtrrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\cos A<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
184	13 38	remulcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)\in ℝ$$
185	74	simpld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<\cos \left(\frac{A}{2}\right)$$
186	1 12 45 83	mulgt0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
187		ltmul2	$$⊢\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\in ℝ\wedge \cos \left(\frac{A}{2}\right)\in ℝ\wedge \left(A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ\wedge 0<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\right)\right)\to \left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<\cos \left(\frac{A}{2}\right)\leftrightarrow A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)\right)$$
188	18 38 13 186 187	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)<\cos \left(\frac{A}{2}\right)\leftrightarrow A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)\right)$$
189	185 188	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)$$
190	29 34 153	mulassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=2\left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
191	32	oveq1d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)$$
192	34 115 124	subdid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=\left(\frac{A}{2}\right)\cdot 1-\left(\frac{A}{2}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
193	34	mulridd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)\cdot 1=\frac{A}{2}$$
194	166	oveq2i	$$⊢{\left(\frac{A}{2}\right)}^3={\left(\frac{A}{2}\right)}^{2+1}$$
195		2nn0	$$⊢2\in {\mathbb{N}}_0$$
196		expp1	$$⊢\left(\frac{A}{2}\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to {\left(\frac{A}{2}\right)}^{2+1}={\left(\frac{A}{2}\right)}^2\left(\frac{A}{2}\right)$$
197	34 195 196	sylancl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^{2+1}={\left(\frac{A}{2}\right)}^2\left(\frac{A}{2}\right)$$
198	194 197	eqtrid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^3={\left(\frac{A}{2}\right)}^2\left(\frac{A}{2}\right)$$
199	7	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^2\in ℂ$$
200	199 34	mulcomd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^2\left(\frac{A}{2}\right)=\left(\frac{A}{2}\right){\left(\frac{A}{2}\right)}^2$$
201	198 200	eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^3=\left(\frac{A}{2}\right){\left(\frac{A}{2}\right)}^2$$
202	201	oveq1d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{{\left(\frac{A}{2}\right)}^3}{3}=\frac{\left(\frac{A}{2}\right){\left(\frac{A}{2}\right)}^2}{3}$$
203		3cn	$$⊢3\in ℂ$$
204	203	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\in ℂ$$
205		3ne0	$$⊢3\ne 0$$
206	205	a1i	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 3\ne 0$$
207	34 199 204 206	divassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{\left(\frac{A}{2}\right){\left(\frac{A}{2}\right)}^2}{3}=\left(\frac{A}{2}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)$$
208	202 207	eqtr2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\frac{{\left(\frac{A}{2}\right)}^3}{3}$$
209	193 208	oveq12d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)\cdot 1-\left(\frac{A}{2}\right)\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)=\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)$$
210	192 209	eqtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)$$
211	210	oveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\frac{A}{2}\right)\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=2\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\right)$$
212	190 191 211	3eqtr3d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)=2\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\right)$$
213		sin01bnd	$$⊢\frac{A}{2}\in \left(0,1\right]\to \left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)<\sin \left(\frac{A}{2}\right)\wedge \sin \left(\frac{A}{2}\right)<\frac{A}{2}\right)$$
214	72 213	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)<\sin \left(\frac{A}{2}\right)\wedge \sin \left(\frac{A}{2}\right)<\frac{A}{2}\right)$$
215	214	simpld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)<\sin \left(\frac{A}{2}\right)$$
216		3nn0	$$⊢3\in {\mathbb{N}}_0$$
217		reexpcl	$$⊢\left(\frac{A}{2}\in ℝ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{A}{2}\right)}^3\in ℝ$$
218	6 216 217	sylancl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to {\left(\frac{A}{2}\right)}^3\in ℝ$$
219		nndivre	$$⊢\left({\left(\frac{A}{2}\right)}^3\in ℝ\wedge 3\in \mathbb{N}\right)\to \frac{{\left(\frac{A}{2}\right)}^3}{3}\in ℝ$$
220	218 8 219	sylancl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \frac{{\left(\frac{A}{2}\right)}^3}{3}\in ℝ$$
221	6 220	resubcld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\in ℝ$$
222	6	resincld	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin \left(\frac{A}{2}\right)\in ℝ$$
223		ltmul2	$$⊢\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\in ℝ\wedge \sin \left(\frac{A}{2}\right)\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)<\sin \left(\frac{A}{2}\right)\leftrightarrow 2\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)\right)$$
224	221 222 43 47 223	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)<\sin \left(\frac{A}{2}\right)\leftrightarrow 2\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)\right)$$
225	215 224	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\left(\left(\frac{A}{2}\right)-\left(\frac{{\left(\frac{A}{2}\right)}^3}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)$$
226	212 225	eqbrtrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)$$
227		remulcl	$$⊢\left(2\in ℝ\wedge \sin \left(\frac{A}{2}\right)\in ℝ\right)\to 2\sin \left(\frac{A}{2}\right)\in ℝ$$
228	14 222 227	sylancr	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\sin \left(\frac{A}{2}\right)\in ℝ$$
229		ltmul1	$$⊢\left(A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\in ℝ\wedge 2\sin \left(\frac{A}{2}\right)\in ℝ\wedge \left(\cos \left(\frac{A}{2}\right)\in ℝ\wedge 0<\cos \left(\frac{A}{2}\right)\right)\right)\to \left(A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)\leftrightarrow A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)<2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)\right)$$
230	13 228 38 77 229	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<2\sin \left(\frac{A}{2}\right)\leftrightarrow A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)<2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)\right)$$
231	226 230	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)<2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)$$
232	222	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin \left(\frac{A}{2}\right)\in ℂ$$
233	38	recnd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos \left(\frac{A}{2}\right)\in ℂ$$
234	29 232 233	mulassd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)=2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)$$
235		sin2t	$$⊢\frac{A}{2}\in ℂ\to \sin 2\left(\frac{A}{2}\right)=2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)$$
236	34 235	syl	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin 2\left(\frac{A}{2}\right)=2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)$$
237	32	fveq2d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin 2\left(\frac{A}{2}\right)=\sin A$$
238	234 236 237	3eqtr2rd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \sin A=2\sin \left(\frac{A}{2}\right)\cos \left(\frac{A}{2}\right)$$
239	231 238	breqtrrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\cos \left(\frac{A}{2}\right)<\sin A$$
240	19 184 20 189 239	lttrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\left(1-\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)\left(1-2\left(\frac{{\left(\frac{A}{2}\right)}^2}{3}\right)\right)<\sin A$$
241	3 19 20 183 240	lttrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A\cos A<\sin A$$
242		sincosq1sgn	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<\sin A\wedge 0<\cos A\right)$$
243	242	simprd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to 0<\cos A$$
244		ltmuldiv	$$⊢\left(A\in ℝ\wedge \sin A\in ℝ\wedge \left(\cos A\in ℝ\wedge 0<\cos A\right)\right)\to \left(A\cos A<\sin A\leftrightarrow A<\frac{\sin A}{\cos A}\right)$$
245	1 20 2 243 244	syl112anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(A\cos A<\sin A\leftrightarrow A<\frac{\sin A}{\cos A}\right)$$
246	241 245	mpbid	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<\frac{\sin A}{\cos A}$$
247	243	gt0ne0d	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \cos A\ne 0$$
248		tanval	$$⊢\left(A\in ℂ\wedge \cos A\ne 0\right)\to \tan A=\frac{\sin A}{\cos A}$$
249	27 247 248	syl2anc	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \tan A=\frac{\sin A}{\cos A}$$
250	246 249	breqtrrd	$$⊢A\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to A<\tan A$$