Metamath Proof Explorer


Theorem logimul

Description: Multiplying a number by _i increases the logarithm of the number by _i _pi / 2 . (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion logimul A A 0 0 A log i A = log A + i π 2

Proof

Step Hyp Ref Expression
1 logcl A A 0 log A
2 1 3adant3 A A 0 0 A log A
3 ax-icn i
4 halfpire π 2
5 4 recni π 2
6 3 5 mulcli i π 2
7 efadd log A i π 2 e log A + i π 2 = e log A e i π 2
8 2 6 7 sylancl A A 0 0 A e log A + i π 2 = e log A e i π 2
9 eflog A A 0 e log A = A
10 9 3adant3 A A 0 0 A e log A = A
11 efhalfpi e i π 2 = i
12 11 a1i A A 0 0 A e i π 2 = i
13 10 12 oveq12d A A 0 0 A e log A e i π 2 = A i
14 simp1 A A 0 0 A A
15 mulcom A i A i = i A
16 14 3 15 sylancl A A 0 0 A A i = i A
17 8 13 16 3eqtrd A A 0 0 A e log A + i π 2 = i A
18 17 fveq2d A A 0 0 A log e log A + i π 2 = log i A
19 addcl log A i π 2 log A + i π 2
20 2 6 19 sylancl A A 0 0 A log A + i π 2
21 pire π
22 21 renegcli π
23 22 a1i A A 0 0 A π
24 2 imcld A A 0 0 A log A
25 readdcl log A π 2 log A + π 2
26 24 4 25 sylancl A A 0 0 A log A + π 2
27 logimcl A A 0 π < log A log A π
28 27 3adant3 A A 0 0 A π < log A log A π
29 28 simpld A A 0 0 A π < log A
30 pirp π +
31 rphalfcl π + π 2 +
32 30 31 ax-mp π 2 +
33 ltaddrp log A π 2 + log A < log A + π 2
34 24 32 33 sylancl A A 0 0 A log A < log A + π 2
35 23 24 26 29 34 lttrd A A 0 0 A π < log A + π 2
36 imadd log A i π 2 log A + i π 2 = log A + i π 2
37 2 6 36 sylancl A A 0 0 A log A + i π 2 = log A + i π 2
38 reim π 2 π 2 = i π 2
39 5 38 ax-mp π 2 = i π 2
40 rere π 2 π 2 = π 2
41 4 40 ax-mp π 2 = π 2
42 39 41 eqtr3i i π 2 = π 2
43 42 oveq2i log A + i π 2 = log A + π 2
44 37 43 eqtrdi A A 0 0 A log A + i π 2 = log A + π 2
45 35 44 breqtrrd A A 0 0 A π < log A + i π 2
46 argrege0 A A 0 0 A log A π 2 π 2
47 4 renegcli π 2
48 47 4 elicc2i log A π 2 π 2 log A π 2 log A log A π 2
49 48 simp3bi log A π 2 π 2 log A π 2
50 46 49 syl A A 0 0 A log A π 2
51 21 recni π
52 pidiv2halves π 2 + π 2 = π
53 51 5 5 52 subaddrii π π 2 = π 2
54 50 53 breqtrrdi A A 0 0 A log A π π 2
55 4 a1i A A 0 0 A π 2
56 21 a1i A A 0 0 A π
57 leaddsub log A π 2 π log A + π 2 π log A π π 2
58 24 55 56 57 syl3anc A A 0 0 A log A + π 2 π log A π π 2
59 54 58 mpbird A A 0 0 A log A + π 2 π
60 44 59 eqbrtrd A A 0 0 A log A + i π 2 π
61 ellogrn log A + i π 2 ran log log A + i π 2 π < log A + i π 2 log A + i π 2 π
62 20 45 60 61 syl3anbrc A A 0 0 A log A + i π 2 ran log
63 logef log A + i π 2 ran log log e log A + i π 2 = log A + i π 2
64 62 63 syl A A 0 0 A log e log A + i π 2 = log A + i π 2
65 18 64 eqtr3d A A 0 0 A log i A = log A + i π 2