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	⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → 𝐴 < ( tan ‘ 𝐴 ) )

Proof

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