Metamath Proof Explorer


Theorem argrege0

Description: Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion argrege0 AA00AlogAπ2π2

Proof

Step Hyp Ref Expression
1 logcl AA0logA
2 1 3adant3 AA00AlogA
3 2 imcld AA00AlogA
4 simp3 AA00A0A
5 simp1 AA00AA
6 5 abscld AA00AA
7 6 recnd AA00AA
8 7 mul01d AA00AA0=0
9 absrpcl AA0A+
10 9 3adant3 AA00AA+
11 10 rpne0d AA00AA0
12 5 7 11 divcld AA00AAA
13 6 12 remul2d AA00AAAA=AAA
14 5 7 11 divcan2d AA00AAAA=A
15 14 fveq2d AA00AAAA=A
16 13 15 eqtr3d AA00AAAA=A
17 4 8 16 3brtr4d AA00AA0AAA
18 0re 0
19 18 a1i AA00A0
20 12 recld AA00AAA
21 19 20 10 lemul2d AA00A0AAA0AAA
22 17 21 mpbird AA00A0AA
23 efiarg AA0eilogA=AA
24 23 3adant3 AA00AeilogA=AA
25 24 fveq2d AA00AeilogA=AA
26 22 25 breqtrrd AA00A0eilogA
27 recosval logAcoslogA=eilogA
28 3 27 syl AA00AcoslogA=eilogA
29 26 28 breqtrrd AA00A0coslogA
30 halfpire π2
31 pirp π+
32 rphalfcl π+π2+
33 rpge0 π2+0π2
34 31 32 33 mp2b 0π2
35 pire π
36 rphalflt π+π2<π
37 31 36 ax-mp π2<π
38 30 35 37 ltleii π2π
39 18 35 elicc2i π20ππ20π2π2π
40 30 34 38 39 mpbir3an π20π
41 3 recnd AA00AlogA
42 41 abscld AA00AlogA
43 41 absge0d AA00A0logA
44 logimcl AA0π<logAlogAπ
45 44 3adant3 AA00Aπ<logAlogAπ
46 45 simpld AA00Aπ<logA
47 35 renegcli π
48 ltle πlogAπ<logAπlogA
49 47 3 48 sylancr AA00Aπ<logAπlogA
50 46 49 mpd AA00AπlogA
51 45 simprd AA00AlogAπ
52 absle logAπlogAππlogAlogAπ
53 3 35 52 sylancl AA00AlogAππlogAlogAπ
54 50 51 53 mpbir2and AA00AlogAπ
55 18 35 elicc2i logA0πlogA0logAlogAπ
56 42 43 54 55 syl3anbrc AA00AlogA0π
57 cosord π20πlogA0ππ2<logAcoslogA<cosπ2
58 40 56 57 sylancr AA00Aπ2<logAcoslogA<cosπ2
59 fveq2 logA=logAcoslogA=coslogA
60 59 a1i AA00AlogA=logAcoslogA=coslogA
61 cosneg logAcoslogA=coslogA
62 41 61 syl AA00AcoslogA=coslogA
63 fveqeq2 logA=logAcoslogA=coslogAcoslogA=coslogA
64 62 63 syl5ibrcom AA00AlogA=logAcoslogA=coslogA
65 3 absord AA00AlogA=logAlogA=logA
66 60 64 65 mpjaod AA00AcoslogA=coslogA
67 coshalfpi cosπ2=0
68 67 a1i AA00Acosπ2=0
69 66 68 breq12d AA00AcoslogA<cosπ2coslogA<0
70 58 69 bitrd AA00Aπ2<logAcoslogA<0
71 70 notbid AA00A¬π2<logA¬coslogA<0
72 lenlt logAπ2logAπ2¬π2<logA
73 42 30 72 sylancl AA00AlogAπ2¬π2<logA
74 3 recoscld AA00AcoslogA
75 lenlt 0coslogA0coslogA¬coslogA<0
76 18 74 75 sylancr AA00A0coslogA¬coslogA<0
77 71 73 76 3bitr4d AA00AlogAπ20coslogA
78 29 77 mpbird AA00AlogAπ2
79 absle logAπ2logAπ2π2logAlogAπ2
80 3 30 79 sylancl AA00AlogAπ2π2logAlogAπ2
81 78 80 mpbid AA00Aπ2logAlogAπ2
82 81 simpld AA00Aπ2logA
83 81 simprd AA00AlogAπ2
84 30 renegcli π2
85 84 30 elicc2i logAπ2π2logAπ2logAlogAπ2
86 3 82 83 85 syl3anbrc AA00AlogAπ2π2