Metamath Proof Explorer


Theorem atanbndlem

Description: Lemma for atanbnd . (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanbndlem A + arctan A π 2 π 2

Proof

Step Hyp Ref Expression
1 rpre A + A
2 atanrecl A arctan A
3 1 2 syl A + arctan A
4 picn π
5 2cn 2
6 2ne0 2 0
7 divneg π 2 2 0 π 2 = π 2
8 4 5 6 7 mp3an π 2 = π 2
9 ax-1cn 1
10 ax-icn i
11 1 recnd A + A
12 mulcl i A i A
13 10 11 12 sylancr A + i A
14 addcl 1 i A 1 + i A
15 9 13 14 sylancr A + 1 + i A
16 atanre A A dom arctan
17 1 16 syl A + A dom arctan
18 atandm2 A dom arctan A 1 i A 0 1 + i A 0
19 17 18 sylib A + A 1 i A 0 1 + i A 0
20 19 simp3d A + 1 + i A 0
21 15 20 logcld A + log 1 + i A
22 subcl 1 i A 1 i A
23 9 13 22 sylancr A + 1 i A
24 19 simp2d A + 1 i A 0
25 23 24 logcld A + log 1 i A
26 21 25 subcld A + log 1 + i A log 1 i A
27 imre log 1 + i A log 1 i A log 1 + i A log 1 i A = i log 1 + i A log 1 i A
28 26 27 syl A + log 1 + i A log 1 i A = i log 1 + i A log 1 i A
29 atanval A dom arctan arctan A = i 2 log 1 i A log 1 + i A
30 17 29 syl A + arctan A = i 2 log 1 i A log 1 + i A
31 30 oveq2d A + 2 arctan A = 2 i 2 log 1 i A log 1 + i A
32 10 5 6 divcan2i 2 i 2 = i
33 32 oveq1i 2 i 2 log 1 i A log 1 + i A = i log 1 i A log 1 + i A
34 2re 2
35 34 a1i A + 2
36 35 recnd A + 2
37 halfcl i i 2
38 10 37 mp1i A + i 2
39 25 21 subcld A + log 1 i A log 1 + i A
40 36 38 39 mulassd A + 2 i 2 log 1 i A log 1 + i A = 2 i 2 log 1 i A log 1 + i A
41 33 40 eqtr3id A + i log 1 i A log 1 + i A = 2 i 2 log 1 i A log 1 + i A
42 31 41 eqtr4d A + 2 arctan A = i log 1 i A log 1 + i A
43 21 25 negsubdi2d A + log 1 + i A log 1 i A = log 1 i A log 1 + i A
44 43 oveq2d A + i log 1 + i A log 1 i A = i log 1 i A log 1 + i A
45 42 44 eqtr4d A + 2 arctan A = i log 1 + i A log 1 i A
46 mulneg12 i log 1 + i A log 1 i A i log 1 + i A log 1 i A = i log 1 + i A log 1 i A
47 10 26 46 sylancr A + i log 1 + i A log 1 i A = i log 1 + i A log 1 i A
48 45 47 eqtr4d A + 2 arctan A = i log 1 + i A log 1 i A
49 48 fveq2d A + 2 arctan A = i log 1 + i A log 1 i A
50 remulcl 2 arctan A 2 arctan A
51 34 3 50 sylancr A + 2 arctan A
52 51 rered A + 2 arctan A = 2 arctan A
53 28 49 52 3eqtr2rd A + 2 arctan A = log 1 + i A log 1 i A
54 rpgt0 A + 0 < A
55 1 rered A + A = A
56 54 55 breqtrrd A + 0 < A
57 atanlogsublem A dom arctan 0 < A log 1 + i A log 1 i A π π
58 17 56 57 syl2anc A + log 1 + i A log 1 i A π π
59 53 58 eqeltrd A + 2 arctan A π π
60 eliooord 2 arctan A π π π < 2 arctan A 2 arctan A < π
61 59 60 syl A + π < 2 arctan A 2 arctan A < π
62 61 simpld A + π < 2 arctan A
63 pire π
64 63 renegcli π
65 64 a1i A + π
66 2pos 0 < 2
67 66 a1i A + 0 < 2
68 ltdivmul π arctan A 2 0 < 2 π 2 < arctan A π < 2 arctan A
69 65 3 35 67 68 syl112anc A + π 2 < arctan A π < 2 arctan A
70 62 69 mpbird A + π 2 < arctan A
71 8 70 eqbrtrid A + π 2 < arctan A
72 61 simprd A + 2 arctan A < π
73 63 a1i A + π
74 ltmuldiv2 arctan A π 2 0 < 2 2 arctan A < π arctan A < π 2
75 3 73 35 67 74 syl112anc A + 2 arctan A < π arctan A < π 2
76 72 75 mpbid A + arctan A < π 2
77 halfpire π 2
78 77 renegcli π 2
79 78 rexri π 2 *
80 77 rexri π 2 *
81 elioo2 π 2 * π 2 * arctan A π 2 π 2 arctan A π 2 < arctan A arctan A < π 2
82 79 80 81 mp2an arctan A π 2 π 2 arctan A π 2 < arctan A arctan A < π 2
83 3 71 76 82 syl3anbrc A + arctan A π 2 π 2