Metamath Proof Explorer

Theorem abslogle

Description: Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Assertion abslogle ⊢A∈ℂ∧A≠0→log⁡A≤log⁡A+π

Proof

Step Hyp Ref Expression
1 logcl ⊢A∈ℂ∧A≠0→log⁡A∈ℂ
2 1 abscld ⊢A∈ℂ∧A≠0→log⁡A∈ℝ
3 absrpcl ⊢A∈ℂ∧A≠0→A∈ℝ+
4 relogcl ⊢A∈ℝ+→log⁡A∈ℝ
5 3 4 syl ⊢A∈ℂ∧A≠0→log⁡A∈ℝ
6 5 recnd ⊢A∈ℂ∧A≠0→log⁡A∈ℂ
7 6 abscld ⊢A∈ℂ∧A≠0→log⁡A∈ℝ
8 1 imcld ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A∈ℝ
9 8 recnd ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A∈ℂ
10 9 abscld ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A∈ℝ
11 7 10 readdcld ⊢A∈ℂ∧A≠0→log⁡A+ℑ⁡log⁡A∈ℝ
12 pire ⊢π∈ℝ
13 12 a1i ⊢A∈ℂ∧A≠0→π∈ℝ
14 7 13 readdcld ⊢A∈ℂ∧A≠0→log⁡A+π∈ℝ
15 1 recld ⊢A∈ℂ∧A≠0→ℜ⁡log⁡A∈ℝ
16 15 recnd ⊢A∈ℂ∧A≠0→ℜ⁡log⁡A∈ℂ
17 ax-icn ⊢i∈ℂ
18 17 a1i ⊢A∈ℂ∧A≠0→i∈ℂ
19 18 9 mulcld ⊢A∈ℂ∧A≠0→i⁢ℑ⁡log⁡A∈ℂ
20 16 19 abstrid ⊢A∈ℂ∧A≠0→ℜ⁡log⁡A+i⁢ℑ⁡log⁡A≤ℜ⁡log⁡A+i⁢ℑ⁡log⁡A
21 1 replimd ⊢A∈ℂ∧A≠0→log⁡A=ℜ⁡log⁡A+i⁢ℑ⁡log⁡A
22 21 fveq2d ⊢A∈ℂ∧A≠0→log⁡A=ℜ⁡log⁡A+i⁢ℑ⁡log⁡A
23 relog ⊢A∈ℂ∧A≠0→ℜ⁡log⁡A=log⁡A
24 23 eqcomd ⊢A∈ℂ∧A≠0→log⁡A=ℜ⁡log⁡A
25 24 fveq2d ⊢A∈ℂ∧A≠0→log⁡A=ℜ⁡log⁡A
26 18 9 absmuld ⊢A∈ℂ∧A≠0→i⁢ℑ⁡log⁡A=i⁢ℑ⁡log⁡A
27 absi ⊢i=1
28 27 oveq1i ⊢i⁢ℑ⁡log⁡A=1⁢ℑ⁡log⁡A
29 10 recnd ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A∈ℂ
30 29 mullidd ⊢A∈ℂ∧A≠0→1⁢ℑ⁡log⁡A=ℑ⁡log⁡A
31 28 30 eqtrid ⊢A∈ℂ∧A≠0→i⁢ℑ⁡log⁡A=ℑ⁡log⁡A
32 26 31 eqtr2d ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A=i⁢ℑ⁡log⁡A
33 25 32 oveq12d ⊢A∈ℂ∧A≠0→log⁡A+ℑ⁡log⁡A=ℜ⁡log⁡A+i⁢ℑ⁡log⁡A
34 20 22 33 3brtr4d ⊢A∈ℂ∧A≠0→log⁡A≤log⁡A+ℑ⁡log⁡A
35 abslogimle ⊢A∈ℂ∧A≠0→ℑ⁡log⁡A≤π
36 10 13 7 35 leadd2dd ⊢A∈ℂ∧A≠0→log⁡A+ℑ⁡log⁡A≤log⁡A+π
37 2 11 14 34 36 letrd ⊢A∈ℂ∧A≠0→log⁡A≤log⁡A+π