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
|- ( A e. ( 0 (,) ( _pi / 2 ) ) -> A < ( tan ` A ) )

Proof

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