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 55 oveq1i ⊢ ( ( 2 · 2 ) · ( ( ( 𝐴 / 2 ) ↑ 2 ) / 3 ) ) = ( 4 · ( ( ( 𝐴 / 2 ) ↑ 2 ) / 3 ) )
146 29 29 124 mulassd ⊢ ( 𝐴 ∈ ( 0 (,) ( π / 2 ) ) → ( ( 2 · 2 ) · ( ( ( 𝐴 / 2 ) ↑ 2 ) / 3 ) ) = ( 2 · ( 2 · ( ( ( 𝐴 / 2 ) ↑ 2 ) / 3 ) ) ) )
147 145 146 syl5reqr ⊢ ( 𝐴 ∈ ( 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 ‘ 𝐴 ) )