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 (0, \frac{π}{2}) \to A < \tan A$

Proof

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

Metamath Proof Explorer

Theorem tangtx

Proof