Metamath Proof Explorer

Theorem logi

Description: Calculate the logarithm of _i . (Contributed by Scott Fenton, 13-Apr-2020)

Ref Expression
Assertion logi ( log ‘ i ) = ( i · ( π / 2 ) )

Proof

Step Hyp Ref Expression
1 efhalfpi ⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i
2 ax-icn ⊢ i ∈ ℂ
3 ine0 ⊢ i ≠ 0
4 halfpire ⊢ ( π / 2 ) ∈ ℝ
5 4 recni ⊢ ( π / 2 ) ∈ ℂ
6 2 5 mulcli ⊢ ( i · ( π / 2 ) ) ∈ ℂ
7 pipos ⊢ 0 < π
8 pire ⊢ π ∈ ℝ
9 lt0neg2 ⊢ ( π ∈ ℝ → ( 0 < π ↔ - π < 0 ) )
10 8 9 ax-mp ⊢ ( 0 < π ↔ - π < 0 )
11 7 10 mpbi ⊢ - π < 0
12 halfpos2 ⊢ ( π ∈ ℝ → ( 0 < π ↔ 0 < ( π / 2 ) ) )
13 8 12 ax-mp ⊢ ( 0 < π ↔ 0 < ( π / 2 ) )
14 7 13 mpbi ⊢ 0 < ( π / 2 )
15 8 renegcli ⊢ - π ∈ ℝ
16 0re ⊢ 0 ∈ ℝ
17 15 16 4 lttri ⊢ ( ( - π < 0 ∧ 0 < ( π / 2 ) ) → - π < ( π / 2 ) )
18 11 14 17 mp2an ⊢ - π < ( π / 2 )
19 reim ⊢ ( ( π / 2 ) ∈ ℂ → ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) ) )
20 5 19 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) )
21 rere ⊢ ( ( π / 2 ) ∈ ℝ → ( ℜ ‘ ( π / 2 ) ) = ( π / 2 ) )
22 4 21 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( π / 2 )
23 20 22 eqtr3i ⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) = ( π / 2 )
24 18 23 breqtrri ⊢ - π < ( ℑ ‘ ( i · ( π / 2 ) ) )
25 8 a1i ⊢ ( ⊤ → π ∈ ℝ )
26 25 25 ltaddposd ⊢ ( ⊤ → ( 0 < π ↔ π < ( π + π ) ) )
27 7 26 mpbii ⊢ ( ⊤ → π < ( π + π ) )
28 picn ⊢ π ∈ ℂ
29 28 times2i ⊢ ( π · 2 ) = ( π + π )
30 27 29 breqtrrdi ⊢ ( ⊤ → π < ( π · 2 ) )
31 2rp ⊢ 2 ∈ ℝ+
32 31 a1i ⊢ ( ⊤ → 2 ∈ ℝ+ )
33 25 25 32 ltdivmul2d ⊢ ( ⊤ → ( ( π / 2 ) < π ↔ π < ( π · 2 ) ) )
34 30 33 mpbird ⊢ ( ⊤ → ( π / 2 ) < π )
35 34 mptru ⊢ ( π / 2 ) < π
36 4 8 35 ltleii ⊢ ( π / 2 ) ≤ π
37 23 36 eqbrtri ⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) ≤ π
38 ellogrn ⊢ ( ( i · ( π / 2 ) ) ∈ ran log ↔ ( ( i · ( π / 2 ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( i · ( π / 2 ) ) ) ∧ ( ℑ ‘ ( i · ( π / 2 ) ) ) ≤ π ) )
39 6 24 37 38 mpbir3an ⊢ ( i · ( π / 2 ) ) ∈ ran log
40 logeftb ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ ( i · ( π / 2 ) ) ∈ ran log ) → ( ( log ‘ i ) = ( i · ( π / 2 ) ) ↔ ( exp ‘ ( i · ( π / 2 ) ) ) = i ) )
41 2 3 39 40 mp3an ⊢ ( ( log ‘ i ) = ( i · ( π / 2 ) ) ↔ ( exp ‘ ( i · ( π / 2 ) ) ) = i )
42 1 41 mpbir ⊢ ( log ‘ i ) = ( i · ( π / 2 ) )