Metamath Proof Explorer


Theorem eflogeq

Description: Solve an equation involving an exponential. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion eflogeq ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )

Proof

Step Hyp Ref Expression
1 efcl ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
2 efne0 ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 )
3 1 2 logcld ( 𝐴 ∈ ℂ → ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ )
4 efsub ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
5 3 4 mpdan ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
6 eflog ( ( ( exp ‘ 𝐴 ) ∈ ℂ ∧ ( exp ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) )
7 1 2 6 syl2anc ( 𝐴 ∈ ℂ → ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) = ( exp ‘ 𝐴 ) )
8 7 oveq2d ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) )
9 1 2 dividd ( 𝐴 ∈ ℂ → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐴 ) ) = 1 )
10 5 8 9 3eqtrd ( 𝐴 ∈ ℂ → ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 )
11 subcl ( ( 𝐴 ∈ ℂ ∧ ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ) → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ )
12 3 11 mpdan ( 𝐴 ∈ ℂ → ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ )
13 efeq1 ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
14 12 13 syl ( 𝐴 ∈ ℂ → ( ( exp ‘ ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 1 ↔ ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
15 10 14 mpbid ( 𝐴 ∈ ℂ → ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ )
16 ax-icn i ∈ ℂ
17 2cn 2 ∈ ℂ
18 picn π ∈ ℂ
19 17 18 mulcli ( 2 · π ) ∈ ℂ
20 16 19 mulcli ( i · ( 2 · π ) ) ∈ ℂ
21 20 a1i ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ∈ ℂ )
22 ine0 i ≠ 0
23 2ne0 2 ≠ 0
24 pire π ∈ ℝ
25 pipos 0 < π
26 24 25 gt0ne0ii π ≠ 0
27 17 18 23 26 mulne0i ( 2 · π ) ≠ 0
28 16 19 22 27 mulne0i ( i · ( 2 · π ) ) ≠ 0
29 28 a1i ( 𝐴 ∈ ℂ → ( i · ( 2 · π ) ) ≠ 0 )
30 12 21 29 divcan2d ( 𝐴 ∈ ℂ → ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) = ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) )
31 30 oveq2d ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) )
32 pncan3 ( ( ( log ‘ ( exp ‘ 𝐴 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 )
33 3 32 mpancom ( 𝐴 ∈ ℂ → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) ) = 𝐴 )
34 31 33 eqtr2d ( 𝐴 ∈ ℂ → 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) )
35 oveq2 ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( i · ( 2 · π ) ) · 𝑛 ) = ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) )
36 35 oveq2d ( 𝑛 = ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) )
37 36 rspceeqv ( ( ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ∧ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · ( ( 𝐴 − ( log ‘ ( exp ‘ 𝐴 ) ) ) / ( i · ( 2 · π ) ) ) ) ) ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
38 15 34 37 syl2anc ( 𝐴 ∈ ℂ → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
39 38 3ad2ant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
40 fveq2 ( ( exp ‘ 𝐴 ) = 𝐵 → ( log ‘ ( exp ‘ 𝐴 ) ) = ( log ‘ 𝐵 ) )
41 40 oveq1d ( ( exp ‘ 𝐴 ) = 𝐵 → ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) )
42 41 eqeq2d ( ( exp ‘ 𝐴 ) = 𝐵 → ( 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
43 42 rexbidv ( ( exp ‘ 𝐴 ) = 𝐵 → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ ( exp ‘ 𝐴 ) ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
44 39 43 syl5ibcom ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 → ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
45 logcl ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
46 45 3adant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
47 zcn ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
48 47 adantl ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℂ )
49 mulcl ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
50 20 48 49 sylancr ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ )
51 efadd ( ( ( log ‘ 𝐵 ) ∈ ℂ ∧ ( ( i · ( 2 · π ) ) · 𝑛 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
52 46 50 51 syl2an2r ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )
53 eflog ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
54 53 3adant1 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
55 ef2kpi ( 𝑛 ∈ ℤ → ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) = 1 )
56 54 55 oveqan12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( ( exp ‘ ( log ‘ 𝐵 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = ( 𝐵 · 1 ) )
57 simpl2 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → 𝐵 ∈ ℂ )
58 57 mulid1d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐵 · 1 ) = 𝐵 )
59 52 56 58 3eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 )
60 fveqeq2 ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) = 𝐵 ) )
61 59 60 syl5ibrcom ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) )
62 61 rexlimdva ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) → ( exp ‘ 𝐴 ) = 𝐵 ) )
63 44 62 impbid ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( exp ‘ 𝐴 ) = 𝐵 ↔ ∃ 𝑛 ∈ ℤ 𝐴 = ( ( log ‘ 𝐵 ) + ( ( i · ( 2 · π ) ) · 𝑛 ) ) ) )