Metamath Proof Explorer


Theorem atanbnd

Description: The arctangent function is bounded by _pi / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanbnd A arctan A π 2 π 2

Proof

Step Hyp Ref Expression
1 atanre A A dom arctan
2 1 adantr A A < 0 A dom arctan
3 atanneg A dom arctan arctan A = arctan A
4 2 3 syl A A < 0 arctan A = arctan A
5 renegcl A A
6 5 adantr A A < 0 A
7 lt0neg1 A A < 0 0 < A
8 7 biimpa A A < 0 0 < A
9 6 8 elrpd A A < 0 A +
10 atanbndlem A + arctan A π 2 π 2
11 9 10 syl A A < 0 arctan A π 2 π 2
12 4 11 eqeltrrd A A < 0 arctan A π 2 π 2
13 halfpire π 2
14 13 recni π 2
15 14 negnegi π 2 = π 2
16 15 oveq2i π 2 π 2 = π 2 π 2
17 12 16 eleqtrrdi A A < 0 arctan A π 2 π 2
18 neghalfpire π 2
19 atanrecl A arctan A
20 19 adantr A A < 0 arctan A
21 iooneg π 2 π 2 arctan A arctan A π 2 π 2 arctan A π 2 π 2
22 18 13 20 21 mp3an12i A A < 0 arctan A π 2 π 2 arctan A π 2 π 2
23 17 22 mpbird A A < 0 arctan A π 2 π 2
24 simpr A A = 0 A = 0
25 24 fveq2d A A = 0 arctan A = arctan 0
26 atan0 arctan 0 = 0
27 25 26 eqtrdi A A = 0 arctan A = 0
28 0re 0
29 pirp π +
30 rphalfcl π + π 2 +
31 rpgt0 π 2 + 0 < π 2
32 29 30 31 mp2b 0 < π 2
33 lt0neg2 π 2 0 < π 2 π 2 < 0
34 13 33 ax-mp 0 < π 2 π 2 < 0
35 32 34 mpbi π 2 < 0
36 18 rexri π 2 *
37 13 rexri π 2 *
38 elioo2 π 2 * π 2 * 0 π 2 π 2 0 π 2 < 0 0 < π 2
39 36 37 38 mp2an 0 π 2 π 2 0 π 2 < 0 0 < π 2
40 28 35 32 39 mpbir3an 0 π 2 π 2
41 27 40 eqeltrdi A A = 0 arctan A π 2 π 2
42 elrp A + A 0 < A
43 atanbndlem A + arctan A π 2 π 2
44 42 43 sylbir A 0 < A arctan A π 2 π 2
45 lttri4 A 0 A < 0 A = 0 0 < A
46 28 45 mpan2 A A < 0 A = 0 0 < A
47 23 41 44 46 mpjao3dan A arctan A π 2 π 2