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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( log ‘ 𝐴 ) ) ≤ ( ( abs ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) + π ) )

Proof

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