Metamath Proof Explorer


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 mulid2i ( 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 mulid2d ( 𝐴 ∈ ( 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 syl5eq ( 𝐴 ∈ ( 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 mulid1d ( 𝐴 ∈ ( 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 mulid2d ( 𝐴 ∈ ( 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 syl5eq ( 𝐴 ∈ ( 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 mulid1d ( 𝐴 ∈ ( 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 syl5eq ( 𝐴 ∈ ( 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 ‘ 𝐴 ) )