This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mullidi 
 |-  ( 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 mullidd 
 |-  ( 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 eqtrid 
 |-  ( 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 mulridd 
 |-  ( 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 mullidd 
 |-  ( 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 eqtrid 
 |-  ( 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 mulridd 
 |-  ( 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 eqtrid 
 |-  ( 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 ) )